Formal Verification of Machine-Code Systems by Translation of Simulable Descriptions

Correctness of safety- and security-critical systems can be ensured by formal verification. While formal verification of source-code and hardware systems is widely used, existing approaches to formal verification of machine code are severely limited in verification strength and processor choice. In this paper, a formal verification tool written in the Rust programming language is introduced, with emphasis on machine-code verification. The problems of previous tools are circumvented by abstraction refinement, an advanced formal verification technique. System behaviour is defined using simulation descriptions written in a limited subset of Rust, allowing straightforward extension of the tool to new architectures and processor model using architecture and processor manuals. A novel technique of translating the descriptions to their verification analogues at compile-time enables fast verification using abstraction refinement without any need for formal verification knowledge by the description writer.