Neuroforger: certified violation witnesses for smart contracts verification via LLMs
该论文提出了一种结合大型语言模型（LLMs）与形式化方法的智能合约验证新框架。当前智能合约验证面临两大挑战：自然语言表达的属性内在存在歧义，且LLM的答案缺乏正确性保证。作者通过两个创新点同时解决这些问题：1）设计了一种扩展Solidity
#formal-verification
共收录 95 条相关情报。
← 返回所有主题Bridging Theory and Practice: An Executable Taxonomy of Security Properties for ProVerif and Tamarin
该论文针对形式化验证工具ProVerif和Tamarin在安全协议验证中的使用门槛问题，提出了一种系统化的、基于证据的安全属性分类法。通过系统综述2022-2025年间使用这两种工具的53篇近期研究，论文提取并整理了当前被实际验证的安全属性
Provably Secure Agent Guardrail
本文针对大型语言模型从有限生成引擎向具有广泛执行权限的智能代理转型过程中出现的失控问题，提出了一种基于逻辑推理基本局限性的新型安全范式。现有防御架构主要依赖经验性语义护栏和概率性大模型裁决器，无法在复杂语义符号解耦攻击下提供确定性安全下界。
An I/O Separation Model for Formal Verification of Kernel Implementations.
本文针对操作系统内核中 I/O 分离不足导致的安全问题，提出了一种形式化的 I/O 分离模型。该模型基于 I/O 传输授权定义分离策略，与具体硬件无关，能够防止恶意驱动通过操控设备绕过 I/O 隔离。作者在 Dafny 语言中对该模型进行了
Heimdall: Formally Verified Automated Migration of Legacy eBPF Programs to Rust
该论文聚焦于Linux内核扩展程序eBPF的安全迁移问题。eBPF程序被广泛用于网络、可观测性及安全策略执行，但其内核验证器仅检查低级内存安全和终止性，未强制许多高级源级属性，如初始化规则、schema一致性或错误处理。作者识别出六类源级b
Pramana: A Protocol-Layer Treatment of Claim Verification in Autonomous Agent Networks
该论文提出了Pramana，一个用于自治代理网络中的声明验证的协议层解决方案。在受监管领域中，自主代理对每个关键输出必须产生一个可审计的验证工件，记录声明内容、来源、执行者、时间和方式。当前的生产验证分为两个未标准化的方向：概率性判决模式（
Natural Language based Specification and Verification
该论文针对大型语言模型（LLM）生成代码中可能引入安全漏洞的问题，提出了一种基于自然语言的规约与验证方法。传统形式化验证需要严格的规约语言，而现有利用LLM生成规约的方法效果有限。作者另辟蹊径，探索让LLM同时承担规约生成和组合验证的任务，
Security Analysis of Master-Password-Protected Password Management Protocols.
本文首次对主密码保护的密码管理协议（M3PM）进行了系统性的形式化安全分析。密码管理器（PM）帮助用户管理登录凭证，缓解记忆大量密码的负担，而M3PM协议描述了客户端与PM服务器之间的交互：客户端使用主密码进行身份验证，服务器协助跨设备检索
μCFI: Formal Verification of Microarchitectural Control-flow Integrity.
该论文提出了一种名为μCFI（微架构控制流完整性）的形式化验证方法，旨在解决现有控制流完整性（CFI）机制在微架构层面的安全漏洞。传统的CFI仅在软件或ISA（指令集架构）层面保证控制流安全，但无法抵御利用微架构侧信道或瞬态执行攻击（如Sp
KVerus: Scalable and Resilient Formal Verification Proof Generation for Rust Code
形式化验证是确保软件正确性和安全性的最高保证，但将其应用于大规模、不断演变的系统仍面临重大挑战。尽管大语言模型（LLM）在自动证明生成方面展现出潜力，但由于无法处理复杂的跨模块依赖关系或代码库及验证工具链的变化，它们在实际应用中常常失败。本
Stable Agentic Control: Tool-Mediated LLM Architecture for Autonomous Cyber Defense
本论文提出了一种面向自主网络防御的工具中介LLM架构（Stable Agentic Control），旨在解决现有方法无法为高对抗压力下的自主系统提供形式化保证的问题。研究背景源于安全运营中心（SOC）在敌对压力下配置端点检测与响应（EDR
FIDO2, CTAP 2.1, and WebAuthn 2: Provable Security and Post-Quantum Instantiation.
本文对FIDO2、CTAP 2.1和WebAuthn 2这一现代无密码认证协议族进行了形式化安全分析，并提出了后量子安全的实例化方案。研究者首先构建了这些协议的符号模型，涵盖了注册、认证、凭证管理等多阶段交互，并利用Tamarin Prov
A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer.
本文对IETF QUIC协议记录层的安全性进行了系统研究。QUIC是传输层协议，其记录层负责数据包加密和头部保护，IETF标准第30版相比Google原始协议和早期草案有重大变化。作者首先提出了一种新的安全定义——带半隐式nonce的认证加
Beyond Code Reasoning: A Specification-Anchored Audit Framework for Expert-Augmented Security Verification
该论文提出了一种名为 SPECA 的基于规范锚定的安全审计框架。传统代码审计工具主要关注代码层面的漏洞模式，但对于由自然语言规范驱动的系统（如协议栈、共识实现、密码库等），其安全约束和正确性条件定义在规范中，代码级工具无法检测此类漏洞。SP
Prime-Field PINI: Machine-Checked Composition Theorems for Post-Quantum NTT Masking
本文（系列第6篇）聚焦后量子密码学中基于NTT（数论变换）硬件的算术掩码组合安全性。布尔掩码的组合理论（NI、SNI、PINI）已成熟，但素数域上的算术掩码（NTT后量子密码的基础）缺乏类似理论。作者提出并形式化证明了素数域上PINI（Pr