The article introduces ASMC (Assembly Model Checker), a tool that integrates Ghidra's PCode semantics with CBMC (C Bounded Model Checker) to enable formal verification of assembly code. The tool lifts .elf files into CBMC's .gb format using SLEIGH, with only ~1kLOC of glue C++ code, supporting use cases like standalone assembly verification, translation validation, and decompilation verification.
Background
CBMC is an open-source bounded model checker for C and C++, widely used in software verification. Ghidra's SLEIGH disassembler framework enables programmatic access to decompiled semantics via PCode intermediate representation.
- Source
- Lobsters
- Published
- Oct 19, 2026 at 12:58 AM
- Score
- 6.0 / 10