零知识虚拟机（zkVM）通过把虚拟机语义翻译成执行轨迹上的代数约束，使通用程序能够被可验证地执行。这些约束的正确性至关重要：一条错误的约束可能使系统处于欠约束（under-constrained）状态，从而接受伪造的证明；也可能因过约束（over-constrained）而拒绝合法执行。现有手段在生产规模下都无法提供有意义的保证——模糊测试和单元测试覆盖不足、SMT 求解器难以应对约束的规模与非线性、定理证明器则需要大量人工投入。 本文提出 ZEBRA，一个全自动的验证与缺陷检测框架。其核心洞察是：对于给定程序与输入，约束系统必须恰好允许一条有效执行轨迹，不多也不少。由此，作者把 zkVM 验证归约为“规范轨迹空间上的解集基数问题”，并在计数之前先消除空行填充（null-row padding）、非确定性置换等结构性冗余。为使基数计算可处理，ZEBRA 将分析从有限域 witness 提升到整数区间格，并利用 zkVM 约束的结构稀疏性——在 5 个真实 zkVM 上，约束平均只使用了其理论连接容量的 14.0%——从而实现紧致的区间传播，并把近似误差控制在有限范围内。在此基础上，ZEBRA 执行并行的分支限界（branch-and-bound）搜索：要么给出一个具体的反例，要么证明在给定有界区域内不存在违规。 在 5 个真实 zkVM 上的评测中，ZEBRA 共发现 11 个零日缺陷，其中 6 个已被独立确认、3 个已被开发者修复；与基于 SMT 的验证相比，ZEBRA 速度快 51.5 倍，可验证的实例多 16.5 个百分点，其范围（区间）验证相比逐输入重复验证最多带来 63 倍的效率提升。该工作面向 zkVM／电路开发者与形式化验证研究者，提供了首个在真实系统上可扩展、可自动化的约束正确性检查路径。

该论文提出了一种基于自动机的黑盒技术，用于自动检测有状态网络协议实现中的状态机漏洞。有状态安全协议的实现需要维护一个状态机来跟踪协议进展，管理消息的类型和顺序以及加密材料，而状态机错误（即状态机bug）可能导致严重安全漏洞。该方法以协议的状态机bug目录作为输入，每个bug被表示为一个有限自动机，接受能够暴露该bug的消息序列。同时，它利用模型学习获得的（可能不准确的）待测实现模型，构造出模型中可执行且自动机可暴露bug的消息序列集，然后将这些序列转化为实际实现上的测试用例，以发现bug证据或排除误报。研究人员将技术应用于三个广泛使用的SSH服务器实现和九个不同的DTLS服务器和客户端实现（包括最新版本）。实验表明，该方法轻松复现了此前安全研究人员发现的所有bug，并生成了证据。更重要的是，它发现了这些实现中多个之前未知的bug，包括两个新漏洞，以及在相同SSH和DTLS实现的新版本中的多种新bug和不符合规范问题。该方法完全黑盒、自动化，可扩展至其他有状态协议，为协议实现的安全性测试提供了有力工具。

本文提出了一种利用代码自身检测功能相似但不一致代码的新方法。研究背景是软件开发中常出现功能相似但实现不一致的代码片段，可能导致难以发现的bug。核心问题是如何自动识别这类语义等价但语法有差异的代码对。方法上，作者设计了一个基于程序分析和机器学习的框架，通过提取代码的语义特征并比较其行为一致性，来发现潜在缺陷。实验在多个开源项目上进行，证明了该方法能有效检测出传统工具遗漏的bug。主要贡献包括提出新思路、构建原型系统以及公开评估数据集。适合代码审计工具开发者、软件质量工程师和编译器研究者阅读。

Rust 作为一种系统级编程语言，通过强大的类型系统和所有权模型在编译时保证内存安全，但实际应用中仍然存在运行时崩溃和内存安全错误，可能导致可利用漏洞。现有静态分析工具在检测 Rust 程序中的缺陷时存在精度或覆盖面的不足。本文提出 MirChecker，一种基于 Rust 中间表示 MIR 的静态分析框架，通过模拟抽象解释和自定义检查器来检测多种类型的缺陷，包括空指针解引用、整数溢出、数组越界等。该方法在多个 Rust 开源项目（如 Rust 标准库、Servo、Tock 等）上进行了评估，结果表明 MirChecker 能够发现现有工具（如 Clippy、Rustc 自身警告）无法检测到的真实错误，同时具有较低的误报率。主要贡献包括：（1）设计并实现了一个针对 MIR 的静态分析引擎，支持路径敏感分析；（2）提出多种检查器覆盖常见缺陷模式；（3）在真实项目中发现多个新的 bug 并得到开发者确认。该工作适合 Rust 开发者、安全研究人员以及编译器工程人员阅读，有助于改进 Rust 生态系统的安全性。

该论文提出了一种自动检测 Linux 内核驱动中引用计数错误（reference counting bugs）的工具 DrvHorn。引用计数是内核实中管理资源（如内存、文件描述符等）生命周期的关键机制，一旦出现错误（如少放、多放或未初始化），可能导致资源泄漏、内存损坏甚至安全漏洞。传统方法如静态分析存在高误报率或难以覆盖复杂路径的问题。DrvHorn 通过将引用计数验证转化为断言检查问题，并利用 Linux 驱动接口（如 open/close 钩子）对内核进行高效建模，同时采用激进程序切片技术降低分析复杂度。作者在 Linux v6.6 内核的所有平台驱动上进行了测试，共发现 545 个引用计数 bug，其中 424 个为以前未知，误报率仅为 29.9%，低于之前研究。针对新发现的 bug，作者向 Linux 内核社区提交了补丁，其中 45 个已被合并。该工具展示了自动化检测复杂内核驱动中资源管理错误的能力，对提升内核安全性具有重要价值。