Ghidra + CBMC = Assembly Model Checker
Summary
The article presents ASMC, a tool that glues Ghidra's pcode semantics to CBMC to enable assembly model checking. It explains how ASMC lifts ELF binaries into CBMC's GOTO IR, demonstrates basic examples and ABI checks across architectures, and discusses translation validation and related tooling. The piece also candidly reflects on the approach's limitations and the author's stance on the project's longevity.