Analysis of the Security Design, Engineering, and Implementation of the SecureDNA System.
本文分析了 SecureDNA 系统的安全设计、工程与实现。SecureDNA 是一个用于 DNA 合成仪的危险序列筛查系统，它通过新颖的密码学手段在查询过程中隐藏订单请求和危险数据库的内容。作者基于版本 1.0.8 的源代码，对密钥管理、
#formal-methods
共收录 40 条相关情报。
← 返回所有主题Why Formal Monitors Fail: Attack Distribution Entropy as a Coverage Bound for LTL-Based LLM Agent Safety
本文研究基于线性时序逻辑（LTL）和有限状态自动机（FSA）的运行时安全监控器在防御大语言模型（LLM）智能体工具调用序列时的失效原因。实际部署中，同一监控器在不同模型架构上对攻击的覆盖率差异巨大：在部分架构上可达 68-75%，而在另一些
A Formal Analysis of SCTP: Attack Synthesis and Patch Verification.
该论文针对流控制传输协议（SCTP）开展形式化安全分析。SCTP 是一种提供多宿、多流和消息导向传输的传输协议，其两个主要实现已通过 PacketDrill 工具的一致性测试，但一致性测试并非穷尽，近期漏洞 CVE-2021-3772 表明
What Syntax Cannot See: The Dynamic Syntactic Invariance Principle and Several Instances of the Same Hidden Assumption, and a Contradiction
本论文提出了一种统一的跨领域研究方法：寻找既有结论中未被察觉的隐含假设，将其显式化为一个可变参数，然后证明当该假设被移除后，结论会发生什么变化。作者将此方法的形式化核心称为“动态句法不变性原理”（Dynamic Syntactic Inva
Assuming You Knew: Fixing an Epistemic Semantics for Flow Policies Using Agentic AI
该论文针对程序信息流策略的语义形式化问题进行修正与验证。许多高级安全需求涉及程序中允许的信息流动，但由于存在选择性降级（selective downgrading）而难以精确表达。认识逻辑（epistemic logic）中的概念被视为一种
Formalization of security
该论文是 Gilles Barthe 撰写的一篇关于安全形式化的综述章节，聚焦于证明助手（proof assistants）在计算机安全领域的应用。研究背景是：设计与实现必须满足预期的安全属性，而证明助手能够通过机械化推理严格验证这些属性，
Granite: A Modular Methodology for Foundational Verification of Hardware-Software Leakage Contracts
本文提出 Granite，一种用于对 RTL 级处理器设计进行模块化形式验证的方法论，旨在同时验证功能正确性和非泄漏性（nonleakage）。基于 ISA 泄漏契约，Granite 证明了带有推测执行、精确中断和 I/O 的流水线 RIS
FAVA: Formal Authorization for Verified Agents with Evidence-Backed Permission Graphs
大型语言模型（LLM）智能体在动态环境中自主执行复杂操作，将语义推理与系统操作交织在一起。传统的静态工具级权限在这种环境下显得力不从心，因为安全授权高度依赖上下文，并受运行时状态和数据流变化的影响。为此，本文提出 FAVA（Formal A
What Can Be Enforced? A Theory of Certified Runtime Safety for Tool-Using Agents
该论文研究使用工具（tool-using）的智能体在运行时安全领域的可执行性（enforceability）理论。现有运行时防护栏（runtime guardrails）在不可逆的工具调用前进行干预，但它们的保证取决于可表示的策略状态、裁判
Cardano's Voltaire Governance: Complete Specification and Research Program
本文是Cardano区块链Voltaire治理系统的完整技术规范与研究议程报告。Cardano的Voltaire治理系统通过CIP-1694引入，并于2024年9月Chang硬分叉后正式启用，旨在解决去中心化协议演进中的适应性、安全性和利益
Look-Ahead-Freedom as Temporal Non-Interference: A Verifiable Correctness Property for Backtesting and Agentic Trading Pipelines
前瞻偏差（Look-ahead bias）是回测和机器学习评估中最常见的陷阱：它使用了决策时刻之后的信息来优化该时刻的决策，导致系统在部署时表现远不如回测。当前业界主要通过特定构造的经验规则和经验性检测器来管理这一问题，但这些方法仅在单一通
Poster: A Novel Formal Threat Analyzer for Activity Monitoring-based Smart Home Heating, Ventilation, and Cooling Control System.
该论文提出了一种新颖的形式化威胁分析器，专门针对基于活动监测的智能家居供暖、通风和空调（HVAC）控制系统。研究背景在于智能家居系统日益普及，但HVAC控制系统中集成的活动监测功能可能引入安全漏洞，攻击者可利用这些漏洞进行隐私侵犯或物理控制
Differential Zonotopes for Verifying Global Robustness of DNNs
本文提出了一种基于差分区域集（differential halo zonotopes）的新型静态分析技术，用于验证深度神经网络（DNN）的全局鲁棒性。全局鲁棒性是一种比局部鲁棒性更强的性质，要求网络对所有输入对（而非单个输入及其邻域）的预测
HAMRAZ: Resilient Partitioning and Replication.
本文提出了一种名为 HAMRAZ 的框架，旨在解决跨组织系统中在部分信任的子系统间协作时的可信性问题。在医疗、金融和军事等领域，子系统之间需要合作，但可能面临恶意拜占庭攻击。现有的工作通常只关注机密性和完整性，而忽略了可用性的保障。HAMR
A Formal Resilience Framework for Cyber-Physical Embodied Systems under Device-Level Cyberattacks
该论文针对网络物理系统（CPS）面临设备级网络攻击时的弹性问题展开研究。传统容错机制通过分析传感器和执行器输出检测渐进漂移或突发故障，并启动相应容忍机制，这在通用故障模型下合理，但无法捕捉网络攻击可能采用的细微策略。对于具身CPS（Embo
Beyond Runtime Enforcement: Shield Synthesis as Defensibility Analysis for Adversarial Networks
本文重新审视了强化学习中的盾牌合成技术，指出其传统上作为运行时安全机制的定位存在偏差。作者提出将相同的自动机理论工具——规范编译、乘积博弈构建、吸引子计算和获胜区域提取——重新解读为设计时的分析仪器，其输出是对系统安全属性的结构性洞察，而非
FASR: Automated Identification of Unsafe Control Actions in STPA
该论文提出了一种名为FASR（Formalizing and Automating STPA with Robustness）的自动化工具，旨在支持系统理论过程分析（STPA）中的不安全控制动作（UCA）识别。STPA是一种广泛应用于安全关
Less Effort, Shorter Proofs: Reinforcement Learning for Security Protocol Analysis in Tamarin
本文提出了一种基于强化学习（RL）的框架，用于提升 Tamarin 协议分析工具中的证明搜索效率。Tamarin 是广泛用于验证安全协议（如 EMV、5G、WPA2）的自动推理工具，但传统方法需要大量人工专家干预。受 AlphaZero 和
BunnyFinder: Finding Incentive Flaws for Ethereum Consensus.
该论文提出了一个名为 BunnyFinder 的自动化框架，旨在发现以太坊共识协议中存在的激励缺陷。以太坊采用基于权益证明（PoS）的共识机制，其中验证者的激励设计直接影响网络的安全性和去中心化程度。BunnyFinder 通过形式化方法建
Mechanized Type Safety for Gradual Information Flow.
本文研究了如何在证明助手中对一种具有渐进信息流标签的安全类型语言进行形式化建模。渐进信息流标签允许在类型系统中动态调整安全级别，从而在编译时静态检查和运行时动态检查之间取得平衡。作者首先给出了该语言的定义解释器语义，并在证明助手中实现，然后