Ghidra + CBMC = 汇编模型检查器

# Ghidra + CBMC = 汇编模型检查器 来源: https://www.philipzucker.com/asmc_cpp/ ASMC (https://github.com/philzook58/asmc) 是另一个 (https://github.com/philzook58/pcode2c) 尝试将 Ghidra 提升后的汇编语义粘合到 CBMC 中的项目。C 有界模型检查器 https://github.com/diffblue/cbmc 是一个处于正确性、可扩展性和实用性帕累托前沿的有用工具。我觉得它非常酷 (https://www.philipzucker.com/cbmc_tut/)。CBMC 有一种称为 GOTO IR 的中间表示，以及名为 `.gb` 的目标文件格式。`asmc-lift` 接受一个已编译的 `.elf` 文件，并使用由 Trail of Bits 打包的 Ghidra pcode 语义 (https://github.com/lifting-bits/sleigh) 将其提升为 `.gb` 文件（感谢 Eric！）。`asmc` 本身是一个驱动程序，它运行 `asmc-lift` 和其他 CBMC 工具来实际执行模型检查。我喜欢它的一点是，像 CBMC 一样，它对许多用例都很灵活（独立汇编验证、翻译验证、链接到外部汇编、用 C 规格描述汇编、DWARF 调试数据验证、补丁后汇编验证、反编译验证），而且主要的提升工具本身只需要相当少量的胶水 C++ 代码（约 1k 行代码）。GOTO 和 P-Code 非常相似。归根结底，我们想对汇编提出的许多问题都涉及它与 C 级别概念的交互，或者在类似 C 的层面更容易表达/描述，因此与 CBMC 的紧密集成非常有用。 ## 基本示例 ## Mov 42 这是一个最基本的示例。我们将 42 移动到 rax（返回寄存器）中。 ```asm %%file /tmp/mov42.s .text .globl myfun myfun: mov $42, %rax ret ``` 我们可以运行它并检查是否确实返回了 42。驱动程序在底层调用 `CC` 并链接汇编文件。我们也可以提供一个预汇编好的 `.elf` 文件。后条件字符串基本上会被拼接到 C 语言的 CBMC 断言中，因此断言语言是 C。对于更复杂的情况，我们需要编写测试框架。 ``` ! 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 ``` 这当然应该通过。 ``` ! 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 检查 这也应该失败，因为我们覆盖了返回指针。 ```asm %%file /tmp/mov42.s .text .globl myfun myfun: mov $42, (%rsp) ret ``` ``` ! 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 ``` 另一种 ABI 违规——没有恢复被调用者保存的 R12 寄存器。 ```asm %%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 目前也支持 RV32/64。支持 Ghidra 所有的不同架构主要只需要在 C 中编写一个新的 ABI 适配层。 ```asm %%file /tmp/mov42.s .text .globl myfun myfun: li a0, 42 ret ``` ``` ! 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 ``` ## 编译并比较 mymax 我们可以将一个 C 函数编译成汇编文件（或 ELF），然后直接对它验证属性。 ```c %%file /tmp/max.c #include <stdint.h> uint32_t mymax(uint32_t a, uint32_t b) { return a >= b ? a : b; } ``` ``` ! gcc -c -S /tmp/max.c -o /tmp/max.s ``` 现在我们可以把汇编后的版本交给 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 ``` 但我们也可以比较原始 C 版本和汇编版本。这就是翻译验证。这里是我们第一个自定义测试框架。基本上，asmc 提供了一个函数来调用汇编片段。所有这些都是通过 CBMC 进行的，因此 CBMC 提供的一切都可以使用。这里我们比较的是 C 版本和汇编版本的输出。 ```c %%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 ``` ## 杂项 仓库中有更大的示例。归根结底，这是一个与 pcode2c 非常相似的工具，pcode2c 将 Ghidra pcode 提升为一个专用的 C 解释器，以便你可以使用 CBMC。 - https://github.com/philzook58/pcode2c - PCode2C: 使用 Ghidra 和 CBMC 迈向翻译验证的第一步 https://www.philipzucker.com/pcode2c/ - 通过 Ghidra 和 CBMC 验证 DWARF https://www.philipzucker.com/pcode2c-dwarf/ 最近，我一直在尝试用 Python 工具做类似的事情，它通过 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/ 所有这些最终都是对 CBAT https://www.ndss-symposium.org/ndss-paper/auto-draft-437/ 的后续工作。 我记得在文献中有其他将汇编语义连接到 CBMC 的努力。这种方法有优点也有缺点。 - 编码为 C 需要绕一些弯路来表达最终是直接的位向量和内存操作。 - 有一些简洁的地方在于——输出 C 可能也能用于其他工具，虽然我对 CBMC 做了一些专门化。 - 拥有可读的 C 输出实际上相当有用——能够编译和运行输出的 C 模型对于调试也很有用。 - 编写 C++ 并为 asmc 生成器修改它更加复杂。 这个新工具在很大程度上是由 AI 基于我的笔记和指导生成的。我并不精通 C++，更重要的是不精通 CBMC 的内部原理。如果不是因为变得容易做到，我根本不会走上尝试这样东西的道路。总而言之，`asmc-lift` 大约 1k 行非常简单合理的 C++ 代码，只是将 Ghidra 粘合到 GOTO。 新世界既令人兴奋又令人恐惧。已有将 CBMC 作为其他语言后端的努力（Rust 的 Kani 使用它，还有一些 Ada 的东西），所以所有的多米诺骨牌都已就位。让 AI 像这样搞定它是苦乐参半的。另一方面，我基本上一直认为二进制验证方面的工作是我感兴趣的事物和社会需求之间的一个（好的！）折中。我在这上面花费了大量时间抓狂。我并不太为此感到难过（如果它确实被替代了）。我认为我的立场是继续编写我的小片段和原型。在这种情况下，过去 7 年里我已经写了大约 4 或 5 个原型。编写第 6 个原型并不那么令人兴奋。 有人可能会抱怨它的 C 语义不是特别严格的语义（我在 Twitter 上见过对没有这么严格语义的抱怨）。它不以发现未定义行为为目标，在 C 建模的选择上做了合理的折中。Ghidra pcode 语义……