该论文处理的是一个在可验证计算工程中常被忽视的信任缺口：GKR 协议的可靠性界只能保证『关于某个算术电路的输出声明是可信的』，却无法保证『该电路确实编码了应用所期望的状态转移』。作者以稀疏 Merkle 树（SMT）的成员证明、非成员证明与状态更新为具体应用载体，在 Isabelle/HOL 证明助手内对这条从状态转移到 GKR 验证的完整信任链进行机器检验。 方法上分为若干层次。首先是编译器模型：它建立了电路接受与状态转移有效性之间的双向关系（而非仅有单向的可靠性蕴含），从而同时覆盖可靠性与完整性两个方向。其次是可复用的协议模型：把层归约（layer reduction）、wiring predicate 扩展，以及从外部导入的 sumcheck 可靠性结论组装起来，形成一个针对某个显式『链事件』的界；其组合定理把语义上的无效性传递到该界上，且 witness 在挑战实验之前就已固定，避免了先看挑战再选证据的隐患。作者特别强调使用具体解释（concrete interpretations）与前提激活（premise activation）来暴露『空洞假设集』——即假设集合在逻辑上被满足但语义上无内容的情况，这是仅靠一次干净编译无法发现的。 进一步的工作构造了精确的四次 KoalaBear 扩域，把基域上的电路对象提升到扩域，并在其陈述的挑战假设下建立分母为 p^4 的装配界。论文还附带了一个可执行的 Rust prover，通过 Creusot/Why3 合约提供部分实现层面的连接，并给出一个条件性定理，把成功的验证者执行轨迹与模型事件关联起来——但该定理依赖一个未被消解的值对应（value-correspondence）前提。作者明确列出未完成的部分：既未建立转录中的在线挑战分布性质，也未建立多轮 Fiat–Shamir 归约。因此其核心贡献是：在单一证明助手内完成编译器正确性与 GKR 装配模型的组合，并显式、诚实地刻画了遗留的实现义务与密码学义务。 适合阅读的人群包括：形式化方法与证明助手研究者、zkVM / 可验证计算与状态承诺（SMT、Rollup 状态根）方向的协议设计者，以及需要对证明系统实现做独立评估的安全审计人员。

该论文关注神经网络“机制编辑”的可验证性，即通过消融、权重编辑或激活引导，从模型中移除某一有害能力（或技能），同时尽量保留其他有用能力。现有做法通常只靠测试集验证编辑效果，但有限测试无法覆盖连续、无穷的输入空间，因此无法保证在所有输入区域都成功移除且不破坏保留能力。作者将可解释性与形式化验证结合，不再只认证“模型某电路计算什么”或“解释是否忠实”，而是认证编辑的行为效果：对于给定连续嵌入空间区域内的每一个输入，证明禁用某电路确实移除了目标技能，并同时可证明另一项技能被保留；这相当于信息流安全意义上的特征非干扰保证。方法上，作者从玩具级 ReLU 网络逐步扩展到标准 softmax+LayerNorm Transformer，利用可靠的边界传播替代精确求解器，使可处理的输入扰动维度提升约 9 倍。论文还给出一个重要的负面结论：任何有限、确定性的黑盒测试都无法证明能力已被移除，并构造了一个能通过穷举测试、却在一个可任意缩小的“幸存者口袋”上被证明失败的编辑实例。其保证适用于小型标准架构网络，并且与所有移除声明一样，前提是目标技能存在可判定的规格；现实世界中的危害可能并不满足这一前提。

本文针对二面体陪集问题（DCP, Dihedral Coset Problem）建立了一条“不可行性”（no-go）定理，属于量子算法与后量子密码学的交叉理论研究。DCP 是 Regev 于 2004 年提出并用于将格上学习带误差问题（LWE）归约到量子求解框架的核心问题之一，其若被高效求解，将对基于格的密码体制构成威胁，因此围绕 DCP 的量子算法设计长期受到关注。作者聚焦于 Regev 提出的“傅里叶采样 + 子集和测量”这一类模板：算法先构造子集和态、测量其低 n-1 位，然后利用剩余的“傅里叶标签”（Fourier labels）继续提取信息。本文证明：只要算法在子集和测量之后，从每个傅里叶标签中丢弃任意 ω(log n) 位信息，那么该算法必然无法成功求解 DCP。换言之，任何沿用该模板的算法都必须高强度、近乎完整地保留并使用傅里叶标签，否则注定失败。这一结论既给出了模板内部的硬性设计约束，也为后续算法设计者提供了明确的“有效方向”指南。作为主要应用，作者分析了 Simon 近期提出的算法（IACR ePrint:2026/1591，2026 年 8 月 11 日）：他们证明该算法在子集和测量之后，可以用“最高有效三分之一”的傅里叶标签以指数级小误差实现，因此落入上述通用 no-go 定理的适用范围，从而不能求解 DCP。为便于可验证性，作者还公开发布了用 Lean 4 形式化验证相关结论的代码。整篇工作的方法论特征在于：不是构造更快的攻击算法，而是用信息损失的角度划定一类算法的能力上界，并用机器可检验的形式化方法增强结论的可信度。适合量子算法、格密码与后量子迁移方向的研究者与评估人员阅读。

该论文针对电子发票在消费/报销侧长期存在的三个痛点——同一张发票可被重复提交报销、收票方难以验证真伪、数据集中托管在中心化机构从而形成性能瓶颈与单点故障——提出并完整实现了一套基于以太坊的电子发票系统。方法上，作者首先将发票生命周期形式化为一个带守卫（guarded）的标签迁移系统（labeled transition system），并在标准密码学假设与共识假设下证明了三条安全性质：(i) 报销唯一性，即一张发票至多被报销一次，即使参与方之间互不信任；(ii) 面额完整性，即任何通过验证的发票在 keccak256 抗第二原像性未被攻破的前提下与链上记录一致；(iii) 每个生命周期操作的授权健全性。核心不变量使用 Solidity SMTChecker 进行机器化验证，证明其在所有可达交易序列上归纳成立。架构上，每张发票被建模为一个不可互换、不可转让的 NFT 型代币，其状态在五个带守卫的子系统中迁移，并采用基于锁的协议，使“重复报销”在结构上不可表达（unrepresentable），而不仅仅是被检测出来。实现层面，作者用 Solidity 0.8 编写合约，并配套四角色的 Web 应用，在私有以太坊网络上进行评估：开票消耗 646,773 gas，完整报销低于 135,000 gas，所有操作均为 O(1) 时间复杂度，单节点吞吐可达 137 次开票/秒。此外，该经过验证的合约还被用作 LLM 报销智能体的安全外壳（safety envelope）：即使智能体内部的策略失效，合约也能可证明地拒绝不安全动作（重复、超额、伪造票据的报销请求）。所有代码与基准测试均已开源。该工作适合区块链安全、智能合约形式化验证、金融风控以及 LLM 智能体安全护栏方向的研究者与工程师阅读。

该论文研究如何让大语言模型（LLM）可靠地参与安全协议的形式化建模。背景是：安全协议（如认证与密钥交换协议）的安全性通常需要借助 Tamarin 这类形式化验证工具来证明，而把自然语言写的协议描述（RFC、规范文档）翻译成可验证的形式化模型，长期依赖形式化方法专家手工完成，成本高、门槛高。LLM 看起来是天然的翻译接口，但其输出在没有专家校验的情况下难以信任。 作者的核心观察是：真正的正确性瓶颈不在中间协议表示的语法是否合法，而在于语义是否准确——即模型是否错误理解了参与者、消息流向、密钥来源、加密假设或攻击者能力。基于这一判断，论文提出一个人机协同（human-in-the-loop）框架，用于生成可被 Tamarin 验证的安全协议形式化模型。 方法上，作者设计了一种协议中间表示（Protocol IR），作为自然语言解析与形式模型生成之间的“可人工审计的语义检查点”。该 IR 显式刻画六个关键维度：协议参与者、消息流、取值来源与溯源（value provenance）、密码学操作、证明目标（proof targets）以及妥协假设（compromise assumptions，例如长期密钥泄露、会话密钥泄露等攻击者能力设定）。在此基础上，作者进一步设计交互式界面，依据模型自身的置信度（confidence）突出显示不确定字段，引导用户优先检查对最终安全性结论影响最大的语义决策，之后才进入形式模型生成与验证阶段。 论文的定位不是取代形式化方法专家，而是让 LLM 产出可审计的语义草稿，再由 Tamarin 等验证工具对生成的形式模型进行机器检查，形成“LLM 起草 + 人工审计 + 工具验证”的闭环。作者公开了代码与验证工件（GitHub 仓库 TamarinAgent）。摘要未给出具体实验数据、评测基准或定量结果，因此实际提升幅度与局限性需查阅全文确认。

本文针对一个此前缺乏系统认识的问题展开研究：大语言模型（LLM）在密码协议的符号化验证（symbolic protocol verification）中究竟能起到多大作用。作者指出，LLM 已在软件工程与安全分析任务中表现出较强潜力，但其在密码协议形式化验证这一高度专业化、对正确性要求极严的领域中的实际能力尚不明确，因此开展了（据作者所述）首次系统性评估。 核心方法上，论文提出了一种基于证明的度量指标 CRoST（Coverage Rate of Solve Tree，求解树覆盖率）。该指标从验证器生成的证明骨架（proof skeleton）出发，衡量 LLM 自动生成的引理（lemma）与人工参考引理之间的相似程度，从而把“LLM 辅助验证的效果”量化为可比较的覆盖率数值。作者通过理论分析与实证验证两条路径论证了 CRoST 这一指标的合理性，使其不只是经验性的打分，而具备一定的解释依据。 实验结果显示：当前最先进的模型在协议验证任务上平均仅达到 38.82% 的覆盖率，但其中有 14.4% 的生成引理覆盖率超过 80%，说明 LLM 已经能够在一定程度上产出对验证真正有用的引理，并非完全无效。与此同时，论文揭示了三类明显的失败模式：一是面对复杂的多阶段协议时表现不佳；二是在朴素地扩大模型规模或采样规模时收益递减，暗示单纯 scaling 难以解决问题；三是产生可观的验证开销，即 LLM 生成的候选引理需要形式化验证器反复求解，代价高昂。 论文的贡献可归纳为：给出首个系统性的 LLM 协议验证能力评估、提出并验证 CRoST 度量、量化当前能力上限与失败模式，并据此为面向真实复杂协议的后续研究指明方向（如更好的引理筛选、搜索策略与开销控制）。该工作适合形式化方法与协议安全研究者、以及尝试把 LLM 引入验证工具链的工程团队阅读。

该论文关注一个在云权限治理中极具现实意义的问题：如何把自然语言描述的访问控制需求，可靠地翻译成形式化、可验证的授权策略。作者指出，这类转换并不只是语法层面的翻译，而需要对权限、约束与例外条件进行严格推理，即便当前最前沿的大模型也常常生成语义上违反真实授权意图的策略，即语法可能合法但授权行为错误。为支撑可量化研究，作者构建了 CedarInstruct 数据集，据其所述这是首个同时支持训练与语义评估、面向可形式化验证的 Cedar 策略合成的数据集：共包含 44 个领域的 5800 个场景，其中 1408 个场景刻画同一个合成组织，每个场景都配有经过验证的目标策略以及可执行的验证计划。基于该数据，作者提出 RAISE 两阶段训练框架：第一阶段是经过验证器筛选的监督微调（verified SFT），第二阶段是强化学习（RL），直接从形式化验证器的反馈信号中学习。研究中的一个关键发现是：SFT 之所以有效，主要是因为模型本身已经具备授权推理能力，只是未经训练时极少能写出合法的 Cedar 语法；一旦写得出合法策略，其推理往往是正确的。第二个发现是，SFT 之后，验证器信息“怎么用”比“用多少”更重要——作者比较了六种逐步消费更丰富验证器信号的 RL 实例化方案，只有 RAISE-OC 显著超越 SFT，其做法是把失败检查与符号反例转化为引导式探索，并用 off-context GRPO 从结果中学习。在约 5400 个已验证场景上通过 LoRA 微调，RAISE-OC 将 Qwen3.5-9B 在留出场景上的语义成功率提升到超过零样本 GPT-6 Astra 13.33 个百分点、超过 Claude Opus 5 16.26 个百分点，并且训练效果可迁移到独立构建的 CedarBench 基准。

当前主流神经网络推理依赖存放在高带宽显存中的稠密浮点权重矩阵，既受严重的内存墙瓶颈制约，也无法在以太坊虚拟机（EVM）等确定性虚拟机上原生执行。而在 Blum-Shub-Smale 模型下，对连续域上递归动力系统的终止性与算术不变量做验证一般是不可判定的。本文提出并对 WERR（Waves & Errors）与第三阶段轨道误差动力学（OED）进行了形式化验证与裸机实证验证。该非张量决策范式不存储任何权重，而是依据沿 Mandelbrot 集边界 ∂M 的一个 24 字节坐标种子 Θ=(c_x, c_y, zoom)，按需程序化地合成非线性决策边界。作者将递推 z_{n+1}=z_n^2+c 投影到模剩余环 Z/9Z 与定点域 Q_{16.16}，在 Lean 4（v4.34.1）与 Mathlib4 中给出十条机器验证定理，且不存在未证明猜想（无 sorry）。定理覆盖 I_3={0,3,6} ⊂ Z/9Z 的理想闭包、通用燃料受限停机性（≤9 步与 ≤12 步）、在 2^63-1 以下 Q_{16.16} 平方无溢出、边界逃逸敏感度的非常数性，以及参数化 EVM gas 上界（≤22,557，控制在 24,000 以内）。实验在 40 核双路 Intel Xeon 服务器上完成：向量化的 36 次迭代 CPU 内核 6.49 秒处理 10 万次决策（15,397 决策/秒，0 字节 VRAM，15.15 倍加速）；S 型离群门控在保留 89.60% 干净基线信号的同时抑制了 100.00% 的对抗性尖峰。适合形式化方法、去中心化/链上推理、EVM 计算与资源受限边缘部署方向的研究者阅读。

该论文研究的是资源解聚（resource disaggregation）架构下的访问控制问题。在这种架构中，内存、加速器等资源被从计算节点上物理分离，并通过网络被远程访问，从而提升资源利用率与共享效率；但代价是本地内核被移出资源访问路径，资源在不受信任的主机环境下被调用。若主机软件被攻陷，攻击者可能使用过期的授权（stale authority）、越权使用超出委派范围的权限，或复用本属于其他进程的权限。作者首先对二十二个既有能力（capability）系统做了系统化梳理，结论是没有任何一个系统能同时满足三点：与主机无关的进程权限校验、在资源侧执行权威性强制（authoritative enforcement）、以及在被撤销时即使远端授权状态尚未更新也能保持有效。针对这一空白，论文提出 SADRA——面向资源解聚架构的分布式能力访问控制系统。其核心设计是：将 SmartNIC 硬件与主机软件隔离，由该硬件在两点独立校验每一次跨节点请求，先是在计算节点侧针对发起进程的权限校验，再在资源侧针对当前权威访问状态校验；通过把进程能力、计算能力与资源能力相互链接，使这些校验只需使用本地状态即可完成，访问路径上无需跨节点协调。当分布式权限被撤销时，SADRA 在资源侧直接拒绝后续所有依赖该权限的访问，而无需等待远端节点同步更新；过期的能力状态则另行异步回收，因此访问拒绝不依赖回收完成。作者针对形式化架构模型证明了能力安全性、权限安全性、撤销可靠性与强隔离性，并用 SPIN 模型检验器验证了该形式化。原型基于 FPGA SmartNIC，实测聚合吞吐 89.5 Gbit/s，与非强制模式的基线（峰值 90–91 Gbit/s）处于运行间波动范围内，性能损耗极小；128 个能力子树的清理耗时 528 ns。

该论文提出 Steelhead——一种双模式共识机制，目标是兼得部分同步协议的高性能与异步协议在恶劣网络条件下的存活性。现有 DAG 类 BFT 协议通常二者只能取其一：部分同步提交规则在健康网络中快，但一旦网络状况超出同步假设就会停滞；异步规则虽能在任意网络条件下保持活性，却需要额外的通信和硬币协议，在正常网络下性能明显吃亏。Steelhead 的核心思路是在同一条 DAG 之上交错两套提交规则：每隔 k 轮由异步规则裁决，该轮领导者在投票结束之后才由公共硬币（common coin）揭示，从而实现领导者隐藏、抵御针对领导者的攻击；其余轮次仍由部分同步规则裁决。每个时间区间内，验证者会用各自的候选周期参数重放已提交的 DAG，统计期望消息延迟，选出延迟最小的周期；当输出停滞时回退到 k=1，以此保证活性。关键工程设计在于：除 DAG 区块本身之外不发送任何额外消息，连周期参数的协商也不依赖额外通信，并且只在需要隐藏领导者的轮次才开启硬币，从而大幅压低异步路径的开销。该机制对任意共享同一委员会的两种 DAG 提交规则具有通用性，作者给出两个实例：在 n>=3f+1 下组合 Mysticeti 与 Mahi-Mahi，以及在 n>=5f+1 下组合 BlueBottle 的两个变体。论文证明了安全性（safety）与活性（liveness），并在 Lean 4 中完成了机器化验证。仿真结果表明：网络健康时 Steelhead 与纯部分同步协议性能相当；当网络状况使部分同步协议停滞时，其表现接近纯异步协议；且在两种网络条件之间切换时都能快速自适应。适合分布式共识研究者、区块链节点与共识层工程师，以及关注形式化验证实践的安全团队阅读。

本文聚焦安全敏感嵌入式系统的信息流安全验证问题。信息流分析（IFA）是验证机密性与完整性的重要手段，但嵌入式系统天然具有并发性与时间相关性，导致既有 IFA 方法往往陷入两难：要么抽象过于粗糙而精度不足、无法判定非法信息流是否存在，要么保持高精度但分析代价（时间/状态空间）高到难以实用。作者在前期工作基础上提出用“自动抽象精化（automatic abstraction refinement）”来缓解这一矛盾：其核心思想是基于状态之间的依赖关系以及已经检测到的潜在信息泄漏迹象，设计启发式策略来自动选择抽象层级——发现可能泄漏时精化抽象以保留细节，依赖关系简单时则采用更粗的抽象以压缩分析开销。前期方法已利用符号执行精确刻画进程间的数据依赖、控制依赖、时序依赖与事件依赖，并用抽象解释对取值进行符号化表示，但抽象层级必须由人工定义；本文的新贡献正是把这些层级的选择交给精心设计的启发式规则自动完成，目标是在可接受的分析时间内保留足以判定“非法信息流是否可能发生”的信息量。作者针对系统设计语言 SystemC 实现了该方法，并在若干共享总线架构上给出实验结果，验证了方案的可行性。论文属于程序设计语言与软件工程（cs.PL、cs.SE）方向的形式化验证研究，适合从事嵌入式/SoC 设计验证、形式化方法与硬件安全属性验证的研究者与工程师阅读。

该论文针对 SSH 通道完整性，提出一个在“部分选定状态”（partially chosen state）下形式化建模的框架，以回答 Terrapin 攻击（USENIX Security 2024）留下的开放问题：在 Terrapin 攻击中，SSH 通道状态被当作攻击向量，不同 AEAD 模式受影响程度不一，而“未受影响”是否等于“安全”尚不明确。作者指出现有安全通道形式化模型基于有状态加密，却未定义通道状态是什么、以及状态如何作为不同 AEAD 模式的输入，因此无法精确刻画此类攻击。论文的核心方法是将 SSH 序列号建模为被攻击者部分选定的状态，并定义一个抽象的有状态加密接口，为 SSH 中八种最主流的 AEAD 模式给出伪代码描述。通过改变发送（SND）预言机，模型可覆盖仅密文（CO，即 Terrapin 攻击）、已知明文（KPA）与选择明文（CPA）三类攻击，从而给出各 AEAD 模式的具体安全界。主要发现：三种 Encrypt-then-MAC（EtM）模式与 ChaCha20-Poly1305 在 CO 模型下均不安全；AES-GCM 是唯一在三种模型变体下均安全的方案。进一步地，作者证明 Encrypt-and-MAC（EaM）配合 CBC 即使在 KPA 模型下仍安全，并提出一种新的类 BEAST 选择明文攻击，可破坏 EaM-CBC 的通道完整性，从而在该方案上区分 KPA 与 CPA 模型。该工作适合密码学与协议安全研究者、SSH 实现维护者及安全架构师阅读。

该论文针对无状态 UTXO（未花费交易输出）风格的账本执行模型提出了一套名为「递归不变量」（Recursive Invariants, RI）的交易级逻辑与工具链，用以支撑多步工作流。背景问题是：UTXO 模型只依据本地数据和被引用数据即可验证交易，天然支持并行验证，且序列化体积/权重可预测；但多步业务流程必须显式地把状态在输出中逐级传递。作者指出一个关键缺口——预先构造好的「下一步交易」可能因为另一笔合法的花费先被确认而失效，于是链下跟踪、冲突处理与交易重建等一致性维护负担被推到了协议边界，带来协调成本与时延上升。 RI 的核心思路是：把工作流规则写成对某笔交易的输入与被索引的后继位置的谓词（predicate），而不是把可执行逻辑或共享可变状态附着在输出上。当某个被引用的后继交易被接受时，被接受交易会在「一步之后」重新检查其前驱的 RI，从而把工作流规则向前携带；连续的单步检查既保持了验证期局部性，又使验证工作可被明确归责与计量。由于许多后继子句在当前交易被验证时并不可判定，作者设计了一个小型静态类型 DSL，采用 Kleene 式三值语义（真、假、未知），把依赖未来的义务推迟到可检查的时刻。 论文形式化了该模型下的 UTXO 验证与账本扩展规则，刻画了「验证期可求值的一步片段」，证明了演绎系统相对三值语义的可靠性（soundness），并给出对应的交易验证算法与账本扩展算法。一个原型 RI 解释器与基准测试工具链评估了六个源自实践的流程；报告出的轨迹显示累计验证成本代理指标近似线性增长，同时展示了分阶段约束能力，且无需为每一步预先承诺一个已构造好的后继交易。 适合读者：区块链协议与智能合约研究者、UTXO/无状态执行模型的设计者、形式化方法与程序语言（三值语义、类型系统）方向的研究者，以及关注交易验证可并行性、可计量性与链下协调成本的工程团队。

本文提出 Hydrozoan，一个面向混合故障模型的 DAG（有向无环图）共识协议。背景是：基于 DAG 的共识可达很高吞吐，并在 n=3f+1 的经典设定下达到最优的三消息延迟下界；已有的两消息延迟协议要么靠牺牲容错度（例如需要 5f+1 规模的委员会）换取，要么依赖回退路径，从而丢掉 DAG 本身的高吞吐优势。Hydrozoan 的核心思路是把故障模型从单一拜占庭故障扩展为混合模型：f 个拜占庭故障验证者加 c 个崩溃故障验证者，验证者总数为 n = 3f+c+2p+1。协议为每个 leader 设计了两条提交路径：当故障验证者不超过 p 个时走两消息延迟的快路径，否则走三消息延迟的慢路径；切换不需要额外消息、不需要视图切换（view change），并且每轮允许存在多个 leader。两条路径复用同一张 DAG，作者提出一种新的“分级间接规则”（graded indirect rule）来协调两条路径的判定结果，保证所有诚实验证者最终达成一致决定。作者进一步指出，在地理分布式部署下，哪条路径更快其实取决于地理位置而非协议本身：需要跨到远端区域的轮次开销远高于不跨区域的轮次。因此 (f, c, p) 三个参数相当于可调旋钮，把“快速仲裁集”放到部署拓扑真正需要的位置，从而在两消息延迟内完成提交；即使参数配置失当，Hydrozoan 仍可退回三消息延迟，因为它以两条路径中先触发者为准进行提交。此外还给出变体 Optimal-Hydrozoan，可在快路径上多容忍一个故障，是首个匹配已知下界的构造。两个协议的安全性（safety）与活性（liveness）均在 Lean 4 中完成机器化验证。地理分布式评估显示：Hydrozoan 的吞吐与 Mysticeti 持平，在快速仲裁集恰好落在低延迟区域时提交速度约快 25%，而在不满足该条件或故障数超过 p 时平滑回退到三消息延迟，而已有两消息延迟协议在此情形下会停滞。

该论文聚焦于硬件形式化信息流验证（Information-Flow Verification, IFV）在真实 RTL 上难以扩展的问题。IFV 能为「无秘密依赖的时序与控制行为」提供强保证，但在实际设计中，证明往往因求解器规模爆炸而超时。作者在 self-composed IFV（把待验证设计与其副本组合成 miter，通过跨副本关系证明非干扰性）场景中归纳出两类反复出现的证明障碍：其一是「实现复杂度」——真正难以求解的是数据通路逻辑本身，而待证性质其实只需要一个紧凑的边界关系；其二是「关系归纳复杂度」——证明依赖跨副本的公共控制事实，而后端求解器无法高效推导出这些事实。为解决这两点，论文提出两种语义级证明分解形式：功能简化（functional simplification），用经过验证的过近似摘要替换难以证明的 RTL 区域；以及关系强化（relational strengthening），显式暴露并证明归纳所需的跨副本关系。在此之上实现 SLED-IFV：一个由求解器校验、LLM 引导的自动化流程，能够自动选择使用哪种分解形式及其具体目标区域。给定 self-composed miter 与无 oracle 的决策表，LLM 先提出分解方案，再在控制器检查下物化为证明产物；控制器把通过检查的产物编译成证明义务，而形式化验证后端始终是唯一的接受权威，因此 LLM 的输出必须被后端验证通过才能生效。在由真实 RTL 构建的九个非平凡基准上，SLED-IFV 相对纯求解器流程取得最高 603 倍加速，并把两个原本 12 小时超时的用例转化为完成的证明；闭环流程在所有用例上都产出了验证器可接受的分解。该工作适合硬件形式化验证、安全 SoC/RTL 设计、EDA 工具链以及 LLM-for-formal-methods 方向的研究者阅读。

背景与问题：LLM 编码智能体（coding agent）如今能够以远超人工审查速度的规模生成复杂程序，这带来了显著的安全与可靠性风险。常见检测手段——模糊测试、静态分析、LLM-as-a-Verifier——虽然能发现大量缺陷，但难以覆盖所有边界情况，无法给出「不存在违背安全属性行为」的强保证。形式化验证恰好能提供机器可检查的保证，但其传统瓶颈在于需要大量人工编写规格与证明工程，门槛高、成本大。核心方法：作者提出统一的多智能体框架 MAGS，把 Dafny 作为「验证感知的中间表示（verification-aware IR）」，使安全属性可以被机械检查。其流程为：先由人工审计并冻结 API 与安全需求（frozen specification），再将智能体生成的代码翻译为 Dafny，随后利用验证器返回的反例/诊断反馈自动修复违规（repair loop），最后把通过验证的 Dafny 程序编译回可执行代码。整个过程由多个智能体分工协作完成，把形式化验证的重活自动化。主要贡献与结论：作者在三个领域共 220 个样例上评估——100 个 CUDA kernel、100 个终端脚本、20 个机械臂任务——在冻结规范下全部成功产出具备非平凡安全保证的程序，成功率达到 100%。独立的安全性与功能性评估也显示三类任务上表现良好。论文同时诚实地揭示失败模式：当自动形式化得到的语义未能完整刻画目标真实行为时，验证仍可能通过但语义已偏（建模不完整 / 规格漂移），说明形式化保证的强度上限取决于规格本身的质量。适合读者：AI 代码生成与智能体平台开发者、需要为生成代码建立安全门禁的安全工程师、形式化验证与程序合成方向的研究者。

该论文关注形式化验证与软件保障中的基础原语——UNSAT 证明（不可满足性证明）。在实际工程中，SAT/SMT 求解器生成的证明往往编码了专有逻辑、内部约束或安全敏感信息，直接公开披露会导致知识产权泄露或攻击面暴露。零知识 UNSAT 认证正是为化解这一矛盾而提出：证明者可在不泄露底层证明任何细节（除"该实例确实不可满足"这一结论外）的前提下，让验证者相信不存在可满足赋值。Luo 等人此前提出的 ZkUnsat 协议通过"在零知识下证明一个弱化后的归结（resolution）证明的有效性"来实现该目标，首次验证了零知识认证的可行性。然而其可扩展性受制于显著的证明者内存开销，难以处理真实规模的实例。本文受 LRAT 等高效明文 UNSAT 证明格式的启发，提出一种不引入额外泄露的预处理技术：将证明进行归一化，使每一条派生子句都由固定公开长度 k 的归结链来支撑。这一归一化既消除了链长度本身的侧信道泄露，又显著降低了证明者内存占用。在 SAT 2002 竞赛基准上，取 k=16 时，该方法比基线 ZkUnsat 多认证约 62% 的实例；在认证实例数量相同的情况下，内存占用降至基线的 25% 以下。该工作属于密码学与形式化方法交叉方向，适合零知识证明、形式化验证、隐私保护计算及安全审计工具的研究者与工程师阅读。

LLM 智能体（agent）会生成并执行多步计划，计划中会调用外部工具；这些工具既可访问私有数据，也可执行命令。在此场景下，安全性并非某个单一步骤的属性，而是由计划所形成的整个执行过程的属性；计划本身就是关键工件，记录了工具调用、控制流与数据依赖关系。论文提出 CaMeLoT，作为已有防御方案 CaMeL（面向工具型 LLM 智能体的提示注入防御）的补充。CaMeLoT 在 CaMeL 基础上增加一个静态验证层，在调用任何工具之前对智能体计划进行检查。其核心方法为：把生成的计划翻译成有限状态迁移系统，用工具调用、provenance（数据来源）与污点信息对该系统进行标注，再使用 CTL（计算树逻辑）表达时序安全策略，并借助 nuXmv 模型检验器进行验证。由于验证发生在执行之前，不安全的计划会被直接拒绝，无需调用 LLM 或执行工具，从而节省运行时本会消耗的 token，也避免了回滚已发生的变更或拆除临时沙箱的成本。当验证失败时，模型检验器会返回反例，用于向智能体提供反馈以修复计划。评估方面，作者在来自 AgentDojo 基准、SOC 工作流和提示抽取（prompt-extraction）实验的策略集上对 CaMeLoT 进行了测试，结果表明它能够在执行前验证广泛的时序属性，同时保留 CaMeL 原有可运行时检查的覆盖范围。该工作属于形式化方法与 LLM 智能体安全的交叉方向，适合智能体安全、安全编排与形式化验证方向的研究者和工程师阅读。

基于能力（capability）的架构如 CHERI 为软件组件的架构级隔离提供了强支持：能力指针同时携带边界与权限，使硬件能够阻止越权访问。然而攻击者还可利用微架构侧信道窃取机密，因此敏感代码通常需以常量时间（constant-time）方式编写，即消除依赖机密数据的分支与访存模式。现代处理器普遍依赖推测执行，而推测执行可能破坏常量时间保证，使被隔离的机密通过瞬态执行被泄漏，即 Spectre 类问题。本文首先指出：为 CHERI 提供安全推测并非易事，已有方案无法保持机密性保证。为此作者构建了一个形式化框架，能够联合推理能力安全（capability safety）、推测执行与信息流安全，并用该框架展示潜在泄漏的存在。随后论文提出 SCHERI——一种在该框架内设计的新型处理器方案，并形式化证明其对常量时间策略提供端到端的安全推测保证。该工作为构建未来基于能力、且对常量时间程序具备 Spectre 抵御能力的处理器提供了形式化基础与实践指导，适合硬件安全、处理器微架构与形式化验证方向的研究者与安全工程师阅读。

该论文针对密码学协议形式化验证工具的实际使用体验开展了一项以人为中心的探索性研究。作者指出，Tamarin、ProVerif 等协议验证工具已被广泛用于分析复杂协议的安全性，但用户如何与这些工具交互、在哪里受阻，长期以来缺乏系统性研究。为此，研究团队面向具备实操经验的用户群体（包括科研人员、研究生与工业界实践者）开展问卷调查，覆盖 Tamarin、ProVerif 及相关协议验证器的使用者。研究结果显示，可用性障碍贯穿整个验证工作流：首先是调试困难，尤其是证明过程不终止（non-termination）与性能退化问题时，用户难以定位原因；其次是缺乏系统化方法，用于验证形式化模型是否忠实反映真实协议，即模型与现实协议之间可能存在的语义偏差难以被发现。在证明失败且未给出具体攻击路径的情况下，用户普遍采取三类应对策略：简化模型、添加辅助引理（helper lemmas）、回溯并重新审视建模抽象层次。参与者还明确提出了若干改进诉求，包括可操作的诊断信息、对验证结果更清晰的解释、可视化支持，以及针对重复性证明任务的自动化能力。作者进一步归纳出一个核心洞察：持续的可用性挑战源自“协议层推理”与“验证器的形式化模型、证明过程、诊断输出”之间的鸿沟，即用户以协议语义思考，而工具以形式化演算和求解器状态回应。基于这些发现，论文提出了面向设计者的具体优先级，旨在提升密码学协议验证工具的可访问性、可解释性与易用性。该工作属于人机交互与形式化方法交叉方向的实证研究，适合协议设计者、形式化验证工具开发者、以及将验证工具引入安全工程流程的团队阅读。

该论文聚焦容器化环境（Docker 容器与 Kubernetes Pod）中的中间人（MitM）攻击防护问题。作者指出，容器内工作负载与传统非容器环境一样面临钓鱼、应用层漏洞利用与网络入侵等威胁，但由于容器网络叠加层、服务网格、动态调度与多租户特性，通信链路的身份与加密边界更易被削弱，从而给 MitM 提供可乘之机。研究采用「系统性综述 + 设计科学（design-and-creation）」的组合方法：先依据 PRISMA 指南执行系统性文献综述，对同一研究主题下的现有证据进行筛选、归类与综合，识别出容器安全实践中的成功要素与空白点；随后提出并实现一套安全框架，用于保护容器化操作系统免受 MitM 攻击。该框架包含三块核心构件：一是用于表示通信行为与密码学原语的概念模型，使协议假设、密钥与信任关系可被形式化刻画；二是基于 AnBxJ Java 安全库的实现，用于协议建模与安全性质验证；三是工作在 OSI 模型第 7 层（应用层）的容器防火墙，用于在应用协议层面实施策略。研究围绕核心问题展开：如何有效保护容器化操作系统免受 MitM 攻击？其答案取向是系统化容器安全实践并引入零信任架构（zero trust architecture），即在容器与 Pod 之间默认不信任任何通信，对每一段连接进行显式认证与加密。论文报告称在容器化操作系统场景中成功实现并验证了该安全机制，并总结出若干成功要素。贡献层面可分为学术与实践两部分：学术上给出 MitM 防护在容器语境下的证据综合与形式化建模路径；实践上为 DevOps/云原生运维人员提供可落地的加固思路与零信任落地参考。适合云原生安全工程师、平台运维、容器网络与零信任架构研究者阅读。需注意，基于摘要无法获知具体实验规模、性能开销数据与防火墙策略细节。

该论文聚焦于现代身份认证体系中的多因素认证（MFA）平台，试图用密码学安全属性的形式化视角来审视其安全性，而不是依赖经验性的渗透测试或厂商自述。研究背景是：认证系统从早期的单一机制（用户名/口令、物理令牌、生物特征）逐步演变为把多种机制组合起来的 MFA 平台，组合方式、因素之间的绑定关系以及跨因素的会话状态管理都引入了新的安全假设，而这些假设往往缺乏统一的安全属性刻画。作者指出，在众多设计目标中，防止重放攻击（即攻击者复用某个可能已经泄露或被截获的认证组件来冒充合法用户）是 MFA 的核心诉求之一。论文的核心工作因此可以概括为：以密码学安全属性为分析框架，对 MFA 中与抗重放相关的机制进行建模与比较，考察不同因素组合、不同协议交互流程在形式化定义下是否真正满足所宣称的抗重放性质，并据此识别出安全属性与实际部署之间的差距。其贡献偏向于概念与形式化层面——为 MFA 提供一套可比较、可验证的安全属性语言和评估视角，帮助研究者和工程人员判断某个 MFA 方案的安全声明是否有严格的密码学依据，而非仅仅依据“多因素”这一标签。适合读者包括身份与访问管理（IAM）架构师、认证协议研究者、密码学协议分析人员以及负责 MFA 选型与评审的安全工程师。需要注意的是，本次可用信息仅为论文摘要，未包含具体的形式化模型、定理、协议清单与实验/案例验证结果，因此对其结论强度与适用范围应保持审慎，建议获取全文后再做技术判断。

本文提出了一套面向密码学软件的全新形式化验证方法论，其核心取向是直接验证“生产级代码”，而不是为了便于验证而专门改写代码。作者选择 Rust 作为目标语言，看重的是它在性能与系统集成方面的优势：Rust 的所有权机制使 Aeneas 工具链能够把 Rust 代码抽取为 Lean 中的纯函数模型，从而免除对指针存活性、别名关系等底层细节的推理负担；Lean 的可扩展性又允许团队开发专用的策略（tactic）与库，大幅简化对抽取后代码的推理。工具链被专门设计并调优以配合 AI：智能体可以自主撰写形式化证明，这些证明由 Lean 内核独立校验；智能体还参与密码标准与平台相关 intrinsic 的形式化工作，但这部分仍需专家主导设计与评审。作者将该方法应用于微软的密码提供者 SymCrypt，验证了从其 C 版本移植到 Rust 的 SHA-3、ML-KEM 等算法实现；并进一步用实验性优化以及 FrodoKEM、ML-DSA、HPKE 等算法的实现来扩展 SymCrypt，以考察编写、移植与验证密码代码的可扩展性。整个 Lean 开发规模约 237 KLOC，为 16.7 KLOC 的 Rust 代码（覆盖 x86-64 与 ARM 平台上的后量子密码套件）建立了内存安全性、无 panic 以及功能正确性的证明。评估结果显示，经过验证的 Rust 实现能够满足 SymCrypt 在性能、可移植性、部署方式与可维护性方面的要求。

零知识虚拟机（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／电路开发者与形式化验证研究者，提供了首个在真实系统上可扩展、可自动化的约束正确性检查路径。

该论文研究区块链智能合约中的抢跑（frontrunning）攻击与抗抢跑性质的形式化定义问题。背景上，智能合约通过共识执行，但交易排序本质上是异步的：交易由矿工（或验证者）决定打包、排序与延迟。由于用户必须通过交易与合约交互，掌握排序权的节点可以重排、延迟或插入交易，从而抢在诚实用户之前获利，这类攻击在以太坊等主流链上已造成数百万美元损失。论文指出当前领域存在两个根本性缺陷。第一，缺少对“合约抗抢跑”这一性质本身的严格定义，导致安全目标模糊、无法对工具与审计结论做一致性比较。第二，现有动态检测方法在覆盖面上严重不足：作者对 287 份智能合约审计报告做了大规模研究，审计方共报告 393 个漏洞，其中 55% 落在当前最先进检测标准的判定范围之外，说明主流工具系统性地漏检了一大批被人类审计师认定的抢跑问题。针对这一缺口，作者提出首个面向智能合约抢跑漏洞的形式化定义。其核心洞察是：抗抢跑并非合约代码的固有属性，而强烈依赖于诚实用户如何与该合约交互——同一个合约在不同交互方式下可以是安全的或不安全的。基于该观察，作者设计了一个健全（sound）的算法，用于合成“安全交互条件”，即在什么交互约束下合约能够抵抗抢跑；并实现原型工具，将其应用于真实已审计合约，在两个以太坊合约中发现了此前未被发现的漏洞。工作属于形式化方法与实证研究结合，读者对象为智能合约安全研究者、审计工程师、形式化验证与区块链安全工具开发者。

该论文关注现代语义丰富系统与应用中的“应用逻辑漏洞”（application logic flaws）。这类漏洞与业务语义和威胁模型深度绑定，难以通过传统的模糊测试或静态分析规模化发现：真实系统往往包含多样的应用特性、复杂的协议逻辑与领域专属的威胁模型，需要大量人工投入与领域专家经验才能完成有效安全分析。作者提出 LL-Verifier——一个自动化逻辑漏洞发现框架，其核心由两部分构成：(1) 利用大语言模型完成自主建模（autonomous modeling）；(2) 利用逻辑模型检测器（logic model checker）完成严格推理。LL-Verifier 接受自然语言输入，尤其是协议描述与安全目标，自动生成形式化逻辑模型与安全属性；这些属性用一种新的逻辑语言表达，该语言构建在通用逻辑语言 Maude 之上，并针对“任意应用级语义”的建模进行了优化。随后，生成的形式化模型被转换为逻辑状态机，从而可以通过逻辑层面的模型检测实现穷尽式、严格的验证。该方案的目标是把原本高度依赖人工的应用级协议分析流程自动化，在逻辑约束范围内提供自动化、穷尽且精确的推理能力。为验证效果，作者在 27 个广泛使用的 IoT 设备的访问控制协议上进行了评估，这些协议带有厂商特有的逻辑流程与语义。论文声称在有效性、效率与实用性上均取得良好表现，并在 IoT 协议与设备中发现了多种复杂的逻辑漏洞，具有严重的安全与隐私影响。值得注意的是，该工作直面的正是应用安全中一个公认的难题——自动化的逻辑漏洞发现。 从研究视角看：研究问题是如何在缺乏人工领域知识的前提下，对具有任意应用语义的协议进行可规模化、可穷尽的安全推理；核心方法是“LLM 自主形式化建模 + Maude 系逻辑语言 + 逻辑状态机模型检测”的三段式流水线；主要贡献是提出该框架、给出一套面向应用级语义的建模语言与转换机制，并在 27 个真实 IoT 访问控制协议上完成实证评估，挖掘出新型逻辑漏洞。适合阅读的读者包括：从事形式化验证、协议安全、IoT 安全的研究人员，以及希望把形式化方法引入业务逻辑审计的安全工程团队。由于仅获取到摘要，方法细节、逻辑语言的具体语法语义、模型检测的可扩展性指标、以及漏洞细节均未展开。

该论文聚焦于以存储为中心的计算（storage-centric computing）场景下固态硬盘（SSD）固件——闪存转换层（FTL）——的安全与正确性问题。研究背景是：数据密集型应用需要把大量数据从存储搬运到计算单元，产生显著的数据移动开销；把计算下沉到 SSD 内部或近端可以缓解该开销，但这要求修改 FTL 中的地址转换、垃圾回收等策略。作者指出，FTL 属于设备固件，其逻辑直接访问安全关键的设备组件，因此即便功能上完全正确的 FTL，也可能在租户之间泄漏数据、丢弃完整性标签，或把闪存块错误地分配给其他租户。论文首先证明一个有缺陷的 FTL 可以在 SSD 内部的五个“表面”（surfaces）上破坏设备状态，并在 DaisyPlus OpenSSD 平台上进行了演示。作者进一步指出现有 FTL 验证工作的两大局限：(1) 只验证功能正确性，被修改的 FTL 即使违反隔离性、完整性与归属（ownership）约束仍能通过验证；(2) 验证与某一具体 FTL 设计绑定，任何改动都要重做全部证明，代价高昂。为此作者提出 CertiFlash：一个在 Rocq（Coq）证明助理中机械化的 FTL 形式化验证框架。CertiFlash 把 FTL 建模为确定性状态机，并在映射、隔离、完整性、归属和分配五个维度上建立单一全局不变式；在该通用 FTL 模型上一次性证明两件事：(i) 每个 FTL 操作都保持该不变式，(ii) 该模型细化了理想化的块设备语义。对新设计，开发者只需为其自身操作消解五条假设（hypotheses），而无需重做上述两个证明。在四个案例研究中，设计者只需在 16,489 行的框架之上新增 27 至 3,231 行代码，验证工作量显著降低。框架已开源。适合关注存储安全、SSD 固件、多租户隔离以及形式化验证的研究者与工程人员阅读。

本文研究的是零知识机器学习（ZKML）电路中的「冗余检查」问题及其可证明安全的去膨胀（debloating）技术。背景是：面向神经网络推理的零知识证明系统会把模型编译成大规模算术约束系统，其中包含大量范围证明、符号查找（sign lookup）、比特分解等约束。作者指出，这些约束中有相当一部分是「冗余检查」——它们所断言的事实在整条电路上已经被其他远处的组件通过一连串推理关系所蕴含，因此单看局部是必要的，但从全局看其约束力是多余的。删除这类冗余约束能显著缩小电路规模、加快证明生成，但删除必须以严格的可靠性（soundness）论证为前提：一旦删得不合理，电路就会变成欠约束（under-constrained），证明者可以构造出原电路本应拒绝的见证，例如谎称某个神经网络产生了它实际上并未计算过的输出。作者强调这不是假设性威胁——已部署的 ZK 系统中出现过的欠约束电路缺陷，曾使攻击者能够伪造交易并完全绕过验证。 核心方法上，作者提出一个自动化框架：对每一个候选删除的约束，工具首先判断「电路其余部分」自身是否仍然能够排除被删约束原本排除的所有取值。为此，工具使用全电路抽象解释（whole-circuit abstract interpretation）来搜索这些替代性论证，并把它们记录在一张溯源图（provenance graph）中；只有当图中存在一条替代路径仍然能够推导出该约束所检查的事实时，才真正删除该约束。这一「先证明替代论证存在、再删除」的流程，从机制上保证去膨胀后的电路不会为敌手开启新的伪造路径，即在不削弱安全性的前提下完成优化。 实验方面，作者在 ezkl 与 zkml 两个生产级框架生成的 MLP、CNN、RNN 与 Transformer 电路上进行评估，电路规模最高达 2530 万条约束。结果显示，工具可移除最高 48.7% 的约束，并把证明者（prover）耗时最多降低 72.8%，同时不削弱安全性。该工作适合零知识证明工程、ZKML 系统开发者、形式化验证与程序分析研究者，以及关注 ZK 电路可靠性漏洞的安全工程师阅读。

该论文聚焦 RISC-V 处理器硬件安全验证中的一大效率瓶颈：把一组已在某个处理器目标上通过验证的安全断言（security assertions）复用到另一个 RISC-V 核上。这一过程目前主要依靠人工完成，单条断言的翻译往往要耗费数小时，是硬件安全验证流程中最昂贵的环节之一。虽然直接用大语言模型做翻译速度快，但作者指出其可靠性不足，存在两类突出问题：一是“信号幻觉”，即模型凭空编造出目标 RTL 中根本不存在的端口或信号名；二是输出不确定性，同一模型在版本更新后、甚至同一版本内的多次推理都可能给出不一致的结果，使流水线难以稳定复现。为应对这些问题，论文提出 AutoTrans 自动化框架，由三个相互衔接的部分构成。第一，设计了一个轻量级、基于正则表达式的 SystemVerilog 信号提取器，先从目标 RTL 中枚举真实存在的信号，作为生成断言时的约束条件，从源头抑制信号幻觉。第二，提出一套提示模板并固定（pinned）推理参数，保证每次运行时提示词的组装都是字节级一致的，从而让整条流水线的输出对模型更新保持韧性；该模板还能仅凭英文自然语言的安全描述，在没有人工撰写断言的前提下生成安全断言。第三，将形式化验证（JasperGold FPV）集成进流程，作为强制性质量门禁，确保生成的断言确实能验证处理器的安全属性，而不是未被检验就静默进入结果集。作者在 Deepseek V4 上开展实验，将安全断言从一个 RISC-V 目标（NS31A）迁移到另一个目标（IBEX）。结果显示，在完全没有人工介入的情况下，自动翻译接受率（TAR）达到 78%；经过人工精修后，最终 TAR 达到 100%。该工作适合从事硬件安全验证、EDA 流程自动化、形式化验证以及 LLM 辅助工程落地研究的读者参考。

该论文研究 ML-KEM-768（即 FIPS 203 标准化的 Kyber 密钥封装）在诚实解封装条件下失败概率上界的严格认证问题。ML-KEM 的安全性论证长期依赖一个启发式结论：解封装失败率约为 2^-164 量级，但近期的形式化评估指出，这一启发式尺度缺乏严格证明，属于公开难题。作者在显式的随机函数/中心二项分布（ROM/CBD）抽象下给出了该尺度的、保持依赖关系的可认证上界：把按域分离的公钥矩阵流建模为独立均匀环元素，把秘密与噪声多项式建模为独立的 CBD2 原语；论文明确说明这不是针对 FIPS 203 固定 SHAKE 实例的信息论结论。分析保留了公钥矩阵以及两个密文压缩项 c_u、c_v 所引入的依赖关系，避免因独立性假设而失真。证明的终端链条分为三段：首先为联合 c_u/c_v 残差构造精确的图耦合全理想参考；其次通过 proper-ideal 二元傅里叶传输进行处理，其中罕见的 |T|>=3 分支用穷尽式三因子反集中重放予以封闭；最后采用精确到比特的 FIPS 解码事件，仅保留 256 坐标的联合界。作者还给出形式化的部分傅里叶引理，使从谱范数到全变差的步骤显式可验证。最终约化有理证书给出 Pr[K' != K] <= P_* <= 2^-164.81，其中 -log2(P_*) = 164.810716201343121…。该阈值精确但数值上极为紧致：认证指数仅超出 164.81 约 0.0007162 bit，而 164.82 未被认证。该结论对任意与公私随机性独立固定的消息、在诚实加密与诚实解封装下成立。作者明确声明它不是精确 DFR、不是固定 SHAKE 的等价定理、不是新的 IND-CCA 归约，也不是自适应 delta-correctness 结果。

在后量子密码学中，基于格的方案（如Falcon/FN-DSA）需要高效的数论变换（NTT）硬件实现，而传统NTT核心的模乘器和旋转因子存储占用了大量芯片面积。本文提出FoldNTT，对TCHES 2022发布的radix-2 CFNTT加速器进行重新设计，面向Falcon/FN-DSA使用的Proth质数 q=12289。主要创新包括：每个蝶形仅使用一个硬件乘法器（原本需要三个），并将旋转因子存储量减少约一半。利用q=3*2^12+1的Proth结构，模约简通过移位加折叠（K-RED fold）实现；同时位反转的旋转因子表满足关系 w[N/2+j] = psi*w[j]，使得表中的一半可以无乘法器地派生。作者在检查已发布RTL时发现一个Bug：其逆变换遗漏了逐级减半步骤，导致输出为2^10*x而不是目标值，FoldNTT对此进行了修正。为确保正确性，作者使用精确宽度SMT和组合式SymbiYosys证明对所有算术模块进行形式化验证，对控制安全不变量使用k-归纳法，并通过变异测试和仿真验证综合变换，且所有验证在CI中自动重跑。在Artix-7 FPGA上的开放流程实验表明，修复后的设计将每个蝶形的DSP48消耗从3个降至1个，存储的twiddle位数减少50%，而全核Fmax仅下降约4%（在最优种子和种子间波动范围内）。作者重构了控制器（参考FSM未公开）并完成全核仿真验证，还构建了可在Basys-3板上运行的门控时序位流。该工作展示了对NTT硬件架构的系统性优化，并通过形式化方法发现并修复了一个隐藏的正确性缺陷，对后量子密码硬件的发展具有重要意义。

该论文提出了一种名为 Scratchy 的视觉暂存器多模态推理方法，旨在解决大语言模型（LLM）在生成密码学形式化证明时面临的结构性依赖难题。在密码学领域，计算安全性论证要求证明必须协调概率、对抗游戏、不变量、假设和界限等要素，而 EasyCrypt 机器检查框架可以验证这些证明。然而，尽管这些要素可能都出现在上下文中，LLM 仍难以生成正确证明，因为证明理论依赖往往在线性表示中隐式存在，且分散在多个程序中。Scratchy 的核心思路是显式地暴露这些依赖：首先，将自然语言的安全描述、形式化上下文和目标命题规范化为类型化的证明关系图；然后，通过结构保持的视觉编译器将该图转换为富含公式的视觉证明状态，该状态作为多模态模型的输入，引导模型生成 EasyCrypt 证明。作者还构建了 Scratchy-eval 评估基准，包含 114 个任务，均来源于可靠的官方 EasyCrypt 文件，其中 64 个为安全形式证明生成任务，50 个为多项选择知识测试任务。评估重点覆盖了语义基础、关系不变量和游戏归约等维度，实验表明，经典 LLM（如 GPT-5.6-Sol 和 Claude-Opus-5）在采用 Scratchy 的结构化视觉证明状态后获得了显著性能提升。该结果凸显了显式证明结构的重要性，并展示了多模态证明状态表示作为计算机辅助密码学工具的前景。论文的贡献在于提出了一种新的形式化证明生成范式，并提供了配套数据集，为安全协议验证的自动化提供了新思路。

该论文提出并证明了一个元定理：对于任何一致且具有足够表达能力的有限句法系统S，必然存在至少一个该定理无法自主产生的定理。所谓“有限句法系统”涵盖形式逻辑系统、形式验证器、安全机制、AI系统、法律与经济模型等所有基于有限规则和符号生成机制的体系。作者证明的不是某个具体定理的不可证明性，而是“存在这样一个不可自主推导的定理”这一元事实，因此该结论适用于所有有限句法系统，甚至适用于证明该结论自身的形式系统。论文将这一结果与哥德尔不完全性定理区分开来，强调它不依赖自指或一致性条件中的特定构造，而是基于系统的有限性和表达能力的普适约束。其核心推论是：任何基于有限规则构造的安全机制或AI系统都存在结构性盲区——存在某些安全属性或行为模式是系统无法从自身规则出发推导或验证的。这意味着完全自主的安全保证和完全可验证的AI行为在逻辑上是不可能的，必须引入外部假设、交互式验证或非自治的补充手段。对于安全领域，该结果对“完备的入侵检测”“全自动漏洞修复”“形式上可验证的AI安全”等理念提出了基础性的质疑。论文旨在引发对形式方法边界和安全实践哲学基础的讨论，而非提供具体攻击或防御方法。适合关注形式方法基础、AI安全理论边界和安全机制完备性假设的研究者阅读。

拜占庭容错（BFT）协议是分布式系统中最难设计和推理的组件之一。近年来，形式化验证领域发展出多种计算机辅助方法，能够对独立（standalone）BFT 协议的安全性与活性进行自动化验证；与此同时，分布式计算社区也尝试将复杂协议拆分为更简单的“构建块”进行组合，以降低设计新协议的概念复杂性。然而，到本文发表为止，还没有任何方法论能够将这两种研究路径统一起来，实现对任意复合式 BFT 协议的基础性（foundational）验证。本文提出了一种复合式拜占庭协议的组合验证方法，核心贡献是建立一套形式化框架，使协议设计者可以基于已验证的简单子协议模块，通过组合规则安全地构建更复杂的 BFT 协议，并自动继承或证明整体协议的期望正确性属性。作者综合运用了并发证明、协议组合理论和自动验证工具，给出了模块化推理规则，并展示了该方法在多个经典 BFT 协议变体上的可行性。这项工作填补了分布式系统形式化验证中的一个空白，有望将 BFT 协议的正确性证明从“一次性、手工程序化”转化为“可组合、可复用”的工程实践。对于研究分布式共识、区块链底层以及安全关键系统的人来说，本文提供了从组合视角系统性验证容错协议的新思路。

本文提出 Griotte 和 Griotte OS，这是对 CHERIoT 硬件能力机器与 CHERIoT RTOS 的抽象化但忠实的建模，旨在为 CHERIoT 的分区隔离（compartmentalisation）安全保证提供形式化验证基础。CHERIoT 是一种软硬件协同设计，通过硬件能力（capabilities）定义“分区”这一概念，操作系统默认隔离各分区以限制漏洞或恶意行为造成的损害。跨分区通信依赖一个特权组件——切换器（switcher），该组件提供跨分区调用接口，同时强制分区隔离并保证栈安全。由于 CHERIoT 的安全属性依赖于能力机器与切换器的互补作用，需回答两个关键问题：其一，如何形式化地描述 CHERIoT 分区所提供隔离的具体安全含义；其二，该设计是否确实强制实施所期望的安全属性。为此，作者用基于续延的逻辑关系（continuation-based logical relation）形式化地刻画出切换器与能力机器组合行为所应满足的安全保证，并为 Griotte 的切换器定义了符合这些保证的规范，进而以证明其实现满足该规范。作者在一系列关键场景上验证了 Griotte 的有效性，这些场景涵盖 CHERIoT 的不同方面，包括在内存与未知代码共享时本地状态的完整性。该方法具有模块化特点：可分别验证每个分区，再组合其规范。整体上，该工作为 CHERIoT 设计提供了坚实的形式化基础。适合安全架构师、系统形式化验证研究者以及关注硬件/OS 隔离机制的蓝队人员阅读。

本文面向可信执行环境（TEE）中飞地程序的安全性问题，特别是状态连续性（State Continuity）的验证，提出了一种形式化验证方法。状态连续性指飞地程序在执行过程中，即使遭遇异常中断、迁移或恶意系统软件干扰，其内部状态仍能保持一致和完整。作者基于程序逻辑和定理证明技术，构建了状态连续性的形式化模型，定义了验证规则，并可能使用了自动化工具进行验证。该研究有助于从数学上保证飞地程序的状态安全，防止回滚、重放等攻击。论文的主要贡献包括状态连续性属性的精确刻画、验证框架的设计与实现，以及基于典型飞地应用的案例研究。这项工作对TEE安全研究者和开发可信应用的安全工程师具有重要参考价值。

该论文针对安全代币（Security Tokens）标准中监管操作语义不明确的问题，提出了一种机械化（machine-checked）的参考执行语义。安全代币标准通常暴露特权转移、冻结、恢复和合规机制，但机制本身并不标识其执行的法律效果或附带的证据与撤销义务。作者在 Isabelle/HOL 中形式化定义了 ERC-8319 中提出的六种监管行动：FREEZE、SEIZE、CONFISCATE、LIQUIDATE、RESTRICT 和 RECOVER。模型区分了应用（applied）、拒绝（rejected）和操作失败（operational-failure）三种结果，并机械化验证了撤销（reversal）、重放（replay）、纪元（epoch）、框架（frame）、案例局部终态（case-local terminality）和收据（receipt）等性质。构建过程中没有未证明的占位符或额外公理。论文证明了外部事实边界：两个在所有权、结算和权益上存在分歧的具体世界会产生相同的核观察结果，因此这些外部事实不能从受限输入中建立。通过构造性见证和直接变异展示了可达性和故障集的伪造（falsification）。针对一个 ERC-TRUST Solidity/EVM 候选实现，论文分别报告了 Foundry、Certora、Kontrol/KEVM、变异测试、确定性构建和运行时身份的证据。当前发布概况满足全部 7 个证据包、49 个 Core 和 24 个强制性 Supporting 义务，且无部分学分；6 个可选义务未声明。在固定运行时前提下，机械化抽象关系被证明是唯一且函数的，包和行推论从哈希绑定证书产生条件性的、概况范围的细化定理。作者明确声明，这些结果并不构成完整的 Isabelle 到 Solidity 到 EVM 的细化定理、编译器正确性、审计、生产就绪或部署验证。其贡献在于一种机器检查的领域语义，以及一张可证伪的地图，说明对于受监管代币执行标准，什么是已证明的、什么是有界证据、什么是假设的、什么是开放的。该研究面向智能合约形式化验证、安全代币标准和监管科技领域的研究者与工程师。

本文提出了 ARMOR，这是首个针对 X.509 证书链验证逻辑（CCVL）的大规模形式化验证实现，旨在为 RFC 5280 的大部分内容提供机器可检查的正确性保证。ARMOR 的设计目标有两个：一是作为 RFC 规范的形式化、机器可检查的替代品，二是作为参考实现和测试预言机。其架构采用模块化设计，将 X.509 CCVL 分解为多个模块，每个模块独立地进行规格说明、实现和验证。目前，ARMOR 已正式验证的模块包括 PEM 和 ASN.1 X.690 DER 语言（子集）的规格说明与解析、证书链构建，以及单个证书内和证书链中证书字段所需属性的多种语义性质。为了实证评估这些目标的达成情况，作者将 ARMOR 与 11 个开源 X.509 实现及一个开源证书检查工具进行了比较，评估其规格准确性和运行时开销。实验结果显示，尽管 ARMOR 引入了较高的运行时开销，但通过使用它，能够检测出若干不符合规范的情况。最后，作者展示了 ARMOR 的端到端应用：将其集成到 BoringSSL 的 TLS 1.3 实现中，并使用 Curl 进行测试。这项工作为证书链验证的正确性提供了可验证的基准，有助于发现现有实现中的合规性问题。

本文提出一个名为 Distiller 的通用框架，旨在优化概率证明系统（包括交互式证明 IP、简洁非交互式论证 SNARK、概率可检验证明 PCP 等）的前端开销。在过去十年中，概率证明的实现虽受广泛关注，但由于前端需要将抽象计算转换为等价的算术约束，导致实现规模难以扩展。Distiller 的关键思想是：用户不需要将原始计算直接编码为约束，而是可以翻译一个抽象规格说明（abstracted specification），并在此基础上进行约束生成。该框架首次在此领域实现了可证明安全的转换，即转换过程本身具有形式化保证。此外，Distiller 将“在约束中编码检查”的思想推向逻辑极限，从而发现更多减少约束数量的机会。在基准测试中，Distiller 实现了 1.3 到 50 倍的成本降低，部分场景下获得了更好的渐近复杂度。这篇论文主要面向研究概率证明系统、零知识证明、SNARK 编译器及形式化验证方法的研究人员与高级工程人员，核心贡献在于提供了一种可证明安全的通用约束简化方法，为提升证明系统的可扩展性提供了新思路。

该论文针对形式化验证程序中的一个关键盲区：即便程序通过了形式化验证，其正确性仍受限于规范（SPEC）的完整性。若规范本身存在漏洞或不完整，验证结果将失去意义。作者提出了一种名为 Fast（Fuzzing-Assisted Specification Testing）的自动化方法，利用同一代码库中规范、实现和测试套件均由同一业务需求派生出的冗余性和多样性进行交叉验证。核心思想是：如果某个意图在实现和测试用例中有所体现，却未被规范捕获，则强烈暗示规范存在盲点。Fast 首先通过变异测试定位规范缺口，即检查代码变体是否仍然符合原始规范；若符合，则进一步利用测试套件推断该缺口是有意引入还是疏忽所致。针对不同规模的代码库，Fast 可选择枚举式或进化式方式生成代码变体。作者在两个具有形式化验证的开源代码库上应用 Fast，分别确认了 13 个和 21 个规范盲点，证明规范不完整在真实应用中普遍存在。该研究为提升形式化验证的可信度提供了一种辅助手段，适合形式化方法、软件测试和安全研究人员阅读。

本文针对使用高斯分布的差分隐私算法的验证问题展开研究。现有形式化验证方法在处理连续分布（尤其是高斯分布）时面临精度和可判定性挑战。作者提出了一种新颖的近似方法，用于逼近无循环程序的概率分布，这些程序可从具有可计算概率密度函数的离散和连续分布（包括高斯和拉普拉斯）中进行采样。他们证明了对于这类程序，验证 (ε,δ)-差分隐私是“几乎可判定的”，即除有限个δ值外，所有情况均可判定。验证算法通过结合积分近似和尾部概率界，以任意所需精度计算概率。该方法已在工具 DipApprox 中实现，利用 FLINT 库进行高精度积分计算，并包含提升可扩展性的优化。作者在基础隐私保护算法上验证了工具的有效性，如稀疏向量技术的高斯变体和 Noisy Max，展示了其在确认隐私保证和检测违规方面的能力。该研究为差分隐私机制的自动化验证提供了理论保证和实用工具，适合形式化方法研究者和隐私保护工程师阅读。

本文研究智能体（Agent）运行时环境中一种被称为“执行编辑”（execution edits）的操作安全性问题。执行编辑包括 Checkpoint（记录当前执行状态）、Fork（分支）、Restore（恢复某个检查点）和 Merge（合并分支），这些操作允许在不重启任务的情况下改变智能体的后续执行路径。然而，执行编辑无法撤销先前的授权或已经发出的工具请求，因此不安全的编辑可能导致同一工具动作被重复授权、丢弃任务仍需要的结果，或与编辑前已开始的调用产生冲突。由于智能体本身不可信，运行时必须依据其执行记录来确定每次编辑需要兼顾哪些过去的动作、必须保留哪些关键结果，才能确保后续执行安全。现有智能体系统却并未从实际运行中推导出每次编辑必须保留的内容，而是将这一需求作为输入条件，导致安全性缺乏严格保障。本文提出了一种算法，能够精确判定一次编辑是否安全，并返回所有安全的继续执行方式，或者证明不存在安全方式。该算法枚举任务在不违反策略的前提下可能完成的所有路径，移除那些可能导致后续无法完成关键结果的路径，若剩余路径为空则返回可验证的证明，表明不存在安全实现；否则，剩余路径精确描述了运行时可以允许的行为。形式化结果覆盖了 Checkpoint 以及 Fork、Restore、Merge 的六种形式，并扩展到原子强制实施以及精确检查器所需的信息。研究使用 Lean 定理证明器对有限检查器和运行时不变式进行了机械化验证，并通过测试验证了所有六种编辑形式。源代码、Lean 证明和可执行测试均公开在 GitHub 仓库中。该工作为智能体运行时的安全控制提供了理论基础和可验证的实现方法，适合系统安全、形式化验证和智能体架构研究者阅读。

本文针对高保证密码学（High-Assurance Cryptography）在现代处理器投机执行（Speculative Execution）时代下的安全保证问题展开研究。传统上，高保证密码学通过程序验证与密码工程方法，为密码软件提供内存安全、功能正确性、可证明安全性以及无时序泄漏等机器可验证的保证，但这些保证通常基于顺序执行语义建立。然而，现代处理器为了提升性能普遍采用投机执行，导致实际执行行为与顺序语义不一致，加之著名的Spectre系列攻击利用投机执行漏洞，使得高保证密码学所承诺的安全属性受到质疑。本文旨在消除这些疑虑，证明高保证密码学的优势在投机执行环境下依然成立，且仅需付出适度的性能开销。作者在Jasmin验证框架之上构建了一种端到端的方法，用于在投机执行语义下证明密码软件的安全属性。该方法扩展了原有验证框架的能力，使其能够建模投机执行带来的微架构侧信道风险。通过在Jasmin中实现ChaCha20和Poly1305两种高效密码算法，作者生成了功能正确且高效的汇编实现，并利用形式化验证证明了这些实现不仅对传统时序攻击安全，而且对投机执行攻击（如Spectre）同样安全。实验结果表明，所提出的方法能够在不显著牺牲性能的前提下，为密码软件提供针对投机执行的高保证安全性。该研究的核心贡献在于：第一，首次将高保证密码学的验证目标扩展到投机执行语义，填补了形式化验证与微架构安全之间的空白；第二，提供了可复用的验证方法论和工具链，使密码工程师能够系统性地设计和验证抗投机执行攻击的密码实现；第三，通过实例验证了该方法的实用性和可扩展性。本文适合密码学与形式化验证领域的研究人员、安全架构师以及需要开发高安全性密码库的工程师阅读，尤其对关注侧信道攻击防御的蓝队人员具有参考价值。

该论文提出了首个面向协议计算后量子安全性的机械化证明体系。核心贡献是设计了一个新的计算一阶逻辑 PQ-BC，该逻辑相对量子攻击者是可靠的，并基于此实现了机械化证明工具 PQ-SQUIRREL（通过修改经典的 SQUIRREL 证明器并加入新策略）。PQ-BC 的构建需要对经典 BC 逻辑进行扩展，使其在单一交互式量子攻击者模型下保持可靠性，同时通过强制一组语法条件来保证工具的正确性。利用 PQ-SQUIRREL，作者完成了多个案例研究，首次给出了计算后量子安全性的机械证明，包括两个基于 KEM 的密钥交换通用构造、IKEv1 和 IKEv2 的两个子协议，以及 Signal X3DH 协议的一个后量子变体。此外，该工具还证明了许多经典的 SQUIRREL 案例研究已经具备后量子安全性。这项工作为后量子安全协议分析提供了基础性工具，填补了机械化后量子安全证明领域的空白。适合密码学协议设计者、形式化验证研究人员以及关注后量子迁移的安全工程师阅读。

本文提出并实现了一个名为 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治理、模型风险管理、形式化验证及可验证机器学习的研究人员阅读，为多模型耦合场景下的风险监控提供了理论工具与可审计性方案。

量子密钥分发（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程序迁移到内存安全语言，并为每个翻译程序提供形式化保证保持可观测行为的系统。

该论文提出了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约简中具有普遍性。本文适合对后量子密码侧信道防护、形式化验证与硬件安全感兴趣的研究者阅读。