All Your Assembly Belongs to Rust: Automated Lifting for Uniform Testing and Verification
TL;DR
This paper translates Rust code containing RISC-V inline assembly into pure Rust code by emulating each instruction using a machine model extracted from the official RISC-V Sail ISA specification, and demonstrates how each category is handled by the translation.
Abstract
Inline assembly in systems software is often a source of challenges, a potential source of undefined behavior, and largely opaque to verification and bug-finding tools. The standard approach to verifying such code axiomatizes instruction semantics in the program logic, requiring custom models in the logic and specialized tooling. In this paper, we explore an alternative: to translate Rust code containing RISC-V inline assembly into pure Rust code by emulating each instruction using a machine model extracted from the official RISC-V Sail ISA specification. The resulting code can then be processed by standard Rust verification and testing tools: bounded model checkers (Kani), undefined-behavior detectors (Miri), and fuzzers, with no custom axiomatization of instruction semantics. We go over the different challenges raised by our approach: pure register operations, memory accesses, control flow, and system instructions, and show how each category is handled by the translation. We have applied this approach to verify inline assembly in two systems: Miralis, a RISC-V firmware hypervisor, and a dynamic root-of-trust firmware.
