ASMC: Wiring Ghidra to CBMC for Assembly Model Checking

Researcher Philip Zucker has published ASMC, another attempt to splice assembly semantics recovered by Ghidra into the C Bounded Model Checker, CBMC. He describes CBMC as sitting nicely on the Pareto frontier of soundness, scalability, and pragmatism.

How it works

CBMC has its own intermediate representation, GOTO IR, and an object-file format, .gb. A component called asmc-lift takes a compiled ELF file and lifts it into a .gb file using Ghidra's p-code semantics as packaged by Trail of Bits (the sleigh library). ASMC itself is a driver that runs asmc-lift and the other CBMC tools. Because GOTO and p-code are fairly similar, the glue is small — roughly a thousand lines of C++.

The tight CBMC integration pays off because many questions about assembly are more naturally expressed in terms of C-level concepts. Hence the breadth of use cases: standalone assembly verification, translation validation, linking against external assembly, C specs for assembly, DWARF debug-data verification, and decompilation verification.

Examples

In the simplest case a function moves 42 into rax, and ASMC confirms that value is returned; a postcondition of outreg.rax == 43 duly fails with a counterexample. The tool also catches ABI violations — clobbering the stack return address, or failing to restore the callee-saved register R12. Both x86-64 and RV32/64 are supported; adding one of the 20-plus architectures Ghidra knows mostly means writing a new ABI shim in C.

An honest afterword

Zucker is candid: the new tool is heavily AI-produced from his notes and directions. He says he is proficient in neither C++ nor CBMC's internals and would not have attempted this unless it became easy. Over seven years he has written five such prototypes — a sixth, by hand, no longer excited him.

His mood is bittersweet. He has always treated binary verification as a sensible compromise between what interests him and what society needs, and he has torn plenty of hair out over it. Yet it is a little sad to watch AI knock out the work so quickly. He wonders whether last year's agentic-AI boom has shifted the acceptable bar for soundness so far that anything less is now defunct. He has no firm answer: it depends on what is in the pipeline, and what he has seen publicly so far does not support that conclusion.

Source: Lobsters