Ghidra 加 CBMC：给汇编代码做有界模型检查
来源：www.philipzucker.com — 2026-10-16
📋 概述
Philip Zucker 介绍了 ASMC：把 Ghidra 提升出的汇编语义喂进 CBMC，从而对汇编本身做形式化验证。链条是三段——CBMC 提供 GOTO IR 与 .gb 对象格式；asmc-lift 借 Trail of Bits 打包的 sleigh/pcode 把 .elf 提升成 .gb；asmc 则是驱动，串起提升与模型检查。作者欣赏它的原因和欣赏 CBMC 一样：用法极灵活（独立汇编验证、翻译验证、把外部汇编链进 C、为汇编写 C 规格、结合 DWARF 调试信息验证、验证打过补丁的汇编、验证反编译结果），而核心提升工具只有约一千行 C++，因为 GOTO 与 P-Code 本来就高度相似。文中给的例子很直观：让 myfun 把 42 放进 rax 再返回，用 --post 「outreg.rax == 42」 通过、改成 43 则给出反例轨迹；若把 42 写进栈顶再 ret，会被判为「意外的返回地址，栈返回地址可能被破坏」；若写 r12 却不恢复，则报「被调用者保存寄存器 R12 未被恢复」——ABI 义务也被自动检查。
🔑 核心要点
- ASMC 的拼法很省事：CBMC 出 GOTO IR 与 .gb 格式，asmc-lift 用 sleigh/pcode 把 ELF 提升成 .gb，asmc 负责串起来跑检查
- 核心提升工具只有约一千行 C++，因为 GOTO IR 与 Ghidra 的 P-Code 结构本来就非常接近
- 用处覆盖面广：独立汇编验证、翻译验证、为汇编写 C 规格、结合 DWARF 校验调试数据、验证打补丁后的汇编、验证反编译结果
- 后置条件直接用 C 写：--post 「outreg.rax == 42」 会被拼进 CBMC 的断言，还能给反例轨迹与最近执行的机器指令
- 连 ABI 都顺手检查：把 42 写进栈顶再 ret 会报「意外的返回地址」，写 r12 而不恢复会报「被调用者保存寄存器未被恢复」
- 设计哲学与 CBMC 一致：许多关于汇编的问题本质上是它与 C 层概念的交互，所以紧贴 CBMC 比自己造一套规格语言更划算
💡 金句
最终我们想问汇编的许多问题，都是关于它如何与 C 层的概念交互，或者用接近 C 的东西表达与规格化会更简单，所以与 CBMC 紧密集成非常有用。
👍 0
👎 0
← 返回 Lobsters 首页