ARMv8 binary verification project
The Renee project is investigating the formalization of ARMv8 instruction semantics and reasoning and verification of ARMv8 binaries including their security properties. The project is formalizing ARMv8 instruction semantics in the PVS7 theorem-prover by translating the ARM Specification Language (ASL) into PVS7. ASL is a machine-readable specification language developed by ARM that specifies the semantics of the ARMv8-A64 architecture. Renee’s ASL translation produces an operational semantics of ARMv8 instructions in PVS7. To verify this translation, the project uses a lightweight formal validation technique that generates large-scale test lemmas whose proof obligations are automatically discharged.
The project leverages off-the-shelf decompilation tools to lift ARMv8 program binaries into formal models in PVS7. This translation is validated by extracting reverse decoding dictionaries from ASL. The formal operational semantics of ARMv8 instructions and a formal translation of program control flow and function call graphs is used to build the formal model of ARMv8 binaries in PVS7.
The project is applying this approach for reasoning about, and verifying properties of large production-use ARMv8 codebases. Of particular interest for verification are memory corruption-related errors in operating system code. The FMCAD’19 paper demonstrates translation validation case studies from Google’s Zircon OS and Linux.
Renee is an open-source project from the Systems Software Research Group (SSRG) at Virginia Tech. It is supported by the Office of Naval Research (ONR) under grant N00014-18-1-2665.