首个 x86 全进程机器检验安全证明发布，覆盖 12.8 万条指令

banteg · x · 2026-10-31

安全研究者 v12sec 与 Zellic 合作发布了（据称是）首个针对 x86 二进制端到端执行安全性质的机器检验证明：对象是一个静态链接 glibc 的 Linux 进程。配图显示共分析 128,693 条指令，其中约 5.4k 条在实际执行路径上被证明、约 10k 条其他路径被证明，23k 条 IFUNC 候选仅验证地址属性，约 88k 条未被触达（如 locale/字符集等代码）。团队认为该方法可扩展，正式发布尚属首次。