Security Properties of Neural Networks as Decision Problems
该论文从计算复杂性角度重新审视已部署神经网络的安全认证问题。验证文献长期聚焦鲁棒性等少量性质，但作者指出实际部署中还存在一类未被系统分类的决策问题：模型是否携带训练阶段植入的后门、存储参数故障是否会把网络推入不安全状态、输出是否泄露输入中的
#formal-methods
共收录 40 条相关情报。
← 返回所有主题Endogenous Interpretation
该论文提出「内生解释」(endogenous interpretation) 这一理论视角,主张程序、解释器、机器以及派生的执行语言并不是彼此分离的语义对象,而是同一个可执行状态转移关系的不同参数化形式。作者进一步指出,每一种具体实现都携带
Authorization Revocation for Long-Running AI Agents: Root-Scoped Quiescence under Delegation and Asynchronous Execution
该论文研究长时运行的 AI 智能体（long-running AI agents）在授权撤销方面的根本性缺陷。这类智能体往往比发起它的进程存活更久，其存活载体包括长期凭据、委托出去的子任务、消息队列、回调、资源预留以及服务提供方侧的操作记录
From Specs to Apps: Verifying and Monitoring Models of Signal and WhatsApp
该论文聚焦于一个长期存在的安全工程问题：即时通信协议的「形式化规范保证」与「实际运行实现行为」之间存在落差。Signal 协议为数以十亿计的用户提供加密通信，是 WhatsApp（全球用户量最大的消息应用）与 Signal 官方客户端的底层
A2ABreak: Systematic Security Analysis of the A2A Protocol
该论文《A2ABreak: Systematic Security Analysis of the A2A Protocol》针对由 Linux 基金会治理、正在成为多智能体生态水平通信层的 Agent2Agent（A2A）协议开展首次系统
On Re-engineering the X.509 PKI with Executable Specification for Better Implementation Guarantees.
X.509 公钥基础设施（PKI）是广泛使用的可扩展且灵活的身份认证机制，但其标准文本由自然语言编写，存在设计复杂、歧义和欠规定（under-specification）等问题，导致实现者难以完全遵循标准。实际中，很多 X.509 实现库因
When Does Authorization End? Effect Closure at Provider Boundaries
该论文研究分布式系统与授权模型中的一个根本性缺口：授权“何时”才算真正结束？论文指出，即使系统报告撤销完成、达到干净状态或操作成功，先前已授权的执行路径仍可能在提供方（如消息中间件、编排平台）未违反自身契约的前提下，继续产生应用程序明确拒绝
Verification of $K$- and Infinite-Step Strong/Weak Anonymity Using Concurrent Compositions
本文研究部分可观测离散事件系统中的匿名性验证问题。匿名性是一种信息流安全属性，其核心思想是：在外部观察者通过系统输出（观测）推断系统内部状态时，系统不应让某一时刻的状态被唯一确定，从而保护用户隐私。在离散事件系统框架下，已有 K-步匿名性和
Information Flow Control in Off-Chain Components
本文针对带有链下组件的区块链智能合约语言，建立了一种形式化模型。链下组件是在区块链节点网络之外的指定位置执行的智能合约片段，但它们与链上合约状态保持同步。它们不仅响应链上状态的变化，还能将外部世界的事件（如股票价格、天气数据）通知给链上组件
Rational Dolev--Yao Attackers: Decidable Incentive-Aware Verification of Security Protocols in Strategic Logic
本文提出“理性 Dolev-Yao 攻击者”模型，将传统符号化协议验证中的 Dolev-Yao 入侵者扩展为具有成本与收益考量的理性主体。传统 DY 入侵者在知识允许范围内执行所有可能动作，不论是否有利于达成目标；而真实对手会最大化效用，仅
An Interactive Prover for Protocol Verification in the Computational Model.
这篇 arXiv 论文提出了一套用于在计算模型下对安全协议进行机械化验证的框架和交互式证明器。研究背景是：安全协议设计的正确性至关重要，需要坚实的数学基础和计算机辅助方法。此前 Bana 和 Comon 提出的形式化方法只能分析固定会话数目
SoK: Computer-Aided Cryptography.
本文是一篇关于计算机辅助密码学（Computer-Aided Cryptography）的系统化综述（SoK），旨在梳理该领域的研究进展与应用边界。随着密码学协议和实现日益复杂，传统手工分析与测试难以保证安全性与正确性。计算机辅助密码学通过
CheckMate: Automated Game-Theoretic Security Reasoning.
本文提出 CheckMate 框架，用于全自动化的博弈论安全分析，特别关注区块链技术。CheckMate 将协议建模为博弈，并分析其博弈论安全性，即激励兼容性和拜占庭容错性。该框架要么通过提供防御策略证明协议是安全的，要么给出所有可能的攻击
Automatic Detection of Speculative Execution Combinations.
该论文针对现代处理器中推测执行机制的安全分析问题展开研究。现代处理器为提升性能，采用了多种推测执行机制，例如分支预测、内存依赖推测、数据值推测等，这些机制会推测性地执行不同类型的指令。攻击者可能同时利用多种推测机制，在单个瞬态执行窗口内触发
Synthesis of Sound and Precise Leakage Contracts for Open-Source RISC-V Processors.
该论文针对开源 RISC-V 处理器中微架构侧信道的信息泄露问题，提出了一种自动化合成泄漏合约（leakage contracts）的方法。泄漏合约是近期提出的、用于指令集架构（ISA）层面的安全抽象，旨在精确刻画处理器通过微架构侧信道可能
Sound Enforcement of Dynamic Release Information Flow Policy-Full Version
本文研究信息流分析（Information Flow Analysis）在真实系统中的应用问题。信息流分析是评估机密性和完整性的主要方法，但实际采用率不高，根本原因在于理论与实践的差距：现有技术通常假设安全策略是静态的（即数据保密性不变），
Velosiraptor: Code Synthesis for Memory Translation
操作系统（OS）的安全运行依赖对内存硬件（如 MMU、IOMMU）的正确配置，这为运行中的不可信应用提供隔离与完整性强约束。然而，硬件厂商不断推出新型地址转换与保护机制，其配置方式各异，导致 OS 开发者必须手动编写底层配置代码。这一过程既
Compositional Security for Reentrant Applications.
该论文聚焦于智能合约等可重入应用（Reentrant Applications）的组合安全（Compositional Security）问题。智能合约中反复出现的灾难性漏洞（如著名的重入攻击）表明，在编写需要与恶意代码组合运行的软件时，我
dfence: Fine-Grained Speculation Barriers for Efficient and Effective Hardware-Software Protection in the Spectre Era (Extended Version)
本文提出了一种名为 dfence 的新型 CPU 指令，旨在以硬件-软件协同的方式高效缓解推测执行攻击（如 Spectre-PHT 和 Spectre-STL）。现有的软件缓解方案（如 Speculative Load Hardening,
UC, Categorically: Rigorous Diagrammatic Proofs
这篇论文将范畴论应用于密码学中的通用可组合性（UC）框架，以建立安全组合的严格数学理论。UC框架由Canetti提出，用于评估协议在并发环境中的安全性，但传统形式化依赖于交互式图灵机和复杂的概率论证明，难以扩展和验证。作者针对静态参与方和会