该论文聚焦于处理器规范（processor specification）的正确性验证问题。处理器规范是反汇编器、反编译器、模拟器等关键安全与程序分析工具的基础，但其正确性很少被系统检查。规范中的错误会扭曲程序行为、掩盖漏洞，甚至为分析规避技术提供可乘之机。论文首次针对开源社区广泛使用的 SLEIGH 语言规范（尤其是 Ghidra 所使用的）开展系统性验证。作者设计并实现了一个名为 InSPECtor 的测试框架，采用基于代理的自动 oracle 验证策略。该方法利用规范本身编码的结构来枚举可解码的指令形式，并生成有针对性的初始状态；随后通过对比执行相同指令的模拟器与硬件参考实现，进行差分测试，从而验证指令解码与模拟的正确性。研究覆盖了多种风格迥异的开源规范，包括 x86-64、AArch64、ARM/Thumb、RISC-V 和 MSP430，这些规范在编写风格、作者偏好及指令集架构设计上存在显著差异。实验发现了超过 38,920 处不一致，并从中提炼出 125 个独特缺陷，且提出了修复建议；这些缺陷涵盖解码错误、语义缺陷以及跨厂商不一致问题。作者将发现归纳为 8 条具体建议，以推动未来规范质量的改进。该工作强调了规范正确性的重要性，并提供了实用工具来大幅提升 SLEIGH 处理器规范的保真度，从而增强下游安全与分析工具的可靠性。

本文介绍了 Zorya 符号执行框架的扩展，使其能够处理由 Go 标准 gc 编译器生成的多线程二进制文件。Zorya 框架最初仅支持单线程 TinyGo 二进制，通过将二进制提升到 Ghidra 的 P-Code 中间表示，并利用 Z3 SMT 求解器对具体值和符号值进行推理来检测漏洞。为了支持 gc 编译的二进制，作者解决了三个关键挑战：从 gdb 转储恢复操作系统线程状态以处理多线程；中和运行时抢占机制避免执行干扰；引入写时复制（copy-on-write）覆盖路径分析，用于检测未执行分支上的静默漏洞（如整数溢出）。研究在 11 个来自生产级 Go 项目（如 Kubernetes、Go-Ethereum 和 CoreDNS）的真实漏洞上进行了严格评估。结果表明，Zorya 成功检测出 7 个二进制级别漏洞，其中包括一个静默整数溢出——其他评估工具在没有手动编写预言（oracle）的情况下无法发现。该工作显著扩展了 concolic 测试在 Go 生态系统的实用性，为自动化安全分析提供了新手段。适合安全研究人员、Go 开发者和二进制分析工具开发者阅读。