KaPilot: LLM-Assisted Generation of Kani Specifications for Unsafe Rust Verification
该论文提出了 KaPilot，一个基于大语言模型（LLM）的多智能体框架，用于自动生成 Rust 语言中 unsafe 代码内存安全的形式化规约（specifications），以支持使用 Kani 验证器进行形式化验证。Rust 的所有权
#formal-verification
共收录 95 条相关情报。
← 返回所有主题C-Verifier: Understanding and Formally Verifying Cross-Service Flaws in AWS Cognito.
该论文针对 AWS Cognito 服务中跨服务缺陷的识别与形式化验证问题展开研究。AWS Cognito 作为一项用户身份与访问管理服务，常与 API Gateway、Lambda 等其他 AWS 服务集成，这种跨服务组合可能引入安全漏洞
Boosting the Performance of High-Assurance Cryptography: Parallel Execution and Optimizing Memory Access in Formally-Verified Line-Point Zero-Knowledge.
本文针对高保证密码学协议形式化验证实现中存在的性能瓶颈问题，提出了一套通用的优化方法。以 Line-Point 零知识证明（LPZK）协议为案例，首先在 EasyCrypt 中实现了一个形式化验证的 LPZK 实现（未考虑性能），然后通过三
Interplay of Efficient Model Checking and Secure Processor Design: A Case Study on Secure Speculation.
该论文探讨了高效模型检查与安全处理器设计之间的相互作用，以安全推测（Secure Speculation）为案例。针对推测执行侧信道攻击（如Spectre）带来的安全威胁，传统缓解措施往往带来显著的性能开销或设计复杂性。论文提出一种形式化方
Vest: Verified, Secure, High-Performance Parsing and Serialization for Rust.
本论文针对 Rust 语言中解析和序列化操作的安全性与性能挑战，提出了一种名为 Vest 的新型框架。Rust 以其内存安全著称，但手写解析器和序列化器仍然容易出错且效率低下。现有方案（如 serde）虽提供自动化，但缺乏形式化验证，且难以
CryptoBap: A Binary Analysis Platform for Cryptographic Protocols.
该论文提出 CryptoBap，一个用于验证加密协议二进制代码安全属性的平台。研究背景是：现实中的加密协议实现可能因编译器优化、平台差异或编程错误而引入安全漏洞，而传统的形式化验证方法通常针对高级语言或协议规范，难以直接分析编译后的机器码。
Fine-Grained Trackability in Protocol Executions.
该论文聚焦于安全协议执行中的细粒度可追踪性问题，提出了一种新的形式化框架，用于在协议执行中精确追踪参与方的身份、行为及其状态变化。研究背景是现有协议追踪技术通常粒度较粗，难以应对复杂攻击场景（如混淆代理、重放攻击）。核心方法包括定义一种扩展
Logical Relations for Formally Verified Authenticated Data Structures.
本文针对认证数据结构（Authenticated Data Structures）的开发与实现正确性难题，提出了一种基于新关系分离逻辑的形式化证明方法。认证数据结构允许不可信的第三方执行操作并生成可验证的输出证明，但此类系统容易因实现错误导
LeanDY: Type-Based and Trace-Based Symbolic Protocol Verification in Lean
该论文提出了一种名为 LeanDY 的形式化验证框架，面向密码协议的安全性分析。现有工具要么全自动但表达能力有限，要么交互式证明灵活但自动化不足。LeanDY 通过结合基于类型推理（type-based reasoning）与基于轨迹推理（
Solver-Aided Constant-Time Hardware Verification.
本文提出 Xenon，一种求解器辅助的交互式形式化验证方法，用于证明 Verilog 硬件设计在常时执行。常时执行是抵御基于时序的侧信道攻击的关键属性。Xenon 通过引入常时反例的新概念，自动合成最小化秘密假设集合，并在交互式验证循环中定
Cryptographic certificates of validity for trustworthy AI
该论文针对当前AI智能体系统在可信执行与合规验证方面的挑战，提出了一种基于密码学有效性证书的新颖方案。核心思想是：首先将智能体应满足的正确性或策略条件形式化为逻辑谓词；然后将该谓词编译为多项式约束上的证人（witness）检查问题；最后利用
Semantic Non-Assembly: Privacy by Architectural Inertness Under Component Exposure
本文提出了一种名为“语义非组合”（Semantic Non-Assembly, SNA）的新型隐私保证框架。与传统的基于保密性、访问控制或统计披露限制的隐私模型不同，SNA 从“暴露发生时信息收益”的角度定义隐私：即使攻击者能够完全暴露和解
Guarded Equivalence Predicates for Scalable Formal Hardware Information-Flow Verification
本文针对硬件信息流（information-flow）的形式化验证中可扩展性不足的问题，提出了一种名为“受保护等价谓词”（Guarded Equivalence Predicates）的方法。在硬件安全验证中，自组合（self-compos
An In-Depth Symbolic Security Analysis of the ACME Standard.
本文对 IETF RFC 8555 标准化的 ACME（自动证书管理环境）协议进行了深入的符号安全分析。ACME 是 Web 公钥基础设施（PKI）的关键组成部分，被 Let's Encrypt 等证书颁发机构用于签发超过十亿张证书，目前大
P-Verifier: Understanding and Mitigating Security Risks in Cloud-based IoT Access Policies.
该论文针对基于云的物联网（IoT）访问策略中存在的安全风险展开研究。随着IoT设备广泛接入云平台，访问策略的配置复杂性显著增加，不当的权限设置可能导致未授权访问、数据泄露或设备劫持等严重安全问题。现有策略验证工具多针对单一云平台或通用网络策
GCD: Garbled, Corrected, Demonstrandum -- Fixing and Proving Go's Extended GCD Implementation
本文对 Go 标准库 `crypto/internal/fips140/bigmod` 中的 `extendedGCD` 实现进行了形式化验证。该实现用于 RSA 密钥对生成中的扩展欧几里得算法，是从 BoringSSL 移植而来。然而，研
Formal verification of the S-two AIR
本文介绍了使用Lean 4证明助手对StarkWare的S-two证明器中的代数中间表示（AIR）进行形式化验证的工作。S-two证明器用于在区块链上高效地证明用Cairo虚拟机语言编写的程序能够运行完成。该证明器通过一个代数中间表示（AI
Tridirectional Discriminating-Power Formal Verification of Smart Contract Reentrancy Defense Against Production-Deployed Solidity Source
本文提出了首个经过机器检查的OpenZeppelin重入防护模式正确性证明，该证明针对生产部署的Solidity源代码的Lean 4状态机模型。所有十三个定理都经过了机器检查，没有使用任何“sorry”或用户引入的公理，公理足迹仅由[pro
Formal Verification of Secure Encrypted Virtualization
该论文针对AMD SEV（安全加密虚拟化）技术缺乏形式化安全保证的问题，提出了一套形式化验证框架。AMD SEV是机密计算中的关键技术，通过硬件内存加密保护虚拟机内敏感数据。然而，现有实现缺乏对安全性属性的严格证明。研究首先对AMD SEV
Formalizing, Verifying and Applying ISA Security Guarantees as Universal Contracts.
该论文提出了一种全新的方法，用于形式化规范指令集架构（ISA）的安全保证。传统上，ISA的规范仅限于功能方面，且通常以非形式化的散文形式描述，缺乏对安全保证的精确刻画。作者引入了通用契约（universal contracts）的概念——这