文章介绍了ASMC（汇编模型检查器），该工具将Ghidra的PCode语义与CBMC（C有界模型检查器）集成，实现对汇编代码的形式化验证。工具使用SLEIGH将.elf文件转换为CBMC的.gb格式，核心粘合代码仅约1千行，支持独立汇编验证、转换验证和反编译验证等多种场景。
背景
CBMC是一个开源的C/C++有界模型检查器，广泛用于软件形式化验证。Ghidra的SLEIGH反汇编框架通过PCode中间表示提供程序化的反编译语义访问能力。
- 来源
- Lobsters
- 发布时间
- 2026年10月19日 00:58
- 评分
- 6.0 / 10