Approximate Algorithms for Verifying Differential Privacy with Gaussian Distributions.
本文针对使用高斯分布的差分隐私算法的验证问题展开研究。现有形式化验证方法在处理连续分布（尤其是高斯分布）时面临精度和可判定性挑战。作者提出了一种新颖的近似方法，用于逼近无循环程序的概率分布，这些程序可从具有可计算概率密度函数的离散和连续分布
#formal-verification
共收录 95 条相关情报。
← 返回所有主题When Can Agents Safely Checkpoint, Fork, Restore, and Merge? Exact Checking for Execution Edits
本文研究智能体（Agent）运行时环境中一种被称为“执行编辑”（execution edits）的操作安全性问题。执行编辑包括 Checkpoint（记录当前执行状态）、Fork（分支）、Restore（恢复某个检查点）和 Merge（合并
High-Assurance Cryptography in the Spectre Era.
本文针对高保证密码学（High-Assurance Cryptography）在现代处理器投机执行（Speculative Execution）时代下的安全保证问题展开研究。传统上，高保证密码学通过程序验证与密码工程方法，为密码软件提供内存
A Logic and an Interactive Prover for the Computational Post-Quantum Security of Protocols.
该论文提出了首个面向协议计算后量子安全性的机械化证明体系。核心贡献是设计了一个新的计算一阶逻辑 PQ-BC，该逻辑相对量子攻击者是可靠的，并基于此实现了机械化证明工具 PQ-SQUIRREL（通过修改经典的 SQUIRREL 证明器并加入新
Verbatim: A Verified Lexer Generator.
本文提出并实现了一个名为 Verbatim 的可执行词法分析器（lexer），其开发和验证均基于 Coq 证明助手。词法分析器和解析器常被用作大型软件系统的前端，负责连接外部输入与系统内部逻辑，因此成为攻击者试图攻陷整个系统的天然目标。作者
Certified but Private: Scalable Zero-Knowledge Proofs for Neural Network Guarantees
本文提出 PANDA，一个基于零知识证明（ZKP）的可扩展系统，用于在保护神经网络模型参数私密性的同时，形式化地证明模型的鲁棒性和公平性。随着机器学习模型在安全关键和法律合规场景中的部署日益增多，模型的鲁棒性和公平性保证变得重要，但模型参数
Verified Pythagorean Composition for Adaptive Cryptographic Games: Noise Flooding in Homomorphic Encryption
本文研究近似同态加密（approximate homomorphic encryption）中噪声泛洪（noise flooding）防御手段在自适应解密攻击下的安全性证明问题。噪声泛洪是抵御解密攻击的标准技术，但其安全证明对组合方式异常敏
Research Report: Not All Move Specifications Are Created Equal : A Case Study on the Formally Verified Diem Payment Network.
这篇研究报告探讨了在智能合约（如 Diem 支付网络）中推广形式化验证时，开发人员对“规范（specifications）”角色的不同理解如何影响形式化验证的整体效果。作者指出，初次接触形式化验证的软件开发者，往往对规范在操作层面上的意义持
VUPER: Verified ASN.1 UPER Parser
该论文提出了 VUPER，一个用于生成经过形式化验证的 ASN.1 UPER（非对齐压缩编码规则）解析器的框架。ASN.1 是一种广泛使用的接口描述语言，而 UPER 是其中关键的编码规则之一，尤其在蜂窝网络和车联网（V2X）通信等安全关键
Joint Lyapunov Certificates for K-Agent Generative AI Governance: Stochastic Stability, Emergent Ensemble Risk, and Zero-Knowledge Governance Attestation
本文提出一个面向多智能体生成式AI系统治理的严格数学框架，聚焦于K个自适应性生成式AI模型在模型风险管理（MRM）原则下的联合稳定性与零知识证明问题。研究背景在于：当多个模型通过交互矩阵形成元学习耦合时，传统基于单个智能体的Lyapunov
Beyond the Quantum Promise: A Security Analysis of Classical Control in Quantum Key Distribution
量子密钥分发（QKD）协议通过量子力学原理提供信息论安全性，但实际部署中QKD本质上是混合协议：其安全结论高度依赖量子阶段与经典后处理阶段的正确集成。虽然ETSI和ITU-T等标准组织已定义了QKD的架构与接口，但现有规范通常在隔离条件下评
A Sound Translation from Tamarin to ProVerif: Enabling Comparative Analysis
这篇论文针对两个主流的协议形式化验证工具 Tamarin 和 ProVerif 提出了首个从 Tamarin 到 ProVerif 的忠实的（sound）翻译方法，以支持系统性的对比分析。Tamarin 基于多集重写规则，验证是可靠且完备的
Game Hopping in Lean
本文提出 HOPSCOTCH，一个基于 Lean 4 的框架，用于机械化计算可靠的、基于游戏的安全证明。安全定义被表达为有状态概率预言机之间的不可区分性，证明过程遵循标准的游戏跳跃范式。HOPSCOTCH 采用浅嵌入方式，预言机和归约都是普
Formal Analysis of BLE Secure Connection Pairing and Revelation of the PE Confusion Attack.
本文针对蓝牙低功耗（BLE）安全连接（Secure Connections）配对协议的安全性展开形式化分析。配对是 BLE 安全体系中的关键环节，决定了后续通信加密密钥的协商方式，因此其安全性直接影响设备间数据传输的机密性与完整性。作者构建
Decidability of Parameterised Dolev-Yao Secrecy
本文研究Dolev-Yao模型中密码协议的参数化保密性验证问题。经典Dolev-Yao保密性问题询问协议是否无论执行多少次都不会泄露秘密，而参数化保密性则要求保密性在所有可能的系统规模（即参与者数量）上一致成立，其中规模被视为参数。这一视角
An AI Approach to Verified Production Cryptographic Libraries
该论文提出 CryptoProver，一个基于人工智能的系统，用于自动合成密码学库的内部规范，并生成经过 Verus 验证的证明。研究背景是：密码学代码是关键基础设施，必须正确无误，但现有形式化验证生产库仍然困难。已有的基于语言模型的证明系
ZKP Security Tools and Verification: Coverage, Effectiveness, Adoption, and Challenges
零知识证明（ZKP）已成为隐私和可验证计算的核心技术，广泛应用于保护处理数十亿美元的数字货币区块链以及处理敏感个人数据的身份应用。然而，ZKP系统复杂，细微的实现错误可能完全破坏其安全保障，使攻击者能够伪造货币或身份证明。为此，研究人员和从
DualityCert: Verifier-Gated Language-Model Repair of Broken Duality Claims in Quantum Field Theory
该论文提出 DualityCert，一个专为四维 N=1 quiver 规范理论中 Seiberg 对偶性声明设计的符号验证器。验证器检查 't Hooft 异常匹配、超势 R-荷一致性、中心荷匹配以及一个有界的手征环代理。通过验证的声明获
Mission-Level Runtime Assurance for LLM-Assisted ISR Swarms over a Verification-Aware Fabric
该论文针对LLM辅助自主机器人蜂群在执行协作情报、监视与侦察（ISR）任务时面临的组合保证失败问题，提出了一种三层（平台/小队/任务）组合运行时验证框架。首先，论文指出现有的单平台防护机制无法检测跨平台违规行为，例如多个平台各自执行合规动作
HarnessLLM: Rust Verification Harness Generation with Large Language Models
Rust语言的所有权模型和类型系统提供了强大的内存安全保障，但unsafe代码和运行时panic依然带来显著风险。形式化验证是确保内存安全的关键，然而开发验证harness（验证框架）是一项具有挑战性的手动任务。虽然大语言模型在各类代码分析