The Project

The LLRM project is exploring techniques for automated reasoning of program behaviors at lower levels of abstraction (e.g., binary, assembly, compiler intermediate representations) toward verifying program properties. A particular focus of interest is reasoning about, and verifying security properties including those related to memory corruption.

An overarching theme of the project is automated reasoning of low-level code that is enabled through formalization of instruction set architecture (ISA) semantics (e.g., x86, ARM), decompilation to higher abstraction levels, and prover-assisted reasoning and verification. Low-level reasoning and verification is motivated in part by application settings where source codes are wholly or partially unavailable, outdated and decaying build processes and environments, and third-party libraries and tools that are no longer available or backwards compatible, and the need to rapidly patch program errors, especially those that can cause security exploits. Motivation also includes relative reduction in trust bases (e.g., TCB excludes compilers, linkers, runtimes) and relative easiness in the formalization of ISA semantics (as opposed to formalizing programming language semantics).

Ongoing thrusts include formalizing x86 semantics in Isabelle (Chum), verifying memory corruption-related weird machines (Luce), sound decompilation (FoxDec), verifying x86 disassemblers, verifying ARMv8 binaries (Renee), proof-backed test case generation, and verifying concurrent x86-64 assembly code.