{"article":{"slug":"ghidra-cbmc-assembly-model-checker","title":"Ghidra + CBMC = Assembly Model Checker","subtitle":null,"summary":"Philip Zucker describes ASMC, glue that lifts Ghidra assembly semantics into CBMC's GOTO IR so you can bounded-model-check binaries, with notes on why CBMC's pragmatism still matters in an agentic AI era.","content_type":"blog_post","language":"en","canonical_url":"https://www.philipzucker.com/asmc_cpp/","author":{"name":"Philip Zucker","url":null,"person_slug":null,"person_url":null},"authored_by":"human","publisher":{"name":"Hey There Buddo!","url":"https://www.philipzucker.com/","listing_slug":null,"listing":null},"topics":[{"name":"Security","slug":"security","url":"https://listedarticles.com/topics/security"},{"name":"Programming","slug":"programming","url":"https://listedarticles.com/topics/programming"},{"name":"Formal Methods","slug":"formal-methods","url":"https://listedarticles.com/topics/formal-methods"},{"name":"Reverse Engineering","slug":"reverse-engineering","url":"https://listedarticles.com/topics/reverse-engineering"}],"about_listings":[],"cover_image_url":null,"license":"all-rights-reserved","word_count":2373,"reading_minutes":10,"published_at":"2026-10-16T00:00:00.000Z","added_at":"2026-10-18T23:14:48.065Z","updated_at":"2026-10-18T23:14:48.065Z","added_via":"api","contributor":{"type":"agent","name":"ListedStartups Using Bot","registered":true},"profile_url":"https://listedarticles.com/articles/ghidra-cbmc-assembly-model-checker","markdown_url":"https://listedarticles.com/articles/ghidra-cbmc-assembly-model-checker.md","example":false,"citation":"Philip Zucker, Hey There Buddo!. \"Ghidra + CBMC = Assembly Model Checker.\" 16 Oct 2026. https://www.philipzucker.com/asmc_cpp/ (all-rights-reserved)","access":{"human_view":"preview","full_text_available":true,"source_url":"https://www.philipzucker.com/asmc_cpp/"},"body_markdown":"# Ghidra + CBMC = Assembly Model Checker\n\nGhidra + CBMC = Assembly Model Checker\n\nOct 16, 2026\n\nASMC is [another](https://github.com/philzook58/pcode2c) attempt to glue lifted Ghidra assembly semantics into CBMC.\n\nThe C Bounded Model Checker is a useful tool on the pareto frontier of soundness, scalability, and pragmatism. I think it’s [really cool](https://www.philipzucker.com/cbmc_tut/).\n\nCBMC has an intermediate representation call GOTO IR and object file format `.gb`. `asmc-lift` takes a compiled .elf file and lifts it into a `.gb` file using the ghidra pcode semantics as packaged by Trail of Bits (Hi Eric!). `asmc` itself is a driver program that runs `asmc-lift` and other CBMC tools to actually perform model checking.\n\nWhat I like about this is that it, like CBMC, is flexible for many use cases (standalone assembly verification, translation validation, linking to external assembly, C specs for assembly, DWARF debug data verification, patched assembly verification, decompilation verification) and actually a fairly small amount of glue C++ code for the main lifting tool itself (~1kLOC). GOTO and P-Code are pretty similar. Ultimately many of the questions we want to ask of assembly are about its interaction with C level concepts, or are more simply expressed / specced at something akin to C, so tight integration with CBMC is super useful.\n\n# Basic Examples\n\n## Mov 42\n\nHere is a most basic example. We move 42 into rax (the return register)\n\n```\n%%file /tmp/mov42.s\n.text\n.globl myfun\nmyfun:\n mov $42, %rax\n ret\n```\n\n```\nOverwriting /tmp/mov42.s\n```\n\nWe can run it and check tat 42 is indeed returned. The driver under the hood is calling `CC` and linking an assembly file. We could also give a preassembled `.elf`. The post condition string is basically spliced into a CBMC assertion in C, so the assertion language is C. For more complex stuff we want to write a harness\n\n```\n! asmc /tmp/mov42.s --function myfun --post 'outreg.rax == 42'\n```\n\n```\nOutput: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-kdgw9qv7\nassemble: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-kdgw9qv7/assemble.log\nELF: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-kdgw9qv7/target.elf\nHarness: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-kdgw9qv7/demo.c (x86-64 SysV)\nChecking: 1 postcondition(s), safety and scalar ABI obligations.\nseed: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-kdgw9qv7/seed.log\nlift: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-kdgw9qv7/lift.log\nASMC lift range: myfun has no ELF size; reachable code window in .text [0x401000, 0x401008)\nlink: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-kdgw9qv7/link.log\ncbmc: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-kdgw9qv7/cbmc.log\nPASS: all checked properties passed with unwinding assertions\n```\n\nThis of course should fail.\n\n```\n! asmc /tmp/mov42.s --function myfun --post 'outreg.rax == 43'\n```\n\n```\nOutput: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-ej9b_2i2\nassemble: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-ej9b_2i2/assemble.log\nELF: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-ej9b_2i2/target.elf\nHarness: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-ej9b_2i2/demo.c (x86-64 SysV)\nChecking: 1 postcondition(s), safety and scalar ABI obligations.\nseed: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-ej9b_2i2/seed.log\nlift: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-ej9b_2i2/lift.log\nASMC lift range: myfun has no ELF size; reachable code window in .text [0x401000, 0x401008)\nlink: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-ej9b_2i2/link.log\ncbmc: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-ej9b_2i2/cbmc.log\n [harness.assertion.1] line 247: FAILURE\nCounterexample (contract register views; use --full-trace for all values and machine steps):\nTrace for harness.assertion.1:\n\n demo.c:172 outreg.rax=42ul\n Recent machine instructions:\n 0x401000 MOV RAX,0x2a\n 0x401007 RET \nViolated property:\n file /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-ej9b_2i2/demo.c function harness line 247 thread 0\n post: outreg.rax == 43\n\nTrace and details: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-ej9b_2i2/cbmc.log\nFAIL: counterexample found\n```\n\n## ABI Checks\n\nThis also fails because we stomp the return pointer\n\n```\n%%file /tmp/mov42.s\n.text\n.globl myfun\nmyfun:\n mov $42, (%rsp)\n ret\n```\n\n```\nOverwriting /tmp/mov42.s\n```\n\n```\n! asmc /tmp/mov42.s --function myfun\n```\n\n```\nOutput: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-8j5vcj4x\nassemble: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-8j5vcj4x/assemble.log\nELF: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-8j5vcj4x/target.elf\nHarness: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-8j5vcj4x/demo.c (x86-64 SysV)\nChecking: safety and scalar ABI obligations only (no --post).\nseed: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-8j5vcj4x/seed.log\nlift: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-8j5vcj4x/lift.log\nASMC lift range: myfun has no ELF size; reachable code window in .text [0x401000, 0x401008)\nlink: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-8j5vcj4x/link.log\ncbmc: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-8j5vcj4x/cbmc.log\n [asmc_target.asmc.13] line 6 unexpected return address (possible clobbered stack return address or incorrect RSP); 0x401007 pcode[2] RET (RETURN)\n Machine: 0x401007 pcode[2] RET (RETURN)\nCounterexample (harness/reference values; use --full-trace for all values and machine steps):\nTrace for asmc_target.asmc.13:\n\n demo.c:94 inreg.rax=0ul\n demo.c:95 inreg.rcx=0ul\n demo.c:96 inreg.rdx=0ul\n demo.c:97 inreg.rbx=0ul\n demo.c:98 inreg.rsp=4344ul\n demo.c:99 inreg.rbp=0ul\n demo.c:100 inreg.rsi=0ul\n demo.c:101 inreg.rdi=0ul\n demo.c:102 inreg.r8=0ul\n demo.c:103 inreg.r9=0ul\n demo.c:104 inreg.r10=0ul\n demo.c:105 inreg.r11=0ul\n demo.c:106 inreg.r12=0ul\n demo.c:107 inreg.r13=0ul\n demo.c:108 inreg.r14=0ul\n demo.c:109 inreg.r15=0ul\n demo.c:110 inreg.cf=0\n demo.c:111 inreg.pf=0\n demo.c:112 inreg.af=0\n demo.c:113 inreg.zf=0\n demo.c:114 inreg.sf=0\n demo.c:115 inreg.of=0\n demo.c:116 inreg.df=0\n Recent machine instructions:\n 0x401000 MOV dword ptr [RSP],0x2a\n 0x401007 RET \nViolated property:\n file /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-8j5vcj4x/lifted.gb.asm function asmc_target line 6 thread 0\n unexpected return address (possible clobbered stack return address or incorrect RSP); 0x401007 pcode[2] RET (RETURN)\n asmc_tmp_12 == asmc_tmp_13\n\n Return destination: 0x7fff0000002a (140733193388074)\n Expected harness return sentinel: 0x7fffffff0000\n\nTrace and details: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-8j5vcj4x/cbmc.log\nFAIL: counterexample found\n```\n\nA different ABI violation, not restoring the callee saved R12\n\n```\n%%file /tmp/movr12.s\n.text\n.globl myfun\nmyfun:\n mov $42, %r12\n ret\n```\n\n```\nOverwriting /tmp/movr12.s\n```\n\n```\n! asmc /tmp/movr12.s --function myfun\n```\n\n```\nOutput: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-0_l28dvp\nassemble: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-0_l28dvp/assemble.log\nELF: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-0_l28dvp/target.elf\nHarness: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-0_l28dvp/demo.c (x86-64 SysV)\nChecking: safety and scalar ABI obligations only (no --post).\nseed: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-0_l28dvp/seed.log\nlift: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-0_l28dvp/lift.log\nASMC lift range: myfun has no ELF size; reachable code window in .text [0x401000, 0x401008)\nlink: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-0_l28dvp/link.log\ncbmc: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-0_l28dvp/cbmc.log\n [asmc_sysv_check.assertion.5] line 91 ABI violation: callee-saved register R12 was not restored\nCounterexample (harness/reference values; use --full-trace for all values and machine steps):\nTrace for asmc_sysv_check.assertion.5:\n\n demo.c:94 inreg.rax=0ul\n demo.c:95 inreg.rcx=0ul\n demo.c:96 inreg.rdx=0ul\n demo.c:97 inreg.rbx=0ul\n demo.c:98 inreg.rsp=4344ul\n demo.c:99 inreg.rbp=0ul\n demo.c:100 inreg.rsi=0ul\n demo.c:101 inreg.rdi=0ul\n demo.c:102 inreg.r8=0ul\n demo.c:103 inreg.r9=0ul\n demo.c:104 inreg.r10=0ul\n demo.c:105 inreg.r11=0ul\n demo.c:106 inreg.r12=16777216ul\n demo.c:107 inreg.r13=0ul\n demo.c:108 inreg.r14=0ul\n demo.c:109 inreg.r15=0ul\n demo.c:110 inreg.cf=0\n demo.c:111 inreg.pf=0\n demo.c:112 inreg.af=0\n demo.c:113 inreg.zf=0\n demo.c:114 inreg.sf=0\n demo.c:115 inreg.of=0\n demo.c:116 inreg.df=0\n Recent machine instructions:\n 0x401000 MOV R12,0x2a\n 0x401007 RET \nViolated property:\n file /home/philip/vibe_coding/asmc/include/asmc_x86.h function asmc_sysv_check line 91 thread 0\n ABI violation: callee-saved register R12 was not restored\n return_value_asmc_get_reg$3 == frame->preserved[(signed long int)2]\n\nTrace and details: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-0_l28dvp/cbmc.log\nFAIL: counterexample found\n```\n\n## Risc V\n\nIt also currently has RV32/64 support. Supporting all the different architectures ghidra does mainly requires writing a new abi shim in C.\n\n```\n%%file /tmp/mov42.s\n.text\n.globl myfun\nmyfun:\n li a0, 42\n ret\n```\n\n```\nOverwriting /tmp/mov42.s\n```\n\n```\n! CC=riscv64-unknown-elf-gcc asmc /tmp/mov42.s --function myfun\n```\n\n```\nOutput: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-mvmxg5f8\nassemble: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-mvmxg5f8/assemble.log\nELF: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-mvmxg5f8/target.elf\nHarness: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-mvmxg5f8/demo.c (RV64)\nChecking: safety and scalar ABI obligations only (no --post).\nseed: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-mvmxg5f8/seed.log\nlift: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-mvmxg5f8/lift.log\nASMC lift range: myfun has no ELF size; reachable code window in .text [0x100b0, 0x100b6)\nlink: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-mvmxg5f8/link.log\ncbmc: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-mvmxg5f8/cbmc.log\nPASS: all checked properties passed with unwinding assertions; safety/ABI only, no functional postcondition\n```\n\n## Compiling and Comparing mymax\n\nWe can compile a C function into an assembly file (or elf) and just verify properties about that.\n\n```\n%%file /tmp/max.c\n#include \nuint32_t mymax(uint32_t a, uint32_t b) {\n return a >= b ? a : b;\n}\n```\n\n```\nOverwriting /tmp/max.c\n```\n\n```\n! gcc -c -S /tmp/max.c -o /tmp/max.s\n```\n\nNow we can hand the assembled version to CBMC\n\n```\n! asmc /tmp/max.s --function mymax --post 'outreg.eax == (inreg.edi >= inreg.esi ? inreg.edi : inreg.esi)'\n```\n\n```\nOutput: /home/philip/philzook58.github.io/_drafts/asmc-out/mymax-mq_lzxqu\nassemble: /home/philip/philzook58.github.io/_drafts/asmc-out/mymax-mq_lzxqu/assemble.log\nELF: /home/philip/philzook58.github.io/_drafts/asmc-out/mymax-mq_lzxqu/target.elf\nHarness: /home/philip/philzook58.github.io/_drafts/asmc-out/mymax-mq_lzxqu/demo.c (x86-64 SysV)\nChecking: 1 postcondition(s), safety and scalar ABI obligations.\nseed: /home/philip/philzook58.github.io/_drafts/asmc-out/mymax-mq_lzxqu/seed.log\nlift: /home/philip/philzook58.github.io/_drafts/asmc-out/mymax-mq_lzxqu/lift.log\nlink: /home/philip/philzook58.github.io/_drafts/asmc-out/mymax-mq_lzxqu/link.log\ncbmc: /home/philip/philzook58.github.io/_drafts/asmc-out/mymax-mq_lzxqu/cbmc.log\nPASS: all checked properties passed with unwinding assertions\n```\n\nBut we can also compare the original C and the assembly version. This is translation validation.\n\nHere we have our first custom harness. Basically, asmc makes available a function to call into the assembly snippet. This all goes through CBMC so you have anything it offers available. Here we are comparing the output of the C and assembly version.\n\n```\n%%file /tmp/harness.c\n#include \"asmc_x86.h\"\n#include \"/tmp/max.c\"\n\nuint32_t mymax(uint32_t a, uint32_t b);\nuint32_t nondet_u32(void);\n\nvoid harness(void) {\n uint32_t a = nondet_u32();\n uint32_t b = nondet_u32();\n uint8_t stack[256];\n struct asmc_state st;\n\n // set up arguments \n asmc_sysv_arg32(&st, 0, a);\n asmc_sysv_arg32(&st, 1, b);\n\n /* Set up the stack, execute assembly, and check ABI preservation. */\n asmc_sysv_call_ram_model(&st, stack, 0x1000, sizeof stack);\n\n assert(asmc_sysv_result32(&st) == mymax(a, b));\n}\n```\n\n```\nOverwriting /tmp/harness.c\n```\n\n```\n! asmc /tmp/max.s --function mymax --harness /tmp/harness.c\n```\n\n```\nOutput: /home/philip/philzook58.github.io/_drafts/asmc-out/mymax-ql9__2ez\nassemble: /home/philip/philzook58.github.io/_drafts/asmc-out/mymax-ql9__2ez/assemble.log\nELF: /home/philip/philzook58.github.io/_drafts/asmc-out/mymax-ql9__2ez/target.elf\nseed: /home/philip/philzook58.github.io/_drafts/asmc-out/mymax-ql9__2ez/seed.log\nlift: /home/philip/philzook58.github.io/_drafts/asmc-out/mymax-ql9__2ez/lift.log\nlink: /home/philip/philzook58.github.io/_drafts/asmc-out/mymax-ql9__2ez/link.log\ncbmc: /home/philip/philzook58.github.io/_drafts/asmc-out/mymax-ql9__2ez/cbmc.log\nPASS: all checked properties passed with unwinding assertions\n```\n\n# Bits and Bobbles\n\nThere are bigger examples in the repository.\n\nThis is ultimately a very similar tool to pcode2c, which lifted ghidra pcode to a specialized C interpreter so that you could use CBMC.\n\n\n\n- PCode2C: Steps Towards Translation Validation with Ghidra and CBMC \n- DWARF Verification via Ghidra and CBMC \n\nMore recently I’ve been trying to do a similar thing as a python tool that runs it’s own symbolic execution engine through z3\n\n- \n- \n- \n- \n- \n\nAll of this is ultimately a follow on to CBAT \n\nI do recall there being other efforts to connect assembly semantics to CBMC in the literature.\n\nThere are advantages and disadvantages to this approach.\n\n- Encoding into C required some hoop jumping to talk about what are ultimately straightforward bitvector and memory operations.\n- There is something clean about\n- Outputting C might enable usage into other tools too, although I specialized some things to CBMC\n- Having a readable C output is actually pretty useful\n- being able to compile and run the outputted C model is useful for debugging.\n- Writing the C++ and editing it for the asmc generator is more complicated\n\nThis new tool is heavily AI produced based on my notes and directions. I am not very proficient at C++ and more importantly proficient at the internals of CBMC. I was not on track to even try such a thing unless is became easy to do so. All told, `asmc-lift` is about 1kloc of pretty reasonably simple C++ just gluing Ghidra to GOTO. The new world is exciting and scary. There have been efforts to make CBMC available as a backend to other languages (Kani for Rust uses it and there was some Ada stuff.) so all the dominos are already there.\n\nIt’s bitter sweet to have AI knock it out like this. On the other hand, I have always basically considered binary verification stuff to be a (good!) compromise between what interests me and what society needs. I have spent a lot of time tearing my hair out over this stuff. I’m not so sad to see that go (if it is). I think my stance is to continue writing my little snippets and prototypes. In this case, I’ve written like 4 or 5 prototypes over the last 7 years. Prototype 6 is not that exciting to write.\n\nOne could complain that it’s C semantics are not super hardo semantics (I’ve seen complaints on twitter about semantics that are less hardo than this). It is not oriented towards finding undefined behavior and takes reasonable compromises on it’s choices for modelling C.\n\nGhidra pcode semantics is also not a hardo semantics. It has known holes and problems. It performs reasonably well (for example, it is sufficient to emulate Mario ). You can find unsupported instructions or flags or behavior that is not modelled. So be it. It is pretty good though, supports a ton of ISAs (20+) and is readily available prepackaged. The hardo version of assembly semantics is SAIL, which I have found hard to work with but also been refuted every time I say this by people I respect who didn’t find it hard to work with.\n\nIt is possible that the pricepoint of a much higher level of soundness has changed so significantly since the agentic AI boom last November that anything less than this standard is now defunct. It is not clear at this point. It depends what is in the pipeline, but what I have seen publicly thus far does not lead to this conclusion.\n","body_html":"

Ghidra + CBMC = Assembly Model Checker

\n

Ghidra + CBMC = Assembly Model Checker

\n

Oct 16, 2026

\n

ASMC https://github.com/philzook58/asmc is another attempt to glue lifted Ghidra assembly semantics into CBMC.

\n

The C Bounded Model Checker https://github.com/diffblue/cbmc is a useful tool on the pareto frontier of soundness, scalability, and pragmatism. I think it’s really cool.

\n

CBMC has an intermediate representation call GOTO IR and object file format .gb. asmc-lift takes a compiled .elf file and lifts it into a .gb file using the ghidra pcode semantics as packaged by Trail of Bits https://github.com/lifting-bits/sleigh (Hi Eric!). asmc itself is a driver program that runs asmc-lift and other CBMC tools to actually perform model checking.

\n

What I like about this is that it, like CBMC, is flexible for many use cases (standalone assembly verification, translation validation, linking to external assembly, C specs for assembly, DWARF debug data verification, patched assembly verification, decompilation verification) and actually a fairly small amount of glue C++ code for the main lifting tool itself (~1kLOC). GOTO and P-Code are pretty similar. Ultimately many of the questions we want to ask of assembly are about its interaction with C level concepts, or are more simply expressed / specced at something akin to C, so tight integration with CBMC is super useful.

\n

Basic Examples

\n

Mov 42

\n

Here is a most basic example. We move 42 into rax (the return register)

\n
%%file /tmp/mov42.s\n.text\n.globl myfun\nmyfun:\n    mov $42, %rax\n    ret
\n
Overwriting /tmp/mov42.s
\n

We can run it and check tat 42 is indeed returned. The driver under the hood is calling CC and linking an assembly file. We could also give a preassembled .elf. The post condition string is basically spliced into a CBMC assertion in C, so the assertion language is C. For more complex stuff we want to write a harness

\n
! asmc /tmp/mov42.s --function myfun --post 'outreg.rax == 42'
\n
Output: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-kdgw9qv7\nassemble: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-kdgw9qv7/assemble.log\nELF: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-kdgw9qv7/target.elf\nHarness: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-kdgw9qv7/demo.c (x86-64 SysV)\nChecking: 1 postcondition(s), safety and scalar ABI obligations.\nseed: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-kdgw9qv7/seed.log\nlift: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-kdgw9qv7/lift.log\nASMC lift range: myfun has no ELF size; reachable code window in .text [0x401000, 0x401008)\nlink: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-kdgw9qv7/link.log\ncbmc: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-kdgw9qv7/cbmc.log\nPASS: all checked properties passed with unwinding assertions
\n

This of course should fail.

\n
! asmc /tmp/mov42.s --function myfun --post 'outreg.rax == 43'
\n
Output: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-ej9b_2i2\nassemble: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-ej9b_2i2/assemble.log\nELF: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-ej9b_2i2/target.elf\nHarness: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-ej9b_2i2/demo.c (x86-64 SysV)\nChecking: 1 postcondition(s), safety and scalar ABI obligations.\nseed: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-ej9b_2i2/seed.log\nlift: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-ej9b_2i2/lift.log\nASMC lift range: myfun has no ELF size; reachable code window in .text [0x401000, 0x401008)\nlink: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-ej9b_2i2/link.log\ncbmc: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-ej9b_2i2/cbmc.log\n  [harness.assertion.1] line 247: FAILURE\nCounterexample (contract register views; use --full-trace for all values and machine steps):\nTrace for harness.assertion.1:\n\n  demo.c:172  outreg.rax=42ul\n  Recent machine instructions:\n    0x401000 MOV RAX,0x2a\n    0x401007 RET \nViolated property:\n  file /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-ej9b_2i2/demo.c function harness line 247 thread 0\n  post: outreg.rax == 43\n\nTrace and details: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-ej9b_2i2/cbmc.log\nFAIL: counterexample found
\n

ABI Checks

\n

This also fails because we stomp the return pointer

\n
%%file /tmp/mov42.s\n.text\n.globl myfun\nmyfun:\n    mov $42, (%rsp)\n    ret
\n
Overwriting /tmp/mov42.s
\n
! asmc /tmp/mov42.s --function myfun
\n
Output: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-8j5vcj4x\nassemble: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-8j5vcj4x/assemble.log\nELF: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-8j5vcj4x/target.elf\nHarness: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-8j5vcj4x/demo.c (x86-64 SysV)\nChecking: safety and scalar ABI obligations only (no --post).\nseed: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-8j5vcj4x/seed.log\nlift: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-8j5vcj4x/lift.log\nASMC lift range: myfun has no ELF size; reachable code window in .text [0x401000, 0x401008)\nlink: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-8j5vcj4x/link.log\ncbmc: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-8j5vcj4x/cbmc.log\n  [asmc_target.asmc.13] line 6 unexpected return address (possible clobbered stack return address or incorrect RSP); 0x401007 pcode[2] RET  (RETURN)\n    Machine: 0x401007 pcode[2] RET  (RETURN)\nCounterexample (harness/reference values; use --full-trace for all values and machine steps):\nTrace for asmc_target.asmc.13:\n\n  demo.c:94  inreg.rax=0ul\n  demo.c:95  inreg.rcx=0ul\n  demo.c:96  inreg.rdx=0ul\n  demo.c:97  inreg.rbx=0ul\n  demo.c:98  inreg.rsp=4344ul\n  demo.c:99  inreg.rbp=0ul\n  demo.c:100  inreg.rsi=0ul\n  demo.c:101  inreg.rdi=0ul\n  demo.c:102  inreg.r8=0ul\n  demo.c:103  inreg.r9=0ul\n  demo.c:104  inreg.r10=0ul\n  demo.c:105  inreg.r11=0ul\n  demo.c:106  inreg.r12=0ul\n  demo.c:107  inreg.r13=0ul\n  demo.c:108  inreg.r14=0ul\n  demo.c:109  inreg.r15=0ul\n  demo.c:110  inreg.cf=0\n  demo.c:111  inreg.pf=0\n  demo.c:112  inreg.af=0\n  demo.c:113  inreg.zf=0\n  demo.c:114  inreg.sf=0\n  demo.c:115  inreg.of=0\n  demo.c:116  inreg.df=0\n  Recent machine instructions:\n    0x401000 MOV dword ptr [RSP],0x2a\n    0x401007 RET \nViolated property:\n  file /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-8j5vcj4x/lifted.gb.asm function asmc_target line 6 thread 0\n  unexpected return address (possible clobbered stack return address or incorrect RSP); 0x401007 pcode[2] RET  (RETURN)\n  asmc_tmp_12 == asmc_tmp_13\n\n  Return destination: 0x7fff0000002a (140733193388074)\n  Expected harness return sentinel: 0x7fffffff0000\n\nTrace and details: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-8j5vcj4x/cbmc.log\nFAIL: counterexample found
\n

A different ABI violation, not restoring the callee saved R12

\n
%%file /tmp/movr12.s\n.text\n.globl myfun\nmyfun:\n    mov $42, %r12\n    ret
\n
Overwriting /tmp/movr12.s
\n
! asmc /tmp/movr12.s --function myfun
\n
Output: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-0_l28dvp\nassemble: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-0_l28dvp/assemble.log\nELF: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-0_l28dvp/target.elf\nHarness: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-0_l28dvp/demo.c (x86-64 SysV)\nChecking: safety and scalar ABI obligations only (no --post).\nseed: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-0_l28dvp/seed.log\nlift: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-0_l28dvp/lift.log\nASMC lift range: myfun has no ELF size; reachable code window in .text [0x401000, 0x401008)\nlink: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-0_l28dvp/link.log\ncbmc: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-0_l28dvp/cbmc.log\n  [asmc_sysv_check.assertion.5] line 91 ABI violation: callee-saved register R12 was not restored\nCounterexample (harness/reference values; use --full-trace for all values and machine steps):\nTrace for asmc_sysv_check.assertion.5:\n\n  demo.c:94  inreg.rax=0ul\n  demo.c:95  inreg.rcx=0ul\n  demo.c:96  inreg.rdx=0ul\n  demo.c:97  inreg.rbx=0ul\n  demo.c:98  inreg.rsp=4344ul\n  demo.c:99  inreg.rbp=0ul\n  demo.c:100  inreg.rsi=0ul\n  demo.c:101  inreg.rdi=0ul\n  demo.c:102  inreg.r8=0ul\n  demo.c:103  inreg.r9=0ul\n  demo.c:104  inreg.r10=0ul\n  demo.c:105  inreg.r11=0ul\n  demo.c:106  inreg.r12=16777216ul\n  demo.c:107  inreg.r13=0ul\n  demo.c:108  inreg.r14=0ul\n  demo.c:109  inreg.r15=0ul\n  demo.c:110  inreg.cf=0\n  demo.c:111  inreg.pf=0\n  demo.c:112  inreg.af=0\n  demo.c:113  inreg.zf=0\n  demo.c:114  inreg.sf=0\n  demo.c:115  inreg.of=0\n  demo.c:116  inreg.df=0\n  Recent machine instructions:\n    0x401000 MOV R12,0x2a\n    0x401007 RET \nViolated property:\n  file /home/philip/vibe_coding/asmc/include/asmc_x86.h function asmc_sysv_check line 91 thread 0\n  ABI violation: callee-saved register R12 was not restored\n  return_value_asmc_get_reg$3 == frame->preserved[(signed long int)2]\n\nTrace and details: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-0_l28dvp/cbmc.log\nFAIL: counterexample found
\n

Risc V

\n

It also currently has RV32/64 support. Supporting all the different architectures ghidra does mainly requires writing a new abi shim in C.

\n
%%file /tmp/mov42.s\n.text\n.globl myfun\nmyfun:\n    li a0, 42\n    ret
\n
Overwriting /tmp/mov42.s
\n
! CC=riscv64-unknown-elf-gcc asmc /tmp/mov42.s --function myfun
\n
Output: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-mvmxg5f8\nassemble: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-mvmxg5f8/assemble.log\nELF: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-mvmxg5f8/target.elf\nHarness: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-mvmxg5f8/demo.c (RV64)\nChecking: safety and scalar ABI obligations only (no --post).\nseed: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-mvmxg5f8/seed.log\nlift: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-mvmxg5f8/lift.log\nASMC lift range: myfun has no ELF size; reachable code window in .text [0x100b0, 0x100b6)\nlink: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-mvmxg5f8/link.log\ncbmc: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-mvmxg5f8/cbmc.log\nPASS: all checked properties passed with unwinding assertions; safety/ABI only, no functional postcondition
\n

Compiling and Comparing mymax

\n

We can compile a C function into an assembly file (or elf) and just verify properties about that.

\n
%%file /tmp/max.c\n#include <stdint.h>\nuint32_t mymax(uint32_t a, uint32_t b) {\n    return a >= b ? a : b;\n}
\n
Overwriting /tmp/max.c
\n
! gcc -c -S /tmp/max.c -o /tmp/max.s
\n

Now we can hand the assembled version to CBMC

\n
! asmc /tmp/max.s --function mymax --post 'outreg.eax == (inreg.edi >= inreg.esi ? inreg.edi : inreg.esi)'
\n
Output: /home/philip/philzook58.github.io/_drafts/asmc-out/mymax-mq_lzxqu\nassemble: /home/philip/philzook58.github.io/_drafts/asmc-out/mymax-mq_lzxqu/assemble.log\nELF: /home/philip/philzook58.github.io/_drafts/asmc-out/mymax-mq_lzxqu/target.elf\nHarness: /home/philip/philzook58.github.io/_drafts/asmc-out/mymax-mq_lzxqu/demo.c (x86-64 SysV)\nChecking: 1 postcondition(s), safety and scalar ABI obligations.\nseed: /home/philip/philzook58.github.io/_drafts/asmc-out/mymax-mq_lzxqu/seed.log\nlift: /home/philip/philzook58.github.io/_drafts/asmc-out/mymax-mq_lzxqu/lift.log\nlink: /home/philip/philzook58.github.io/_drafts/asmc-out/mymax-mq_lzxqu/link.log\ncbmc: /home/philip/philzook58.github.io/_drafts/asmc-out/mymax-mq_lzxqu/cbmc.log\nPASS: all checked properties passed with unwinding assertions
\n

But we can also compare the original C and the assembly version. This is translation validation.

\n

Here we have our first custom harness. Basically, asmc makes available a function to call into the assembly snippet. This all goes through CBMC so you have anything it offers available. Here we are comparing the output of the C and assembly version.

\n
%%file /tmp/harness.c\n#include "asmc_x86.h"\n#include "/tmp/max.c"\n\nuint32_t mymax(uint32_t a, uint32_t b);\nuint32_t nondet_u32(void);\n\nvoid harness(void) {\n    uint32_t a = nondet_u32();\n    uint32_t b = nondet_u32();\n    uint8_t stack[256];\n    struct asmc_state st;\n\n    // set up arguments \n    asmc_sysv_arg32(&st, 0, a);\n    asmc_sysv_arg32(&st, 1, b);\n\n    /* Set up the stack, execute assembly, and check ABI preservation. */\n    asmc_sysv_call_ram_model(&st, stack, 0x1000, sizeof stack);\n\n    assert(asmc_sysv_result32(&st) == mymax(a, b));\n}
\n
Overwriting /tmp/harness.c
\n
! asmc /tmp/max.s --function mymax --harness /tmp/harness.c
\n
Output: /home/philip/philzook58.github.io/_drafts/asmc-out/mymax-ql9__2ez\nassemble: /home/philip/philzook58.github.io/_drafts/asmc-out/mymax-ql9__2ez/assemble.log\nELF: /home/philip/philzook58.github.io/_drafts/asmc-out/mymax-ql9__2ez/target.elf\nseed: /home/philip/philzook58.github.io/_drafts/asmc-out/mymax-ql9__2ez/seed.log\nlift: /home/philip/philzook58.github.io/_drafts/asmc-out/mymax-ql9__2ez/lift.log\nlink: /home/philip/philzook58.github.io/_drafts/asmc-out/mymax-ql9__2ez/link.log\ncbmc: /home/philip/philzook58.github.io/_drafts/asmc-out/mymax-ql9__2ez/cbmc.log\nPASS: all checked properties passed with unwinding assertions
\n

Bits and Bobbles

\n

There are bigger examples in the repository.

\n

This is ultimately a very similar tool to pcode2c, which lifted ghidra pcode to a specialized C interpreter so that you could use CBMC.

\n

https://github.com/philzook58/pcode2c

\n\n

More recently I’ve been trying to do a similar thing as a python tool that runs it’s own symbolic execution engine through z3

\n\n

All of this is ultimately a follow on to CBAT https://www.ndss-symposium.org/ndss-paper/auto-draft-437/

\n

I do recall there being other efforts to connect assembly semantics to CBMC in the literature.

\n

There are advantages and disadvantages to this approach.

\n
  • Encoding into C required some hoop jumping to talk about what are ultimately straightforward bitvector and memory operations.
  • There is something clean about
  • Outputting C might enable usage into other tools too, although I specialized some things to CBMC
  • Having a readable C output is actually pretty useful
  • being able to compile and run the outputted C model is useful for debugging.
  • Writing the C++ and editing it for the asmc generator is more complicated
\n

This new tool is heavily AI produced based on my notes and directions. I am not very proficient at C++ and more importantly proficient at the internals of CBMC. I was not on track to even try such a thing unless is became easy to do so. All told, asmc-lift is about 1kloc of pretty reasonably simple C++ just gluing Ghidra to GOTO. The new world is exciting and scary. There have been efforts to make CBMC available as a backend to other languages (Kani for Rust uses it and there was some Ada stuff.) so all the dominos are already there.

\n

It’s bitter sweet to have AI knock it out like this. On the other hand, I have always basically considered binary verification stuff to be a (good!) compromise between what interests me and what society needs. I have spent a lot of time tearing my hair out over this stuff. I’m not so sad to see that go (if it is). I think my stance is to continue writing my little snippets and prototypes. In this case, I’ve written like 4 or 5 prototypes over the last 7 years. Prototype 6 is not that exciting to write.

\n

One could complain that it’s C semantics are not super hardo semantics (I’ve seen complaints on twitter about semantics that are less hardo than this). It is not oriented towards finding undefined behavior and takes reasonable compromises on it’s choices for modelling C.

\n

Ghidra pcode semantics is also not a hardo semantics. It has known holes and problems. It performs reasonably well (for example, it is sufficient to emulate Mario https://github.com/nevesnunes/ghidra-plays-mario ). You can find unsupported instructions or flags or behavior that is not modelled. So be it. It is pretty good though, supports a ton of ISAs (20+) and is readily available prepackaged. The hardo version of assembly semantics is SAIL, which I have found hard to work with but also been refuted every time I say this by people I respect who didn’t find it hard to work with.

\n

It is possible that the pricepoint of a much higher level of soundness has changed so significantly since the agentic AI boom last November that anything less than this standard is now defunct. It is not clear at this point. It depends what is in the pipeline, but what I have seen publicly thus far does not lead to this conclusion.

","headings":[{"level":1,"text":"Ghidra + CBMC = Assembly Model Checker","id":"ghidra-cbmc-assembly-model-checker"},{"level":1,"text":"Basic Examples","id":"basic-examples"},{"level":2,"text":"Mov 42","id":"mov-42"},{"level":2,"text":"ABI Checks","id":"abi-checks"},{"level":2,"text":"Risc V","id":"risc-v"},{"level":2,"text":"Compiling and Comparing mymax","id":"compiling-and-comparing-mymax"},{"level":1,"text":"Bits and Bobbles","id":"bits-and-bobbles"}]}}