Ghidra + CBMC = Assembly Model Checker

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

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.

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.

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.

Basic Examples

Mov 42

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

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

Overwriting /tmp/mov42.s

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

! asmc /tmp/mov42.s --function myfun --post 'outreg.rax == 42'

Output: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-kdgw9qv7
assemble: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-kdgw9qv7/assemble.log
ELF: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-kdgw9qv7/target.elf
Harness: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-kdgw9qv7/demo.c (x86-64 SysV)
Checking: 1 postcondition(s), safety and scalar ABI obligations.
seed: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-kdgw9qv7/seed.log
lift: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-kdgw9qv7/lift.log
ASMC lift range: myfun has no ELF size; reachable code window in .text [0x401000, 0x401008)
link: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-kdgw9qv7/link.log
cbmc: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-kdgw9qv7/cbmc.log
PASS: all checked properties passed with unwinding assertions

This of course should fail.

! asmc /tmp/mov42.s --function myfun --post 'outreg.rax == 43'

Output: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-ej9b_2i2
assemble: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-ej9b_2i2/assemble.log
ELF: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-ej9b_2i2/target.elf
Harness: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-ej9b_2i2/demo.c (x86-64 SysV)
Checking: 1 postcondition(s), safety and scalar ABI obligations.
seed: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-ej9b_2i2/seed.log
lift: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-ej9b_2i2/lift.log
ASMC lift range: myfun has no ELF size; reachable code window in .text [0x401000, 0x401008)
link: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-ej9b_2i2/link.log
cbmc: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-ej9b_2i2/cbmc.log
  [harness.assertion.1] line 247: FAILURE
Counterexample (contract register views; use --full-trace for all values and machine steps):
Trace for harness.assertion.1:

  demo.c:172  outreg.rax=42ul
  Recent machine instructions:
    0x401000 MOV RAX,0x2a
    0x401007 RET 
Violated property:
  file /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-ej9b_2i2/demo.c function harness line 247 thread 0
  post: outreg.rax == 43

Trace and details: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-ej9b_2i2/cbmc.log
FAIL: counterexample found

ABI Checks

This also fails because we stomp the return pointer

%%file /tmp/mov42.s
.text
.globl myfun
myfun:
    mov $42, (%rsp)
    ret

Overwriting /tmp/mov42.s

! asmc /tmp/mov42.s --function myfun

Output: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-8j5vcj4x
assemble: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-8j5vcj4x/assemble.log
ELF: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-8j5vcj4x/target.elf
Harness: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-8j5vcj4x/demo.c (x86-64 SysV)
Checking: safety and scalar ABI obligations only (no --post).
seed: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-8j5vcj4x/seed.log
lift: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-8j5vcj4x/lift.log
ASMC lift range: myfun has no ELF size; reachable code window in .text [0x401000, 0x401008)
link: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-8j5vcj4x/link.log
cbmc: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-8j5vcj4x/cbmc.log
  [asmc_target.asmc.13] line 6 unexpected return address (possible clobbered stack return address or incorrect RSP); 0x401007 pcode[2] RET  (RETURN)
    Machine: 0x401007 pcode[2] RET  (RETURN)
Counterexample (harness/reference values; use --full-trace for all values and machine steps):
Trace for asmc_target.asmc.13:

  demo.c:94  inreg.rax=0ul
  demo.c:95  inreg.rcx=0ul
  demo.c:96  inreg.rdx=0ul
  demo.c:97  inreg.rbx=0ul
  demo.c:98  inreg.rsp=4344ul
  demo.c:99  inreg.rbp=0ul
  demo.c:100  inreg.rsi=0ul
  demo.c:101  inreg.rdi=0ul
  demo.c:102  inreg.r8=0ul
  demo.c:103  inreg.r9=0ul
  demo.c:104  inreg.r10=0ul
  demo.c:105  inreg.r11=0ul
  demo.c:106  inreg.r12=0ul
  demo.c:107  inreg.r13=0ul
  demo.c:108  inreg.r14=0ul
  demo.c:109  inreg.r15=0ul
  demo.c:110  inreg.cf=0
  demo.c:111  inreg.pf=0
  demo.c:112  inreg.af=0
  demo.c:113  inreg.zf=0
  demo.c:114  inreg.sf=0
  demo.c:115  inreg.of=0
  demo.c:116  inreg.df=0
  Recent machine instructions:
    0x401000 MOV dword ptr [RSP],0x2a
    0x401007 RET 
Violated property:
  file /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-8j5vcj4x/lifted.gb.asm function asmc_target line 6 thread 0
  unexpected return address (possible clobbered stack return address or incorrect RSP); 0x401007 pcode[2] RET  (RETURN)
  asmc_tmp_12 == asmc_tmp_13

  Return destination: 0x7fff0000002a (140733193388074)
  Expected harness return sentinel: 0x7fffffff0000

Trace and details: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-8j5vcj4x/cbmc.log
FAIL: counterexample found

A different ABI violation, not restoring the callee saved R12

%%file /tmp/movr12.s
.text
.globl myfun
myfun:
    mov $42, %r12
    ret

Overwriting /tmp/movr12.s

! asmc /tmp/movr12.s --function myfun

Output: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-0_l28dvp
assemble: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-0_l28dvp/assemble.log
ELF: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-0_l28dvp/target.elf
Harness: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-0_l28dvp/demo.c (x86-64 SysV)
Checking: safety and scalar ABI obligations only (no --post).
seed: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-0_l28dvp/seed.log
lift: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-0_l28dvp/lift.log
ASMC lift range: myfun has no ELF size; reachable code window in .text [0x401000, 0x401008)
link: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-0_l28dvp/link.log
cbmc: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-0_l28dvp/cbmc.log
  [asmc_sysv_check.assertion.5] line 91 ABI violation: callee-saved register R12 was not restored
Counterexample (harness/reference values; use --full-trace for all values and machine steps):
Trace for asmc_sysv_check.assertion.5:

  demo.c:94  inreg.rax=0ul
  demo.c:95  inreg.rcx=0ul
  demo.c:96  inreg.rdx=0ul
  demo.c:97  inreg.rbx=0ul
  demo.c:98  inreg.rsp=4344ul
  demo.c:99  inreg.rbp=0ul
  demo.c:100  inreg.rsi=0ul
  demo.c:101  inreg.rdi=0ul
  demo.c:102  inreg.r8=0ul
  demo.c:103  inreg.r9=0ul
  demo.c:104  inreg.r10=0ul
  demo.c:105  inreg.r11=0ul
  demo.c:106  inreg.r12=16777216ul
  demo.c:107  inreg.r13=0ul
  demo.c:108  inreg.r14=0ul
  demo.c:109  inreg.r15=0ul
  demo.c:110  inreg.cf=0
  demo.c:111  inreg.pf=0
  demo.c:112  inreg.af=0
  demo.c:113  inreg.zf=0
  demo.c:114  inreg.sf=0
  demo.c:115  inreg.of=0
  demo.c:116  inreg.df=0
  Recent machine instructions:
    0x401000 MOV R12,0x2a
    0x401007 RET 
Violated property:
  file /home/philip/vibe_coding/asmc/include/asmc_x86.h function asmc_sysv_check line 91 thread 0
  ABI violation: callee-saved register R12 was not restored
  return_value_asmc_get_reg$3 == frame->preserved[(signed long int)2]

Trace and details: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-0_l28dvp/cbmc.log
FAIL: counterexample found

Risc V

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

%%file /tmp/mov42.s
.text
.globl myfun
myfun:
    li a0, 42
    ret

Overwriting /tmp/mov42.s

! CC=riscv64-unknown-elf-gcc asmc /tmp/mov42.s --function myfun

Output: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-mvmxg5f8
assemble: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-mvmxg5f8/assemble.log
ELF: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-mvmxg5f8/target.elf
Harness: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-mvmxg5f8/demo.c (RV64)
Checking: safety and scalar ABI obligations only (no --post).
seed: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-mvmxg5f8/seed.log
lift: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-mvmxg5f8/lift.log
ASMC lift range: myfun has no ELF size; reachable code window in .text [0x100b0, 0x100b6)
link: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-mvmxg5f8/link.log
cbmc: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-mvmxg5f8/cbmc.log
PASS: all checked properties passed with unwinding assertions; safety/ABI only, no functional postcondition

Compiling and Comparing mymax

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

%%file /tmp/max.c
#include <stdint.h>
uint32_t mymax(uint32_t a, uint32_t b) {
    return a >= b ? a : b;
}

Overwriting /tmp/max.c

! gcc -c -S /tmp/max.c -o /tmp/max.s

Now we can hand the assembled version to CBMC

! asmc /tmp/max.s --function mymax --post 'outreg.eax == (inreg.edi >= inreg.esi ? inreg.edi : inreg.esi)'

Output: /home/philip/philzook58.github.io/_drafts/asmc-out/mymax-mq_lzxqu
assemble: /home/philip/philzook58.github.io/_drafts/asmc-out/mymax-mq_lzxqu/assemble.log
ELF: /home/philip/philzook58.github.io/_drafts/asmc-out/mymax-mq_lzxqu/target.elf
Harness: /home/philip/philzook58.github.io/_drafts/asmc-out/mymax-mq_lzxqu/demo.c (x86-64 SysV)
Checking: 1 postcondition(s), safety and scalar ABI obligations.
seed: /home/philip/philzook58.github.io/_drafts/asmc-out/mymax-mq_lzxqu/seed.log
lift: /home/philip/philzook58.github.io/_drafts/asmc-out/mymax-mq_lzxqu/lift.log
link: /home/philip/philzook58.github.io/_drafts/asmc-out/mymax-mq_lzxqu/link.log
cbmc: /home/philip/philzook58.github.io/_drafts/asmc-out/mymax-mq_lzxqu/cbmc.log
PASS: all checked properties passed with unwinding assertions

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

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.

%%file /tmp/harness.c
#include "asmc_x86.h"
#include "/tmp/max.c"

uint32_t mymax(uint32_t a, uint32_t b);
uint32_t nondet_u32(void);

void harness(void) {
    uint32_t a = nondet_u32();
    uint32_t b = nondet_u32();
    uint8_t stack[256];
    struct asmc_state st;

    // set up arguments 
    asmc_sysv_arg32(&st, 0, a);
    asmc_sysv_arg32(&st, 1, b);

    /* Set up the stack, execute assembly, and check ABI preservation. */
    asmc_sysv_call_ram_model(&st, stack, 0x1000, sizeof stack);

    assert(asmc_sysv_result32(&st) == mymax(a, b));
}

Overwriting /tmp/harness.c

! asmc /tmp/max.s --function mymax --harness /tmp/harness.c

Output: /home/philip/philzook58.github.io/_drafts/asmc-out/mymax-ql9__2ez
assemble: /home/philip/philzook58.github.io/_drafts/asmc-out/mymax-ql9__2ez/assemble.log
ELF: /home/philip/philzook58.github.io/_drafts/asmc-out/mymax-ql9__2ez/target.elf
seed: /home/philip/philzook58.github.io/_drafts/asmc-out/mymax-ql9__2ez/seed.log
lift: /home/philip/philzook58.github.io/_drafts/asmc-out/mymax-ql9__2ez/lift.log
link: /home/philip/philzook58.github.io/_drafts/asmc-out/mymax-ql9__2ez/link.log
cbmc: /home/philip/philzook58.github.io/_drafts/asmc-out/mymax-ql9__2ez/cbmc.log
PASS: all checked properties passed with unwinding assertions

Bits and Bobbles

There are bigger examples in the repository.

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

https://github.com/philzook58/pcode2c

• PCode2C: Steps Towards Translation Validation with Ghidra and CBMC https://www.philipzucker.com/pcode2c/
• DWARF Verification via Ghidra and CBMC https://www.philipzucker.com/pcode2c-dwarf/

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

• https://www.philipzucker.com/refine_assembly/
• https://www.philipzucker.com/asm_verify4/
• https://www.philipzucker.com/asm_verify3/
• https://www.philipzucker.com/asm_verify2/
• https://www.philipzucker.com/assembly_verify/

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

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

There are advantages and disadvantages to this approach.

• 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

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.

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.

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.

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.

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.