Renee: A Formal Methodology and Toolchain for Scalable Verification of Binary Code using Dependent Type Theory
Abstract
Renee: A Formal Methodology and Toolchain for Scalable Verification of Binary Code using Dependent Type TheoryWe propose to develop a veri?cation methodology and an associated toolchain, called Renee, for verifying systems software at the machine code level. At its core, the methodology involves developing a formal speci?cation language called the Renee Speci?cation Language (or RSL) inside a theorem-proving infrastructure, in particular, PVS. RSL will use dependent type theory, parametrized and generic nested theories, and reasoning libraries (e.g., bit-vector arithmetic, logical operators, logical and arithmetic shifts), whichenable the semantics of a machine s instruction-set-architecture (ISA) to be precisely captured. Renee will use a parser that translates a program binary into RSL using a formal decoder that leverages program symbolization techniques. Given the program s correctness specification, also expressed in RSL, the program s equivalence to the speci?cation is then established inside the theorem prover using automatic and interactive theoremproving. To prove the concept, we propose the ARM-v8 A64 ISA as the target machine architecture, whose semantics is formally speci?ed in the recently introduced ARM Specification Language (ASL). We propose to develop a parser that translates ASL into RSL using SAIL as an intermediate language. ASL-to-SAIL translators already exist; we therefore propose to develop a SAIL-to-RSL parser. A parser that translates ARM binaries into SAIL will also be developed, leveraging recently developed binary dis-assemblers such as Rambler and Uroboros. To reduce veri?cation costs and the trust base, we propose to auto-generate the parsers. The Renee methodology will be demonstrated by verifying real world systems software such as operating systems (e.g., rumpkernel), compiler components (e.g., LLVM code generator), or hypervisor subsystems (e.g., xenfs).
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Jul 26, 2018
- Source ID
- N000141812665
Entities
People
- Binoy Ravindran
Organizations
- Office of Naval Research
- United States Navy
- Virginia Tech