Welcome to LLRM project website!

The Low-Level Reasoning Machine (LLRM) project is exploring techniques for automated reasoning of program behaviors at lower levels of abstraction (e.g., binary, assembly, machine-independent intermediate representations) to verify program properties. A particular focus of interest is reasoning about and verifying security properties.

Control flow graph (snippet) automatically lifted from the ssh/OpenSSH binary by the FoxDec verified decompiler.

An overarching theme of the project is the automated reasoning of low-level code, enabled through the formalization of instruction set architecture (ISA) semantics (e.g., x86-64, 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 a relative reduction in trust bases (e.g., TCB excludes compilers, linkers, and runtimes) and a relative ease in formalizing ISA semantics (as opposed to formalizing programming language semantics).

Ongoing thrusts include formalizing x86 semantics (Chum, libLISA), verified decompilation (FoxDec), verifying memory corruption-related weird machines (Luce), verifying x86 disassemblers (DSV), and formalizing ARMv8 semantics and verifying ARMv8 binaries (Renee).