Expressing Intent

Expressing Intent: An evaluation of the Arm Machine Readable Specification

Kloppenburg, Jeroen (TU Delft Electrical Engineering, Mathematics and Computer Science)

Chakraborty, S.S. (mentor)
Langendoen, K.G. (graduation committee)

Delft University of Technology

Delft University of Technology

Computer Science

2023-07-11

The behaviour of software is intrinsically linked to the hardware it runs on. As hardware innovations continuously change the landscape of computing, software has to adapt to these changes. Running legacy software on new hardware requires either the old hardware to be emulated, or a very time-consuming and error-prone process of reverse engineering the software to determine its behaviour, and then writing new software that has the same behaviour, but runs on the new hardware. Binary lifting and translation tools aim to automate this process, but are often limited by the lack of accurate and complete instruction semantics.

This project aims to evaluate the feasibility of using the Arm Machine Readable Specification to aid in this process. The specification is a machine-readable description of the Arm architecture, including self-proclaimed "executable" instruction semantics, written in a specification language called ASL. This project has created an emulator that can run Arm instructions on a non-Arm architecture, using the specification to determine the behaviour of the instructions. The emulator is able to run simple programs with little context, but is not yet able to run more complex programs, due to the lack of support for behaviour that depends on the specific hardware implementation, and context dependencies outside of the instruction set, such as operating system interactions.

This emulation based solely on the specification has demonstrated that it is a promising approach to reason about the behaviour of Arm programs, but it is not complete enough to be used for binary lifting and translation. The context dependency of executables, and the lack of implementation specific behaviour in the specification are the main reasons for this.

Specification
ARM
Binary Translation
Emulation
Formal specification

http://resolver.tudelft.nl/uuid:146b06aa-6f18-4da7-8558-47a064ee8480

Student theses

master thesis

© 2023 Jeroen Kloppenburg