本文提出并实现了一个名为 Verbatim 的可执行词法分析器（lexer），其开发和验证均基于 Coq 证明助手。词法分析器和解析器常被用作大型软件系统的前端，负责连接外部输入与系统内部逻辑，因此成为攻击者试图攻陷整个系统的天然目标。作者认为，一个经过形式化验证、具备机械化词法分析能力的工具能够显著降低针对这些前端的攻击效力。论文的核心贡献在于：1）给出了 Verbatim 的完整实现，它是一个可执行的、与标准词法分析器规范兼容的 lexer；2）在 Coq 中机械证明了 Verbatim 相对于标准词法分析器规范的正确性，即所有正确性证明均已机器检查，避免了手工证明中可能存在的漏洞；3）分析了 Verbatim 的理论复杂度，并提供了实证性能评估结果。与依赖测试或运行时检查的传统 lexer 生成器不同，Verbatim 从构造上保证了词法分析的正确性，为构建高可信软件前端提供了新的思路。该研究适合对形式化验证、编译器前端安全、高保证软件工程感兴趣的 researchers 和开发者；对于蓝队而言，理解这类验证工具可帮助评估在关键系统中引入形式化验证组件的可行性和收益，从而减少外部输入处理环节的潜在攻击面。然而，由于本文尚未发布完整工具链或大规模应用案例，其实际工程部署价值仍需进一步验证。

本文提出 PANDA，一个基于零知识证明（ZKP）的可扩展系统，用于在保护神经网络模型参数私密性的同时，形式化地证明模型的鲁棒性和公平性。随着机器学习模型在安全关键和法律合规场景中的部署日益增多，模型的鲁棒性和公平性保证变得重要，但模型参数常被视为商业机密，不能直接暴露给审计方或终端用户。PANDA 构建在 CROWN 这一高效的鲁棒性认证框架之上，CROWN 已被许多最先进的神经网络形式化验证工具使用。PANDA 的核心贡献是提出一种新的算法，用于证明非线性激活层的线性松弛界，从而生成简单且轻量的证明。实验表明，PANDA 能够在 5 分钟内为超过 290 万参数的神经网络生成局部鲁棒性证明，并在 10 秒内完成验证。相比之下，之前基于 ZKP 的鲁棒性系统依赖指数时间算法，无法扩展到有意义的网络规模。PANDA 的证明生成和验证复杂度在神经元数量上呈多项式增长，因此能够支持的神经网络规模比之前方法大 4 个数量级，同时显著降低证明者的开销。该研究面向机器学习安全、形式化验证和密码学交叉领域的研究人员，尤其适合关注模型完整性证明和隐私保护下的认证技术的安全从业者。

本文研究近似同态加密（approximate homomorphic encryption）中噪声泛洪（noise flooding）防御手段在自适应解密攻击下的安全性证明问题。噪声泛洪是抵御解密攻击的标准技术，但其安全证明对组合方式异常敏感：若用统计接近的模拟替换 q 次自适应解密应答，并采用普通混合论证，则会损失线性因子 q。传统密码学证明改为累积条件 KL（Kullback-Leibler）散度成本，并在最后一次性转换为统计距离，从而获得参数关键的平方根损失。作者使用 Rocq 证明助手和 SSProve 框架对该论证进行机器验证。针对任意满足近似正确性和 IND-CPA 安全的全同态加密方案，他们形式化了对于任意 q 次查询的 IND-CPAD 攻击者的归约，并证明了攻击优势上界为 β_CPA(B_A,q) + sqrt(qn)/(2γ)，其中 n 是明文维度，γ 是泛洪宽度乘子。证明过程中构建了一种基于 SSProve 语义的新型关系程序逻辑，其毕达哥拉斯判断（Pythagorean judgment）能够组合条件 KL 预算而无需转换为统计距离；同时，一个经过验证的迹编译器将局部预言机规则提升到任意自适应程序，且仅需一次最终转换。该工作的核心贡献在于：为自适应场景下噪声泛洪安全性提供了机器可验证的证明框架，解决了混合论证中线性损失与平方根损失之间的微妙权衡问题，并为同态加密安全性证明的机械化奠定了基础。适合对密码学形式化验证、同态加密安全性分析以及程序逻辑感兴趣的科研人员与安全工程师阅读。

这篇研究报告探讨了在智能合约（如 Diem 支付网络）中推广形式化验证时，开发人员对“规范（specifications）”角色的不同理解如何影响形式化验证的整体效果。作者指出，初次接触形式化验证的软件开发者，往往对规范在操作层面上的意义持有微妙但不同的解释，这些解释会直接影响他们编写的规范类型，进而导致保证效果碎片化，削弱验证工作的整体效力。论文基于在一个金融敏感的智能合约环境中部署形式化验证系统的实际经验，总结了工业界资深开发者（但对形式化方法尚属新手）中常见的三种观点：1）规范是与最终用户沟通的实现与功能之间的契约；2）规范是类型系统的扩展；3）规范是高层状态机的定义。作者认为，虽然哪种解释更接近规范的真正目的尚无定论，但一个重要区分被忽略了：某些规范是“抽象规范（abstracting specs）”，用于锁定需求或意图，因此越多越好；另一些规范是“证明辅助（proof assistance）”，旨在促进实现与抽象规范之间的精化证明，因此应仅在需要时编写；还有一些规范是“指称规范（denotational specs）”，从形式化方法角度看并不增加额外的保证。若缺乏这一区分，形式化验证很容易陷入“规范累积但整体保证并未增加”的陷阱。论文作为一种经验报告，核心贡献在于提出应当明确区分不同类型的规范，并强调抽象规范在保证整体验证有效性中的关键作用。适合正在或计划在智能合约、区块链或高安全性系统中引入形式化验证的团队阅读，尤其对安全工程师和验证工程师具有实践指导意义。

该论文提出了 VUPER，一个用于生成经过形式化验证的 ASN.1 UPER（非对齐压缩编码规则）解析器的框架。ASN.1 是一种广泛使用的接口描述语言，而 UPER 是其中关键的编码规则之一，尤其在蜂窝网络和车联网（V2X）通信等安全关键领域应用广泛。为保证这一基础基础设施的正确性和安全性，作者首先形式化了位精确解析器的概念，并识别出能够证明解析器与序列化器往返一致性的属性，同时考虑了 ASN.1 的向后/向前兼容性等特性。接着，他们按照 UPER 规范，为 ASN.1 基本类型和结构实现并验证了解析器和序列化器组合子。他们还开发了一个编译器，能够将 ASN.1 定义转换为经过验证的解析器。最后，他们构建了一个以 VUPER 解析器为测试基准的动态测试框架。为了实证评估，作者使用 5G 和 V2X 通信协议测试了 7 个开源和 4 个商业 ASN.1 解析器。VUPER 在流行解析器中发现了 20 种类型的不一致，并展示了对 ASN.1 UPER 标准更严格的合规性。此外，他们还通过利用这些解析器漏洞展示了具体攻击。该研究的主要贡献在于提出了一种可能的方法来生成验证过的解析器，并揭示了现有解析器实现中的大量缺陷，为相关安全加固提供了基础。适合编译器、形式化验证、协议安全及通信系统安全领域的研究人员和工程师阅读。

本文提出一个面向多智能体生成式AI系统治理的严格数学框架，聚焦于K个自适应性生成式AI模型在模型风险管理（MRM）原则下的联合稳定性与零知识证明问题。研究背景在于：当多个模型通过交互矩阵形成元学习耦合时，传统基于单个智能体的Lyapunov稳定性分析不再充分——可能出现每个智能体各自满足声称的稳定性边界，但整个联合系统在涌现层面发生漂移（emergent ensemble-level drift）的情形。作者将该差距形式化为“联合Lyapunov证明”（JLP），这是一个结合密码学与随机过程的协议，能够在每个验证周期内不泄露专有权重的前提下，证明聚合动态满足MRM持续监控标准。主要贡献包括：完整刻画联合二次Lyapunov函数的无穷小生成元；推导系统失去均方稳定性的临界耦合阈值精确表达式；证明“噪声底限定理”（Noise-Floor Theorem），并识别零知识证明的正确目标；推导基于实时权重的逐周期简洁非交互式知识论证（SNARK）。所有理论声明均通过多智能体softmax系统的五项数值研究验证。该论文适合从事AI治理、模型风险管理、形式化验证及可验证机器学习的研究人员阅读，为多模型耦合场景下的风险监控提供了理论工具与可审计性方案。

这篇 SoK（系统化知识）论文对计算机辅助密码学（Computer-Aided Cryptography）领域进行了跨领域的系统化梳理。计算机辅助密码学是一个活跃的研究方向，致力于开发和应用形式化、机器可检查的方法来设计、分析和实现密码学协议。论文聚焦于三个主要领域：（1）设计级安全性，涵盖符号安全性和计算安全性；（2）功能正确性与效率；（3）实现级安全性，重点关注数字侧信道抗性。在每个领域中，作者首先阐明了计算机辅助密码学在应对当前挑战中的作用——它能提供何种帮助以及存在的注意事项；随后提出了对现有工具的 taxonomy（分类法），比较了它们的准确性、覆盖范围、可信度和易用性；接着 highlights（重点介绍）了主要成就、权衡取舍和研究挑战。在覆盖这三个主要领域之后，论文呈现了两个案例研究：第一个研究尝试整合不同领域的工具，以巩固它们能提供的保证；第二个研究总结了计算机辅助密码学社区参与 TLS 1.3 标准化工作的经验教训。最后，论文对论文作者、工具开发者和标准化组织提出了未来发展的建议。该论文是该领域的权威性综述，适合密码学研究者、安全形式化方法开发者、协议设计者以及标准化参与者阅读。

量子密钥分发（QKD）协议通过量子力学原理提供信息论安全性，但实际部署中QKD本质上是混合协议：其安全结论高度依赖量子阶段与经典后处理阶段的正确集成。虽然ETSI和ITU-T等标准组织已定义了QKD的架构与接口，但现有规范通常在隔离条件下评估协议安全性，导致跨层交互成为未被充分探索的攻击面。本文提出一种基于ETSI和ITU-T QKD规范的形式化验证框架，首次在混合协议模型下对QKD进行自动化协议级安全分析，重点考察经典操作如何影响量子阶段所提供的安全保证。作者使用自动化协议验证工具Tamarin，构建了符合ETSI/ITU-T规范的QKD协议综合符号模型。在该框架下，作者针对名为Eve+的敌手模型，获得了三项规范级漏洞的形式化证据：被颠覆的纠缠注入（subverted entanglement injection）、基延迟测量（basis-deferred measurement）和消息反射（message reflection）。这些漏洞均源于规范程序文本中经典控制平面的某种缺失，且仅在符号抽象下成立，并非对所有实际部署的普遍断言。为缓解这些问题，作者提出两项协议改进：测量承诺（measurement commitment）和身份绑定消息认证码（identity-bound MACs）。Tamarin验证表明，这些对策能够消除Eve+模型下识别出的漏洞。研究结果和建议已发送给相关标准化组织。本文的贡献在于首次以形式化方法系统性地将经典控制面纳入QKD协议安全分析，揭示了标准规范中被忽略的跨层风险，为QKD协议的设计与标准化提供了可验证的改进方向。适合QKD协议设计者、密码学标准化人员以及形式化方法安全研究者阅读。

这篇论文针对两个主流的协议形式化验证工具 Tamarin 和 ProVerif 提出了首个从 Tamarin 到 ProVerif 的忠实的（sound）翻译方法，以支持系统性的对比分析。Tamarin 基于多集重写规则，验证是可靠且完备的；而 ProVerif 基于应用 pi 演算的扩展，验证速度更快但可能不完整。两者的底层形式化体系和验证技术差异很大，导致难以直接比较。作者开发了一种新翻译方法，包含公式重写、多集重写语义的编码以及对同时事件的处理，能够支持 Tamarin 的绝大多数特性，包括多集重写规则、引理和限制。同时，论文精确刻画了无法忠实翻译的情况，并通过形式化证明保证了在忠实翻译片段内的可靠性（soundness）和完整性（completeness）：若 ProVerif 验证成功，则原 Tamarin 模型中也成立；若 Tamarin 中存在某条轨迹，除非涉及攻击者知识，否则该轨迹在 ProVerif 中也被保留。对于非线性（XOR）等最佳努力编码，论文会单独报告，且不在上述保证范围内。实验部分在 121 个 Tamarin 模型上评估了翻译过程，共覆盖 566 个引理任务中的 562 个。在非 XOR 且两个工具都给出确定性结果的任务中，247 个里有 246 个结论一致，剩余的一个明确标注为使用了不完整模型。在 Tamarin 返回布尔结果且 ProVerif 返回逻辑结果的 362 个任务中，ProVerif 在 334 个任务（92.3%）上运行更快，每个任务的中位数运行时间比为 6.74 倍，峰值内存比为 6.24 倍。这项研究为安全协议分析工具的互操作和结果交叉验证奠定了基础，对形式化验证社区具有重要意义。

本文提出 HOPSCOTCH，一个基于 Lean 4 的框架，用于机械化计算可靠的、基于游戏的安全证明。安全定义被表达为有状态概率预言机之间的不可区分性，证明过程遵循标准的游戏跳跃范式。HOPSCOTCH 采用浅嵌入方式，预言机和归约都是普通的 Lean 定义，从而能够直接与 Lean 生态系统集成，包括 Mathlib 中的一般数学理论（如有限群论）。在 HOPSCOTCH 中，游戏跳跃证明被表示为一个显式的形式化对象，其构造子对应于游戏跳跃论证的标准步骤，使得证明更易于构造、自动化和检查。作者证明了一个通用计算可靠性定理，该定理通过针对所使用假设构造归约，并推导出任何区分器优势的具体上界，来解释这些证明对象。预言机之间的观测等价性通过状态抽象方法论建立：一种简单而强大的方法，支持添加或遗忘状态、将急切采样替换为惰性采样等变换。框架通过以下形式化证明加以展示：加密后认证（encrypt-then-MAC）的 IND-CCA 安全性、基于 DDH 假设的 ElGamal 加密安全性、从一次性保密性到公钥 IND-CPA 安全性的蕴含关系，以及 GGM 伪随机函数构造。据作者所知，最后一项是非恒定深度 GGM 的首个机械化证明。该工作主要面向对密码学形式化验证、定理证明器在安全协议分析中的应用感兴趣的研究人员，也适合希望构建可审计安全证明的系统开发者。核心贡献在于将游戏跳跃证明转化为可互相操作的形式化对象，并通过状态抽象简化证明过程，同时保持了与既有数学库的兼容性。

本文针对蓝牙低功耗（BLE）安全连接（Secure Connections）配对协议的安全性展开形式化分析。配对是 BLE 安全体系中的关键环节，决定了后续通信加密密钥的协商方式，因此其安全性直接影响设备间数据传输的机密性与完整性。作者构建了该协议的正式模型，通过验证脚本对协议逻辑进行严谨的数学推演，并实现了相应的攻击以验证理论发现。研究的核心贡献在于揭示了一种名为“PE 混淆攻击”（PE Confusion Attack）的新型安全威胁，该攻击利用协议中配对阶段参数（Pairing Element, PE）的语义歧义或验证缺失，可能导致攻击者混淆不同配对过程中的关键参数，进而削弱配对过程提供的安全保障。论文提供了完整的工件，包括模型、脚本和攻击实现，供后续研究者复现与深入分析。这项研究对于蓝牙协议栈实现者、安全审计人员以及物联网设备制造商具有重要参考价值，有助于理解 BLE 配对协议在形式化层面存在的设计缺陷，并为未来协议修订或补丁提供理论依据。本文仅基于论文摘要，具体攻击细节和技术路线尚未公开，但其揭示的协议漏洞方向值得关注。

本文研究Dolev-Yao模型中密码协议的参数化保密性验证问题。经典Dolev-Yao保密性问题询问协议是否无论执行多少次都不会泄露秘密，而参数化保密性则要求保密性在所有可能的系统规模（即参与者数量）上一致成立，其中规模被视为参数。这一视角能够刻画攻击如何随参与者数量扩展，并为小型实例分析在实践中的有效性提供了形式化基础。文章指出，即使在有界新鲜性或有界消息大小的限制下，一般意义上的参数化保密性也是不可判定的。然而，作者识别出两种使问题可判定的结构性限制：(i) 每个角色的全局有界新鲜性；(ii) Dolev-Yao入侵者被限制为良类型替换。在这些假设下，协议执行可通过一个对代理和项的折叠映射获得有限表示。主要成果是证明了在该设定下参数化保密性是可判定的，并得到了一个cut-off定理：即使系统允许任意多的会话，任何保密性违反都必定在某个有界大小的系统中被观察到。该cut-off是自包含的；更严格地，诱导的转移系统在基于界限的偏序下构成良结构转移系统（WSTS），因此保密性问题还可归约为WSTS中的覆盖性问题。这一结果为符号协议分析中有限见证的存在性提供了结构性解释，并将Dolev-Yao验证与参数化验证技术联系起来。本文属于理论计算机科学范畴，主要贡献在于可判定性结论和新的验证方法，对密码协议的形式化分析与验证具有重要理论意义。

该论文提出 CryptoProver，一个基于人工智能的系统，用于自动合成密码学库的内部规范，并生成经过 Verus 验证的证明。研究背景是：密码学代码是关键基础设施，必须正确无误，但现有形式化验证生产库仍然困难。已有的基于语言模型的证明系统只能解决给定规范和前提的孤立义务，无法完成整个生产库的验证。CryptoProver 从高级 API 契约出发，在不改变可执行代码的前提下，自动合成内部规范（internal specifications）和 Verus 检查过的证明。实验证明，CryptoProver 成功对 curve25519-dalek 构造了一个新的独立证明，并针对 RFC 8439 规范验证了 RustCrypto 中此前未经验证的 chacha20 实现。这些密码学库被部署在 Signal 和 Shadowsocks 等系统中，其中 Signal 的全球下载量估计为 2.18 亿次。作为对照，由人类主导的 curve25519-dalek 独立验证历时八个月，由五位主要贡献者公开开发。在给定 API 契约和固定的可信库（包含域规范、算术事实、公理和 vstd）后，CryptoProver 在 11.4 小时内合成了内部规范和证明，记录的 API 成本为 466.99 美元。CryptoProver 遵循信任优先的设计原则：机械门（mechanical gates）拒绝削弱规范、虚构公理和跨模块破坏，而隔离机制阻止参考证明的检索（包括从 git 历史中检索）。该工作展示了 AI 在自动化密码学代码形式化验证方面的潜力，有望降低人工验证成本并提高验证覆盖率。适合对形式化验证、AI 辅助代码分析以及密码学库安全保证感兴趣的从业者阅读。

零知识证明（ZKP）已成为隐私和可验证计算的核心技术，广泛应用于保护处理数十亿美元的数字货币区块链以及处理敏感个人数据的身份应用。然而，ZKP系统复杂，细微的实现错误可能完全破坏其安全保障，使攻击者能够伪造货币或身份证明。为此，研究人员和从业者开发了越来越多的漏洞检测和形式化验证方法来确保这些系统的安全性。但它们的实际有效性和采用情况仍不明确。本文旨在阐明ZKP安全工具的现状。首先，我们系统化了这些工具的格局，发现大多数工具针对Circom，而对较新的DSL和zkVM的支持有限。接着，我们使用六个工具对70个真实世界漏洞进行了评估，发现这些工具在隔离目标上检测到45.7%的漏洞，但在完整代码库上，检测率降至19.6%，且重要的漏洞类别未被覆盖。我们还首次对形式化验证工作进行了系统分析，揭示当前工作主要集中在约束正确性上，并指出了关键差距和风险。最后，我们对48位从业者进行了调查，结果显示开发和安全性仍然以人为主导，LLM被广泛使用，从业者更青睐具有更清晰保证和更低集成难度的工具。总体而言，我们的结果强调了将安全工具更好地集成到开发和审计过程中的必要性，并为研究人员和从业者提供了可操作的见解。本文适合需要了解ZKP安全工具现状、有效性及挑战的安全研究人员、区块链开发者以及审计人员阅读。

该论文提出 DualityCert，一个专为四维 N=1 quiver 规范理论中 Seiberg 对偶性声明设计的符号验证器。验证器检查 't Hooft 异常匹配、超势 R-荷一致性、中心荷匹配以及一个有界的手征环代理。通过验证的声明获得一致性证书，但仅表明未发现被测试的不一致性，而非证明对偶性成立。研究者将验证器作为语言模型代理的修复环境：代理接收一个故意被破坏的声明，并编辑它直至通过验证。在包含 145 个被破坏声明的预注册基准上（分析在第一次确证模型调用前固定），验证器门控重试相比单次尝试将最终修复成功率提升了 +8.3 个百分点（deepseek-chat）和 +7.1 个百分点（qwen-plus，Holm 校正 p<0.002）。在相同预算（11 次尝试）下，停止优先策略组合在 deepseek-chat 上弱于独立验证器过滤重采样 10.3 个百分点，但在 qwen-plus 上反而强 14.7 个百分点，逆转了两种验证器利用策略在两个确证模型上的顺序。在 qwen-plus 上，类别级验证器反馈相比无内容重试提升 +8.7 个百分点，而可解释的义务恒等式单独相比结构相同但被掩码的反馈提升 +6.4 个百分点；在 deepseek-chat 上未检测到这些效应。另外，预注册的 MiniMax-M2.5 扩展实验再次观察到迭代收益，且独立验证器过滤重采样优于策略组合。因此，哪种策略更优因模型而异，而所有获胜策略都使用了相同的廉价证书。该论文发布了验证器、基准、协议及所有逐次尝试记录。该研究展示了符号验证器与语言模型代理结合的有效性，对 AI 辅助科学推理和形式验证领域具有参考价值。

该论文针对LLM辅助自主机器人蜂群在执行协作情报、监视与侦察（ISR）任务时面临的组合保证失败问题，提出了一种三层（平台/小队/任务）组合运行时验证框架。首先，论文指出现有的单平台防护机制无法检测跨平台违规行为，例如多个平台各自执行合规动作但共同违反任务策略（如分散执行禁止目标或集体超预算）。其次，在有争议的通信环境下，违规行为可能因证据丢失或延迟而隐藏。为此，论文设计了一个将任务策略分解为单智能体与跨智能体方面的框架，并通过验证感知的消息传递汇聚每个平台的判定结果，进而采用一种基于证据的两轴（安全性与完整性）代数进行融合，并标注出共同触发违规的平台来源。该框架能够将未支持的负面判定降级为明确的“未知”状态，而非报告为全队安全。在模拟ISR任务中，一个针对真实LLM规划器的间接提示注入攻击导致四个平台分开执行被禁止的收集任务，该攻击在每个单平台监视器中均不可见，但被组合框架检测并给出完整溯源；在注入故障场景下，尽力而为的中央监视器输出虚假的全局安全信号，而验证感知消息传递则不会产生此类误报。该工作为LLM辅助蜂群系统的运行时安全保障提供了可组合、可溯源的解决方案，尤其适用于通信不可靠、需要高完整性保证的对抗环境。

Rust语言的所有权模型和类型系统提供了强大的内存安全保障，但unsafe代码和运行时panic依然带来显著风险。形式化验证是确保内存安全的关键，然而开发验证harness（验证框架）是一项具有挑战性的手动任务。虽然大语言模型在各类代码分析任务中表现出色，但直接将其应用于harness生成往往导致API调用不准确、非确定性数据生成低效以及虚假的修复。本文提出HarnessLLM，一种自动化工作流，利用LLM直接从现有测试套件为Rust代码生成验证harness。HarnessLLM自动从测试用例中提取调用场景，基于依赖分析生成非确定性参数，并增量式合成harness。随后迭代优化harness，保留关键代码区域，并将虚构的类型或函数报告给LLM进行修正。在9个真实世界Rust代码库上的评估中，HarnessLLM从494个测试用例中提取了294个调用场景，准确率94.66%，平均每个场景生成harness耗时145秒。其性能优于现有方法Autoharness，后者仅能处理41%的场景。最终，生成的harness检测到6个真实内存安全漏洞，证明了该方法在验证中的实用价值。据作者所知，这是首个利用LLM为真实Rust项目生成面向内存安全验证的harness的工作。

该论文提出了 KaPilot，一个基于大语言模型（LLM）的多智能体框架，用于自动生成 Rust 语言中 unsafe 代码内存安全的形式化规约（specifications），以支持使用 Kani 验证器进行形式化验证。Rust 的所有权和类型系统提供了强内存安全保证，但 unsafe 代码仍存在内存安全风险。形式化验证可以确保内存安全，但为 unsafe Rust 编写精确规约具有挑战性且高度依赖人工。LLM 在生成形式化规约方面显示出潜力，但通常以代码为中心，容易继承实现缺陷，且缺乏系统化的质量评估。KaPilot 流程首先进行轻量级程序分析和证明桩生成。SafetyReq 智能体从目标 Rust 函数的文档中提取精炼的安全需求列表，引导 SpecGenerate 智能体生成初始规约，指定内存安全问题。然后，通过包含 SpecGenerate、SpecPrecheck 和 SpecVerify 智能体的生成-预检-验证循环迭代优化规约，评估质量并反馈错误。多次执行该循环后，KaPilot 生成一组候选规约。最后，应用 shuffle（打乱）和 implication（蕴含）策略系统地从候选中确定最佳规约。作者在 54 个具有真实标注的 unsafe Rust 函数和 70 个无标注的函数上评估了 KaPilot。在有真实标注的数据集上，规约生成成功率达到 88.9%；在无标注数据集上为 71.4%。其中 57.4% 的生成规约与真实标注等价或更强。与 AutoSpec 基线相比，KaPilot 生成了多 14.8% 的可验证规约和多 25.9% 的等价或更优规约。该研究展示了 LLM 在自动化形式化验证规约生成方面的潜力，为提升 unsafe Rust 代码安全性提供了新方法。

该论文针对 AWS Cognito 服务中跨服务缺陷的识别与形式化验证问题展开研究。AWS Cognito 作为一项用户身份与访问管理服务，常与 API Gateway、Lambda 等其他 AWS 服务集成，这种跨服务组合可能引入安全漏洞。作者提出了一种名为 C-Verifier 的形式化验证框架，能够自动建模 AWS Cognito 的配置及其与其他服务的交互行为，通过符号模型检测技术发现潜在的跨服务逻辑缺陷，例如权限提升、未授权访问等。该方法首先将 AWS 资源配置抽象为形式化模型，然后利用 SMT 求解器对安全属性进行验证。实验结果表明，C-Verifier 在多个真实世界的 AWS 架构中成功识别出未知的跨服务漏洞，并提供了形式化证明。该工作的主要贡献在于：首次将形式化验证系统性地应用于 AWS Cognito 的跨服务场景，提出了可扩展的建模方法，并实际发现了若干高危缺陷。适合云安全研究人员、AWS 服务开发者以及安全工程师阅读。

本文针对高保证密码学协议形式化验证实现中存在的性能瓶颈问题，提出了一套通用的优化方法。以 Line-Point 零知识证明（LPZK）协议为案例，首先在 EasyCrypt 中实现了一个形式化验证的 LPZK 实现（未考虑性能），然后通过三步优化获得高达 3000 倍的加速，最终性能与手动优化版本 lpzkv2 相当。三步优化包括：修改算法规范以减少计算复杂度、采用可证明安全的并行执行模型、以及优化内存访问结构。每一步优化都在 EasyCrypt 中形式化验证，并自动合成可执行代码。论文详细分析了每步优化带来的性能提升，并讨论了自动化安全证明和代码合成面临的挑战。该工作表明，通过系统的形式化优化，可以在不牺牲安全性保证的前提下显著提升验证密码学实现的性能，为高保证密码学的大规模应用提供了可行的技术路径。

该论文探讨了高效模型检查与安全处理器设计之间的相互作用，以安全推测（Secure Speculation）为案例。针对推测执行侧信道攻击（如Spectre）带来的安全威胁，传统缓解措施往往带来显著的性能开销或设计复杂性。论文提出一种形式化方法，通过模型检查技术对处理器推测机制进行安全性验证，并在此过程中优化模型检查的效率。具体而言，作者将安全属性建模为时序逻辑公式，利用符号模型检查器对处理器微架构进行自动化验证，识别出潜在的推测执行信息泄露路径。为应对状态空间爆炸问题，论文采用抽象-细化循环和启发式剪枝策略，将验证时间从指数级降低到多项式级。实验基于RISC-V处理器原型实现，测试了多种推测执行窗口配置，结果表明该方法能发现已知缓解措施中未被覆盖的漏洞，同时验证了主流防御（如流水线冲刷、延迟加载）的正确性。该工作强调了硬件设计阶段纳入形式化验证的重要性，为处理器设计人员提供了在性能与安全之间权衡的系统性工具。

本论文针对 Rust 语言中解析和序列化操作的安全性与性能挑战，提出了一种名为 Vest 的新型框架。Rust 以其内存安全著称，但手写解析器和序列化器仍然容易出错且效率低下。现有方案（如 serde）虽提供自动化，但缺乏形式化验证，且难以应对复杂格式。Vest 结合了形式化验证与高性能实现：首先，用户使用一种安全领域专用语言（DSL）描述数据格式规范；然后，Vest 自动生成经过验证的解析器和序列化器代码。其核心创新在于利用符号执行和 SMT 求解器对生成的代码进行属性验证（如内存安全、无崩溃、格式合规），同时通过编译器优化和运行时技术（如零拷贝、预分配）保持接近手写代码的性能。实验在多个实际数据格式（如 JSON、MessagePack、FlatBuffers）上评估，结果显示 Vest 不仅消除了常见漏洞（如缓冲区溢出、未定义行为），而且性能与 serde 相当或更优，在某些场景下提升高达 30%。该工作为 Rust 生态系统提供了安全与效率兼顾的解析/序列化基础设施，适合编译器工程师、形式化方法研究者及系统程序员阅读。

该论文提出 CryptoBap，一个用于验证加密协议二进制代码安全属性的平台。研究背景是：现实中的加密协议实现可能因编译器优化、平台差异或编程错误而引入安全漏洞，而传统的形式化验证方法通常针对高级语言或协议规范，难以直接分析编译后的机器码。核心问题是如何在二进制层面自动验证协议的弱保密性和认证属性。方法上，CryptoBap 首先将 ARMv8 和 RISC-V 架构的协议二进制代码反编译为中间表示（IR），然后执行密码感知的符号执行，自动提取覆盖所有执行路径的协议模型。符号执行过程支持间接跳转解析和基于循环总结技术的有限循环处理，完全自动化。提取的模型通过第三方工具链转换为 ProVerif 或 CryptoVerif 可接受的输入格式，从而利用这些成熟的自动验证器完成安全属性证明。论文证明了该方法的可靠性（soundness），并通过多个案例验证了平台的有效性，包括玩具示例以及真实协议 TinySSH（SSH 实现）和 WireGuard（现代 VPN 协议）。实验结果表明，CryptoBap 能够成功提取协议模型并验证安全属性，且运行效率可接受。该工作的主要贡献在于：1）首个结合二进制翻译、密码感知符号执行和自动验证器链的集成平台；2）针对 ARMv8 和 RISC-V 指令集的支持；3）对真实世界协议的成功验证。适合的研究读者包括形式化验证、二进制分析、加密协议实现安全性领域的研究人员。

该论文聚焦于安全协议执行中的细粒度可追踪性问题，提出了一种新的形式化框架，用于在协议执行中精确追踪参与方的身份、行为及其状态变化。研究背景是现有协议追踪技术通常粒度较粗，难以应对复杂攻击场景（如混淆代理、重放攻击）。核心方法包括定义一种扩展的迹语义（trace semantics），并引入可追踪性属性（trackability properties）的细粒度分类。通过案例研究（如Needham-Schroeder协议）验证了框架的有效性。实验表明，该方法能够揭示协议设计中隐藏的追踪漏洞，为改进协议安全性提供指导。主要贡献是建立了一个系统化的细粒度可追踪性分析理论，并提供了自动化工具原型。适合安全协议设计者、形式化验证研究人员以及关注隐私与问责制的安全分析师阅读。

本文针对认证数据结构（Authenticated Data Structures）的开发与实现正确性难题，提出了一种基于新关系分离逻辑的形式化证明方法。认证数据结构允许不可信的第三方执行操作并生成可验证的输出证明，但此类系统容易因实现错误导致安全漏洞。作者首先设计了一种关系分离逻辑，用于推理使用抗碰撞哈希函数的程序，该逻辑为类型系统构建了两个语义模型，从而阐释了如何通过类型抽象来强制实现安全性与正确性。基于这些模型，论文进一步证明了库中多项优化的正确性，并展示了如何将优化的、手工编写的认证数据结构实现与自动生成的代码安全链接。所有结果均在 Coq 证明助手中使用 Iris 框架完成机械化验证。该工作为认证数据结构库的可靠实现提供了坚实的理论基础，有助于减少此类系统中的安全缺陷。适合形式化验证、编程语言理论与安全协议交叉领域的研究者阅读。

该论文提出了一种名为 LeanDY 的形式化验证框架，面向密码协议的安全性分析。现有工具要么全自动但表达能力有限，要么交互式证明灵活但自动化不足。LeanDY 通过结合基于类型推理（type-based reasoning）与基于轨迹推理（trace-based reasoning），实现了状态化、无界协议的模块化验证。遵循语言与自动化协同设计原则，框架为协议提供定制化自动推理，同时保持高表达力。LeanDY 作为 Lean 证明助手的库实现，扩展了 DY* 的设计，融合协议特定自动化与交互式证明。它统一支持多种功能与安全需求，包括机密性、认证以及递归条件机密性（如 XOR 协议）。论文在 LeanDY 中形式化 SegWit 风格的区块链原语，并深入验证了基于此模型支付通道的惩罚机制和链活性属性，展示了框架的表达力。该研究适合对形式化方法、密码协议验证和区块链安全感兴趣的研究者。

本文提出 Xenon，一种求解器辅助的交互式形式化验证方法，用于证明 Verilog 硬件设计在常时执行。常时执行是抵御基于时序的侧信道攻击的关键属性。Xenon 通过引入常时反例的新概念，自动合成最小化秘密假设集合，并在交互式验证循环中定位验证失败根源，显著降低调试工作量。为加速验证，Xenon 利用 Verilog 模块摘要实现模块化，避免重复验证相同实例。实验表明，Xenon 能验证多种电路，包括高度模块化的 AES-256 实现（验证时间从六小时降至三秒）以及 ScarV 侧信道加固的 RISC-V 微控制器（规模比此前验证的设计大一个数量级）。小规模用户研究发现，Xenon 帮助非专家用户比现有工具更正确、更快速地完成验证任务。

该论文针对当前AI智能体系统在可信执行与合规验证方面的挑战，提出了一种基于密码学有效性证书的新颖方案。核心思想是：首先将智能体应满足的正确性或策略条件形式化为逻辑谓词；然后将该谓词编译为多项式约束上的证人（witness）检查问题；最后利用简洁的密码学证明系统（如SNARK/STARK），可选地结合零知识性质，生成一个独立可验证的证书，来证明智能体的某个动作确实符合约定的形式化策略。该方案在形式化源代码验证与密码学认证之间找到了一个平衡点：验证者无需信任智能体本身，也无需重新执行智能体的计算过程，仅通过检查一个紧凑的证书即可确信策略被遵守。论文从高层描述了该方法的架构，给出了从逻辑条件到多项式约束的核心数学转换，并将其与证明携带代码（PCC）、零知识虚拟机（zkVM）、形式化方法以及智能体治理等已有技术进行了关联讨论。最后，论文指出了完整实现所需面对的规范、审计和部署问题。该研究适用于AI安全、可解释AI、智能体合规等方向的研究人员与工程师。

本文提出了一种名为“语义非组合”（Semantic Non-Assembly, SNA）的新型隐私保证框架。与传统的基于保密性、访问控制或统计披露限制的隐私模型不同，SNA 从“暴露发生时信息收益”的角度定义隐私：即使攻击者能够完全暴露和解密某个子系统中的任意组件（低于阈值），也无法获得可操作数据。核心思想是阻止任何低于指定阈值的组件联盟组装出足以评估特定谓词的完整输入域赋值。该保证是结构性的，通过体系架构而非策略实现，且隐私属性在组件被攻陷时以可预测的方式退化，而非单点崩溃。参考实现将结构保证与经过审计的组织约束相结合（附录A形式化描述）。论文形式化了SNA保证，并使用ProVerif验证了四个关键属性：设备非关联性、注册观测器非识别性、提交服务器盲目性以及主动防御门正确性。前三个属性通过双通道溯源架构实现。Birthmark标准实例在受限捕获硬件上实现了该保证，展示了零知识证明方法计算不可行场景下的可部署性。所有形式化属性和范围限制均记录在附录A中。该工作适合对隐私架构、分布式系统安全及形式化验证感兴趣的研究人员阅读。

本文针对硬件信息流（information-flow）的形式化验证中可扩展性不足的问题，提出了一种名为“受保护等价谓词”（Guarded Equivalence Predicates）的方法。在硬件安全验证中，自组合（self-composition）技术将信息流验证转化为两个电路副本之间的安全性质检查，产生的关系性证明义务对通用的属性推演引擎（PDR）而言难以仅从位级逻辑中发现。最近基于PDR的技术利用副本对称性和全局跨副本等价谓词来利用这种重复结构，但当对应内部信号在整个可达状态空间中都不一致时，这些谓词效果有限，且无法捕获仅在特定控制上下文中相关的等式。作者观察到，在硬件信息流验证中，上下文相关关系自然存在：内部信号对可能只需在某个控制阶段、事务窗口、循环状态或协议区域内保持一致。为此，本文引入了受保护等价谓词，将该类关系暴露给PDR。与将提议的上下文等式作为假设不同，验证器将相应的失配条件作为辅助阻塞义务提交。保护条件是从关系性反例归纳（CTI）中通过CTI局部提取和状态分裂搜索提取的；只有后端证明不可达的候选者才会影响证明过程。在12个信息流验证基准测试和两个PDR后端的实验中，受保护谓词将两个上下文相关的基准超时转化为在1800秒时限内34.2-89.5秒内完成的证明，并在其他基准上将证明时间最多减少10.8倍。该方法为硬件安全验证提供了一种系统性的可扩展策略，尤其适用于需要检查不同运行轨迹下数据流一致性的复杂控制逻辑。

本文对 IETF RFC 8555 标准化的 ACME（自动证书管理环境）协议进行了深入的符号安全分析。ACME 是 Web 公钥基础设施（PKI）的关键组成部分，被 Let's Encrypt 等证书颁发机构用于签发超过十亿张证书，目前大多数 HTTPS 连接都依赖于通过 ACME 颁发的证书。然而，相比于 TLS 1.3 或 OAuth 等其他协议标准，ACME 的安全性尚未得到同等深度的研究。先前的形式化分析仅考虑了早期草案版本的密码学核心，忽略了 RFC 中许多安全关键的低级细节，例如递归数据结构、带有异步子协议的长时间运行会话以及多域名证书的签发。本研究通过构建详细的符号模型，全面覆盖了 RFC 中定义的各种消息流程和状态转换，利用符号分析工具自动验证了 ACME 协议的安全属性，包括认证、授权、隐私和抗重放等。分析发现了若干潜在的设计缺陷和实现风险，并提出了改进建议。该工作为 ACME 协议的标准化和安全部署提供了重要的理论支撑。

该论文针对基于云的物联网（IoT）访问策略中存在的安全风险展开研究。随着IoT设备广泛接入云平台，访问策略的配置复杂性显著增加，不当的权限设置可能导致未授权访问、数据泄露或设备劫持等严重安全问题。现有策略验证工具多针对单一云平台或通用网络策略，缺乏对跨云、多设备场景下IoT特有语义（如设备状态、事件触发）的考虑。为此，作者提出了P-Verifier系统，一种自动化的访问策略验证与缓解框架。P-Verifier的核心创新在于：（1）设计了一种领域特定语言（DSL）来形式化描述云IoT访问策略，捕获策略中的条件、动作及设备属性；（2）开发了基于符号执行的策略分析引擎，能够检测策略冲突、权限过度分组以及违反最小权限原则的规则；（3）实现了一个策略修复建议模块，在识别风险后自动生成修正配置。实验部分，作者在AWS IoT、Azure IoT和Google Cloud IoT三大主流云平台上收集了真实策略样本（涵盖智能家居、工业监控等场景），并与现有工具（如AWS IAM Access Analyzer、Z3策略分析器）进行对比。结果表明，P-Verifier在策略漏洞检测率上平均提升37%，误报率降低至5%以下，修复建议的采纳率超过80%。论文还展示了P-Verifier在检测因设备动态属性（如固件版本、位置变化）导致的瞬时策略违规方面的独特能力。该工作为云安全研究人员、IoT平台开发者以及安全运维人员提供了实用的分析工具和设计思路，有助于从根源上减少由访问策略缺陷引发的IoT安全事件。

本文对 Go 标准库 `crypto/internal/fips140/bigmod` 中的 `extendedGCD` 实现进行了形式化验证。该实现用于 RSA 密钥对生成中的扩展欧几里得算法，是从 BoringSSL 移植而来。然而，研究者发现了两处偏差：一是系数更新方式与原始实现不同，二是允许更大的输入域。第一个偏差导致算法不变量被破坏，第二个偏差使得原有证明不再适用。研究者修复了第一个偏差（性能提升平均 24%），并针对第二个偏差将 BoringSSL 的证明移植并扩展到更大的输入域。他们使用 Go 语言专用验证器 Gobra 证明了修复后实现的正确性和终止性，并借助 Lean 验证了一些非线性算术引理。验证过程表明，即使是经过充分审查的代码也可能存在细微错误，形式化验证是发现此类错误的有效工具，而 AI 代理可通过迭代优化不变量和引理来辅助验证。

本文介绍了使用Lean 4证明助手对StarkWare的S-two证明器中的代数中间表示（AIR）进行形式化验证的工作。S-two证明器用于在区块链上高效地证明用Cairo虚拟机语言编写的程序能够运行完成。该证明器通过一个代数中间表示（AIR）捕获Cairo语言的语义，该AIR断言存在满足特定代数约束的有限域值表。然后，加密交互式证明系统circle STARK提供一个高效验证的证书，证明AIR是可满足的。本文的核心贡献在于，利用Lean 4证明助手对AIR编码的可靠性（soundness）进行了形式化验证，即证明AIR的可满足性蕴含相应的计算性声明。这一验证确保了AIR编码不会错误地声称一个无效的程序运行完成。论文详细描述了验证过程，包括如何在Lean 4中形式化AIR的语义、约束以及soundness证明。该工作对于提高Cairo智能合约和区块链应用的安全性具有重要价值，因为它提供了一个数学上严谨的保证，防止因AIR编码错误导致的虚假计算声明。读者包括对形式化验证、区块链安全性以及零知识证明感兴趣的研究者和工程师。

本文提出了首个经过机器检查的OpenZeppelin重入防护模式正确性证明，该证明针对生产部署的Solidity源代码的Lean 4状态机模型。所有十三个定理都经过了机器检查，没有使用任何“sorry”或用户引入的公理，公理足迹仅由[propext]（一个标准的mathlib4公理）限定，并集成在持续集成中。智能合约重入攻击自2016年以来已导致超过5亿美元的损失，其中DAO 2016攻击盗取了约360万ETH，并迫使以太坊硬分叉。OpenZeppelin ReentrancyGuard模式是生产DeFi中的事实标准防御措施，但此前没有工作建立其判别能力：即该防护能阻止对易受攻击实例的攻击，保持非攻击交易的正确执行，并区分相邻的安全和易受攻击变体。以往的工作要么形式化了玩具合约上的防护正确性，要么形式化了孤立实例上的攻击可行性，但未同时涵盖两个方向及针对生产源码的边界情况。本文通过变异测试验证了三种生产实例：DAO 2016、Compound v2和Aave V3的flashLoan，以及Aave V3 flashLoan的一个最小差异突变体（flashLoanVulnerable），该突变体隔离了一个安全关键差异。三方向结构包括：(a) DAO 2016模式的攻击复现，(b) Compound v2的正确性证明，(c) 区分Aave V3符合CEI模式的flashLoan与突变体的边界案例证明。一个顶层的元定理在“无改造”原则下组合了这三个方向，并在首次跨协议压力测试（从Compound v2到Aave V3）中进行了演示；更广泛的家族可移植性是未来工作。完整的Lean 4源码、CI配置和复现命令可在GitHub上获取。

该论文针对AMD SEV（安全加密虚拟化）技术缺乏形式化安全保证的问题，提出了一套形式化验证框架。AMD SEV是机密计算中的关键技术，通过硬件内存加密保护虚拟机内敏感数据。然而，现有实现缺乏对安全性属性的严格证明。研究首先对AMD SEV规范进行设计级和属性级抽象，建立精确的模型，然后通过属性检查（property checking）验证机密性、完整性和可用性（CIA三元组）。该方法为定义和验证执行环境的关键安全属性提供了严谨的数学基础。实验表明，该框架能够有效捕获规范中的安全约束，并发现潜在的安全缺口。该工作适用于安全架构师、云服务提供商和形式化方法研究人员，有助于提升对AMD SEV安全性的信任度。

该论文提出了一种全新的方法，用于形式化规范指令集架构（ISA）的安全保证。传统上，ISA的规范仅限于功能方面，且通常以非形式化的散文形式描述，缺乏对安全保证的精确刻画。作者引入了通用契约（universal contracts）的概念——这是一种软件契约，能够表达任意不可信代码的权限边界。通用契约独立于软件抽象层次，既能为软件推理提供必要的细节，又保留了ISA设计者和CPU实现者的实现自由度。论文的核心贡献包括：（1）提出了一种通用的、可平衡硬件实现与软件客户端需求的形式化安全保证规范方法；（2）开发了Katamaran工具——一个半自动化的分离逻辑验证器，用于Sail语言描述的ISA语义，能够生成机器可检查的证明；（3）通过两个差异显著的ISA实例验证了方法的通用性：自定义能力机ISA（MinimalCaps）和带有物理内存保护（PMP）的简化RISC-V。此外，作者还利用为RISC-V with PMP形式化的安全保证验证了一个femtokernel。实验结果表明，该方法能够支持在存在对抗代码的情况下对安全关键软件进行非形式化和形式化推理，同时确保硬件实现与安全契约的一致性。该工作为建立高置信度的处理器安全基础提供了形式化工具和方法论。

该论文提出了一种结合大型语言模型（LLMs）与形式化方法的智能合约验证新框架。当前智能合约验证面临两大挑战：自然语言表达的属性内在存在歧义，且LLM的答案缺乏正确性保证。作者通过两个创新点同时解决这些问题：1）设计了一种扩展Solidity语言的正式规范语言，支持抽象类型，使得属性表达无歧义；2）开发了一个工作流，将LLM与类型检查和具体执行相结合，自动生成并验证违规见证（即反例）。其核心思想是将规范编码为包含存在量化抽象类型变量的Solidity测试；通过为这些变量实例化具体值（符合正确类型），测试将转换为可执行的反例（概念验证），直观展示属性为何被违反。作者将该流程实现为工具Neuroforger，并在来自文献的智能合约验证数据集上实验评估，获得了有前景的结果，证明了其在真实场景中的潜在适用性。本文适合对智能合约安全、形式化验证及LLM应用感兴趣的读者。

该论文针对形式化验证工具ProVerif和Tamarin在安全协议验证中的使用门槛问题，提出了一种系统化的、基于证据的安全属性分类法。通过系统综述2022-2025年间使用这两种工具的53篇近期研究，论文提取并整理了当前被实际验证的安全属性集合，将其分为多个类别并给出非形式化的直观定义，同时用一阶逻辑给出了严格的形式化定义以确保清晰性和一致性。此外，论文还提供了在ProVerif和Tamarin中建模这些属性的通用模式，并在开放仓库中收录了可执行的示例代码，从而弥合了理论安全属性定义与实际可执行验证模型之间的鸿沟。该工作有助于安全协议设计者（而非形式化验证专家）更便捷地使用形式化工具来表达和验证协议的安全需求，对推动形式化验证在安全社区的普及具有重要意义。

本文针对大型语言模型从有限生成引擎向具有广泛执行权限的智能代理转型过程中出现的失控问题，提出了一种基于逻辑推理基本局限性的新型安全范式。现有防御架构主要依赖经验性语义护栏和概率性大模型裁决器，无法在复杂语义符号解耦攻击下提供确定性安全下界。为克服这一困境，作者提出了一种可执行证明约束动作（ePCA）框架，采用神经符号隔离架构。该框架放弃对自然语言的语义信任，强制代理在执行物理操作前将其意图无损形式化为一阶逻辑数学约束，从而确保决策的可验证安全性。在宏观和微观二维动态对抗系统中的实验评估表明，该形式化验证机制在评估场景中实现了零攻击成功率和零误报率，且计算延迟极低。本文为构建未来智能系统的底层防御基础提供了在明确系统假设下的条件形式化基础和工程范式。适合AI安全研究员、大模型应用开发者及安全架构师阅读。

本文针对操作系统内核中 I/O 分离不足导致的安全问题，提出了一种形式化的 I/O 分离模型。该模型基于 I/O 传输授权定义分离策略，与具体硬件无关，能够防止恶意驱动通过操控设备绕过 I/O 隔离。作者在 Dafny 语言中对该模型进行了形式化规约、精化以及在 Wimpy 内核设计中的实例化验证，并自动生成了经过验证的正确汇编代码。通过形式化建模，发现了原 Wimpy 内核中先前未知的设计与实现漏洞。最后，论文概述了该模型在其他 I/O 内核上的适用性。本研究为高可信的 I/O 安全内核开发提供了理论基础和自动化工具，适合操作系统安全、形式化验证领域的研究者阅读。

该论文聚焦于Linux内核扩展程序eBPF的安全迁移问题。eBPF程序被广泛用于网络、可观测性及安全策略执行，但其内核验证器仅检查低级内存安全和终止性，未强制许多高级源级属性，如初始化规则、schema一致性或错误处理。作者识别出六类源级bug，这些bug能够通过编译和内核验证，但会导致数据静默损坏、将先前跟踪的事件泄露至用户空间，或产生错误的执行结果。其中，作者发现了十款开源eBPF程序中此前未报道的信息泄露：这些程序中的环形缓冲区或栈驻留事件记录会将完全可解码的先前跟踪事件（包括用户标识路径和足以恢复每个事件KASLR偏移的内核返回地址）泄露到用户空间。为加固这些被验证器接受的缺陷程序并支持安全迁移，作者提出了Heimdall——一个自动化流水线，利用大语言模型（LLM）将遗留的libbpf C程序翻译为基于Aya Rust的eBPF程序。Heimdall迭代修复编译和内核验证失败，通过静态分析安全引擎拒绝Rust-Aya中不安全的逃逸机制，并借助符号执行和Z3等价性检查逐程序证明翻译后程序与原始程序行为等价。在102个eBPF程序上的实验表明，Heimdall成功生成了96个经形式化验证等价（94.1%）的翻译版本。Heimdall是首个能够自动化地将生产级eBPF程序迁移到内存安全语言，并为每个翻译程序提供形式化保证保持可观测行为的系统。

本文介绍了首个基于机械化证明的后量子安全协议验证方法。作者提出了PQ-BC，一种针对量子攻击者计算安全性的计算一阶逻辑，并实现了对应的机械化支持工具PQ-SQUIRREL。该工作基于经典的BC逻辑及其在SQUIRREL证明器中的机械化实现。PQ-BC的发展需要使BC逻辑对单一交互式量子攻击者保持完备性。作者通过修改SQUIRREL，依赖PQ-BC的完备性结果并强制执行一组语法条件，实现了PQ-SQUIRREL证明器；此外，还提供了新的策略来扩展工具范围。利用PQ-SQUIRREL，作者进行了多个案例研究，提供了首个机械化的后量子安全性证明，包括两个通用的基于KEM的密钥交换构造、IKEv1和IKEv2的两个子协议，以及Signal的X3DH协议的一个后量子变体。此外，他们用PQ-SQUIRREL证明了几个经典的SQUIRREL案例已经具有后量子安全性。这项工作的贡献在于将形式化验证扩展到后量子设置，为安全协议的后量子安全性提供了自动化的推理工具。

该论文提出了Pramana，一个用于自治代理网络中的声明验证的协议层解决方案。在受监管领域中，自主代理对每个关键输出必须产生一个可审计的验证工件，记录声明内容、来源、执行者、时间和方式。当前的生产验证分为两个未标准化的方向：概率性判决模式（如自一致性投票、评审LLM集成）产生判断而非工件；而工件产生模式（如RAG、工具增强轨迹、生成器-验证器循环）产生特定于供应商的记录，外部审计员无法在不进行定制集成的情况下重构。Pramana定义了缺失的线路格式：每个关键代理输出被封装在一个类型化的ClaimAttestation中，包含四种变体（测量、推理、类比、引用），每种都配有针对记录源的verify()操作。对于测量声明和引用声明，verify()是确定性的；对于推理声明和类比声明，确定性则取决于预言机（在LLM支持下可审计重放）。这种四类分类源于古典印度认识论（pramana，有效知识的来源）。生命周期在TLA+中指定，并通过TLC在三个对称缩减模型上进行了全面验证：总共38,563个不同的可达状态，零个不变性违反。Python参考实现通过了84个测试。一个A2A和MCP的线扩展清单层叠了三个部署级不变性：可达性、SLA边界和离线可重新验证。一个探索性试点（n=100，2,275次评审调用）探讨了LLM作为代码生成中的评判者。最显著的观察是跨越语料库的40个百分点的原始FPR差异，与参考解决方案质量显著一致。该试点本身并不验证Pramana；结构论证和形式验证做到了这一点。

该论文针对大型语言模型（LLM）生成代码中可能引入安全漏洞的问题，提出了一种基于自然语言的规约与验证方法。传统形式化验证需要严格的规约语言，而现有利用LLM生成规约的方法效果有限。作者另辟蹊径，探索让LLM同时承担规约生成和组合验证的任务，且规约以自然语言表达。初步实验结果表明，该方法在小型基准测试中展现了潜力，能够通过自然语言描述的功能性规约，指导LLM验证代码实现的正确性，从而在代码生成阶段预防漏洞。论文属于初步研究阶段，尚未在大规模系统上验证，但为后续结合LLM与形式化方法提供了新思路。

本文首次对主密码保护的密码管理协议（M3PM）进行了系统性的形式化安全分析。密码管理器（PM）帮助用户管理登录凭证，缓解记忆大量密码的负担，而M3PM协议描述了客户端与PM服务器之间的交互：客户端使用主密码进行身份验证，服务器协助跨设备检索凭证。随着PM数据泄露事件频发以及用户对服务器滥用的担忧，确保服务器对主密码和凭证不知情至关重要。作者通过文档分析、流量分析和逆向工程等方法，从43个行业和学术界的PM中识别出事实上的M3PM协议。为了形式化M3PM协议的安全属性，他们在通用可组合（UC）框架内提出了一组理想功能。根据对手的知识类型，他们将针对主密码的离线猜测攻击分为四类。分析表明，43个PM中有38个至少易受一种离线猜测攻击，揭示了各种单主密码保护的M3PM协议在不同条件下无法抵抗此类攻击的情况。此外，他们还发现了一种预言机攻击，使被攻陷的服务器能够学习知名开源PM Passbolt的加密密钥，并证明1Password的双密钥机制为用户的主密码和凭证提供了强保护。

该论文提出了一种名为μCFI（微架构控制流完整性）的形式化验证方法，旨在解决现有控制流完整性（CFI）机制在微架构层面的安全漏洞。传统的CFI仅在软件或ISA（指令集架构）层面保证控制流安全，但无法抵御利用微架构侧信道或瞬态执行攻击（如Spectre、Meltdown）的控制流劫持。作者通过形式化建模微架构状态（如分支预测器、缓存、乱序执行单元）与控制流之间的关系，定义了微架构层面的安全策略。μCFI基于模型检验技术，能够验证处理器设计是否满足该策略，从而确保即使在微架构优化（如预测执行）下，控制流也不会被恶意操纵。实验在RISC-V处理器核心上实现，验证了多个已知攻击变种（如Spectre v1、v2）的缓解效果，并发现了新的潜在攻击路径。该工作首次将形式化验证应用于微架构CFI，为安全处理器设计提供了理论保证。

形式化验证是确保软件正确性和安全性的最高保证，但将其应用于大规模、不断演变的系统仍面临重大挑战。尽管大语言模型（LLM）在自动证明生成方面展现出潜力，但由于无法处理复杂的跨模块依赖关系或代码库及验证工具链的变化，它们在实际应用中常常失败。本文识别出根本问题在于语义-结构鸿沟：LLM基于语义代码模式进行操作，而形式化验证受刚性结构依赖约束，这种脱节导致脆弱且不可持续的证明。为弥合这一鸿沟，作者提出了一种自适应性验证的新范式，并实现了KVerus——一个面向基于Verus的Rust验证的检索增强系统，能够适应不断演变的软件环境。KVerus构建了包含代码元数据、引理语义和工具链细节的动态知识库，通过结合依赖感知的程序分析、语义引理索引和错误驱动的自我精化，它能够导航复杂的跨文件依赖来合成证明，并在面对常见的演化变化时自动修复证明。在三个单文件基准测试中，KVerus验证了80.2%的任务，优于当前最先进的AutoVerus（56.9%），并且在破坏性的Verus更新下退化更少。在三个具有跨文件依赖的仓库级基准测试中，KVerus实现了51.0%的成功率，而多轮提示基线仅为4.5%。最后，在Asterinas Rust操作系统内核中，KVerus生成了被上游接受的证明，验证了内存管理模块中23个先前未验证的函数（占证明代码的21.0%）。KVerus标志着向使现代安全关键软件的形式化验证成为可扩展且可持续实践迈出的重要一步。

本论文提出了一种面向自主网络防御的工具中介LLM架构（Stable Agentic Control），旨在解决现有方法无法为高对抗压力下的自主系统提供形式化保证的问题。研究背景源于安全运营中心（SOC）在敌对压力下配置端点检测与响应（EDR）策略的实际需求。核心方法包括：LLM代理使用确定性工具（如Stackelberg最佳响应、贝叶斯观测更新、攻击图原语）并操作有限动作目录，通过工具输出接口强制执行。作者利用Lean 4证明助理机器检查了一个复合Lyapunov函数（零sorry），证明了系统的可控性、从非对称传感器数据中的可观测性，以及对智能对抗扰动的输入-状态稳定性（ISS）鲁棒性，并给出两个推论将认证扩展到目录中的任何控制器或对手。在282个真实企业攻击图上，所有声明均有裕量成立。在成对攻击/防御遥测上，使用工具中介的Claude Sonnet 4控制器相比确定性贪婪基线将攻击者的预期收益（博弈值）降低了59%，且在四个温度下的40次运行中方差为零。使用Claude Haiku 4.5的控制器收敛到次优博弈值，但在额外40次运行中仍保持在目录边界内，表明架构稳定性不依赖于控制器能力。LLM的非确定性有助于创造性策略探索，而工具中介架构确保了系统稳定性。适合对自主防御、形式化验证、LLM应用安全感兴趣的研究人员和工程师阅读。

本文对FIDO2、CTAP 2.1和WebAuthn 2这一现代无密码认证协议族进行了形式化安全分析，并提出了后量子安全的实例化方案。研究者首先构建了这些协议的符号模型，涵盖了注册、认证、凭证管理等多阶段交互，并利用Tamarin Prover工具进行了自动化安全验证。分析揭示了在标准安全假设下协议能够满足预期的安全属性（如抗钓鱼、密钥泄露保护、绑定认证等），但发现了在特定场景下存在的设计缺陷，例如CTAP 2.1中某些消息序列可能导致不安全的凭证共享。基于这些发现，论文提出了两方面的贡献：一是给出了一个增强的、可证明安全的协议规范修正；二是引入了后量子密码原语（如基于格的签名方案），对协议进行了后量子安全实例化，并证明了其在量子计算机威胁下的安全性。实验评估表明，后量子实例化在性能开销上可接受，兼容现有硬件。该工作为大规模部署无密码认证提供了坚实的理论基础和工程指导。

本文对IETF QUIC协议记录层的安全性进行了系统研究。QUIC是传输层协议，其记录层负责数据包加密和头部保护，IETF标准第30版相比Google原始协议和早期草案有重大变化。作者首先提出了一种新的安全定义——带半隐式nonce的认证加密（AE with semi-implicit nonces），以精确刻画QUIC的隐私保护目标。他们证明QUIC使用的加密构造是通用构造的一个实例，该通用构造以标准AEAD安全方案和PRF安全密码为参数。通过形式化验证工具F*，作者对该构造进行了安全证明，并发现了短头部可塑性以及数据包计数器最低有效位数选择导致nonce机密性受限于特定弱点，进而提出了增强鲁棒性的改进方案。除安全模型外，作者还给出了记录层的具体功能规范，修复了草案中的多处错误后，证明了正确解密等关键功能的正确性。最后，他们实现了经验证内存安全、符合规范且具备安全属性的高性能记录层，吞吐量接近2 GB/s。面向防御者的价值在于：该工作为QUIC记录层的安全性提供了严格的形式化基础，揭示潜在设计局限并提出改进，有助于构建更安全的QUIC实现，并预防未来因实现错误或设计缺陷引发的攻击。

该论文提出了一种名为 SPECA 的基于规范锚定的安全审计框架。传统代码审计工具主要关注代码层面的漏洞模式，但对于由自然语言规范驱动的系统（如协议栈、共识实现、密码库等），其安全约束和正确性条件定义在规范中，代码级工具无法检测此类漏洞。SPECA 框架从自然语言规范中提取显式、类型化的安全属性，并基于这些属性通过结构化证明尝试推理来审计实现。该框架具备三种代码驱动审计所不具备的能力：规范依赖的检测、在共享属性词汇下进行受控的跨实现比较、以及可将误报分解为可解释的管道阶段可追溯的根因。实验部分，在 Sherlock Ethereum Fusaka 审计竞赛（366 个提交、10 个实现）中，SPECA 恢复了所有 15 个范围内的漏洞，并独立发现了 4 个被开发者确认的 bug。在 RepoAudit C/C++ 基准测试（15 个项目）中，SPECA 达到最佳公布精度（88.9%），并发现了 12 个超出已有 ground truth 的候选 bug，其中两个被上游维护者确认。多模型分析表明，能力更强的模型在属性范围内审计更忠实，将检测瓶颈从模型推理转移到属性生成质量。所有误报可追溯至三种根因：信任边界误解、代码阅读错误和规范解释错误，每种都提供了可改进的目标。

本文（系列第6篇）聚焦后量子密码学中基于NTT（数论变换）硬件的算术掩码组合安全性。布尔掩码的组合理论（NI、SNI、PINI）已成熟，但素数域上的算术掩码（NTT后量子密码的基础）缺乏类似理论。作者提出并形式化证明了素数域上PINI（Prime-Field PINI）的组合定理。核心见解是“更新参数”（renewal argument）：当在两个流水线阶段间施加新的随机掩码时，中间导线无论第一阶段的防护参数如何都会变得完全均匀。对于两个PF-PINI gadgets（参数k1和k2），经新鲜掩码组合的两阶段流水线满足PF-PINI(k2)，阶段1的多重性被完全消除。无新鲜掩码时，中间导线多重性可达k1，构成差分功耗分析的必要条件。作者在Lean 4中形式化了两个定理，包含18个机器检查的证明，零个“sorry”存根。他们还形式化地桥接了Barrett约简的代数模型与硬件忠实算术模型，并实例化定理以正式诊断微软Adams Bridge PQC加速器：其缺失阶段间新鲜掩码导致Barrett输出导线在一阶探针模型下非均匀，这一架构缺陷与三个独立实证分析一致。计算证据进一步表明“1比特屏障”在Barrett和Montgomery约简中具有普遍性。本文适合对后量子密码侧信道防护、形式化验证与硬件安全感兴趣的研究者阅读。