Recent News
- 10/24: Paper on extended incorrectness logic is accepted at POPL’25.
- 07/24: Project FoxDec’s paper on verified x86-64 binary lifting is accepted at CCS’24.
- 06/24: Project libLISA’s paper on x86-64 instruction synthesis is accepted at OOPSLA’24.
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 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 are motivated in part by application settings where source codes are wholly or partially unavailable, outdated and decaying build processes and environments, third-party libraries and tools that are no longer available or backward 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 formalizing ISA semantics (as opposed to formalizing programming language semantics).
Ongoing thrusts include formalizing x86 semantics (Chum, libLISA), verifying memory corruption-related weird machines (Luce), sound decompilation (FoxDec), and verifying x86 disassemblers (DSV).