Architectural systems semantics

Modern CPU architectures are becoming increasingly complex; with pipelines which allow hundreds of instructions to execute at once, possibly out-of-order, writing to multiple layers
of instruction and data caches, performing both application-level software and the variety of system-level operations a device may want to perform.

Vendor specifications for such processor architectures are not always entirely explicit and clear at what is intended behaviour for an implementation and what is not. This makes testing a specific program intended to be deployed on such hardware difficult: it is not possible to know if the program behaves correctly on all possible implementations of that architecture. Instead most systems are tested on specific implementations rather than against a concrete specification of all valid behaviours or get verified agnostic to the underlying architecture entirely.
Each architecture must be tackled independently, and their semantics modelled separately. Often this is done by encoding the behaviour in some domain-specific language. In one such example, Sail, the semantics of the armv8, mips and ibm power isas have been described, at least to some extent, in an effort to allow mechanised generation and verification of test cases.
However, encoding the semantics of an entire architecture is not a small undertaking. As such, there are sizeable gaps in the armv8 model: namely, in the concurrent behaviour of the system-level operations re- quired to fully model the operation of an OS [4]. Instruction fetching, interrupt handling, virtual memory and paging, are some key aspects of the architecture that must be fully modelled before a real substantial effort in testing and validating programs at that level can be undertaken.

The proposed research therefore will have 3 goals: (1) to analyse the armv8 architecture to produce a semantic model of the system-level components, (2) to validate these models to ensure they match common implementations of the underlying architecture and (3) to use these models to create the foundation for a test oracle for testing software and hardware for armv8-based systems.

(1). Models should be produced for the system-level instruction behaviours', particularly those pertaining to (a) instruction fetching (b) interrupts and (c) virtual memory.
(2). Validation of the instruction descriptions should be carried out to verify the modelled behaviour from (1) is indeed valid and correct. Both through automated testing and discussions with arm Engineers where possible.
(3). Use the updated model to be able to run whole system applications over an interpreter that implements an executable version of the model; to test applications over the entire envelope of acceptable behaviour for processor. Either finding defects in common processors on the market, or to help organisations test that their software are free from such defects.
Wider Impact Devices running these arm architectures are ubiquitous; both Apple and Samsung use this architecture in all their mobile devices. Finding and correcting faults in these devices would be work with immediate impact to the industry.

This work could also be extended, with the ideas and tools produced being applied on a wider range of processor architectures. Both verifying older systems (ibm power, mips) but also in advising current and future projects (risc-v) to make them more resilient and safer.

Future work could utilize the constructed models to verify (or invalidate) desirable security properties of these systems. Proving that serious vulnerabilities are impossible in their systems, or, helping discover and debug ones that are.