ASMC 将 Ghidra 汇编语义接入 CBMC
热点事件持续更新
ASMC 将 Ghidra 汇编语义接入 CBMC
1 篇报道1 个报道来源1 小时前更新
先了解这件事
AI 综述
Philip Zucker 介绍并演示了 ASMC：它把 Ghidra 的 pcode 汇编语义接入 CBMC，用于对编译后的汇编做模型检查。asmc-lift 将 .elf 文件提升为 CBMC 的 .gb 格式，再由 asmc 驱动检查；主提升工具约 1kLOC C++ 胶水代码，可用于独立汇编验证、翻译验证和反编译验证。 演示中，mov $42,%rax 的后置条件 outreg.rax == 42 通过，改成 43 则返回反例。
AI 根据报道生成 · 1 小时前更新
最新进展10月18日 12:38
Ghidra + CBMC 组装模型检查器 ASMC：把汇编语义接入 CBMC报道时间线
沿着报道，了解事件的不同侧面。
10月18日
- Hacker NewsGhidra + CBMC 组装模型检查器 ASMC：把汇编语义接入 CBMC
ASMC 将 Ghidra 的 pcode 汇编语义接入 CBMC，asmc-lift 把编译后的 .elf 文件提升为 CBMC 的 .gb 格式，再由 asmc 驱动完成模型检查。主提升工具仅约 1kLOC C++ 胶水代码，支持独立汇编验证、翻译验证、反编译验证等场景。示例中 mov $42,%rax 的后置条件 outreg.rax == 42 通过，改成 43 则返回反例。
本事件热度走势
还没有足够的连续观测数据，暂不绘制趋势。