Recent News

  • 4/23: Paper on binary intermediate representation for formally verified decompilation is accepted at TAP’23.
  • 4/23: Paper on reachability analysis for low-level code is conditionally accepted at TAP’23.
  • 2/23: Our PhD student Joshua Bockenek successfully defended his PhD thesis! Josh’s thesis made contributions to projects Luce and FoxDec.
  • 9/22: Ghidra/P-Code formalization work has been accepted at VSTTE’22.
  • 5/22: Our PhD student Xiaoxin (Cindy) An successfully defended her PhD thesis! Cindy’s thesis made contributions to projects DSV and Renee.

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 (DSV), verifying ARMv8 binaries (Renee), proof-backed test case generation, and verifying concurrent x86-64 assembly code.