该论文针对流控制传输协议（SCTP）开展形式化安全分析。SCTP 是一种提供多宿、多流和消息导向传输的传输协议，其两个主要实现已通过 PacketDrill 工具的一致性测试，但一致性测试并非穷尽，近期漏洞 CVE-2021-3772 表明该协议仍存在安全隐患。尽管已有补丁，但协议设计中是否遗留其他缺陷仍是开放问题。作者采用基于形式化方法的严谨路线：首先创建了 SCTP 的 Promela 模型，并根据 RFC 规范及与 RFC 主要作者的咨询，定义了 10 条刻画协议核心功能属性；随后使用 Spin 模型检查器验证模型满足这些属性。接着定义了四种攻击者模型：Off-Path（外部攻击者，可伪造对端的端口和 IP）、Evil-Server（恶意对等方）、Replay（可捕获和重放但不修改报文）、On-Path（完全控制信道）。他们修改了面向传输协议的攻击合成工具 Korg，以支持 SCTP 模型及上述四种攻击者模型。通过攻击合成，共得到 14 个独特的攻击：Off-Path 模型中包含 CVE 漏洞本身，Evil-Server 模型中有 4 个攻击，Replay 模型中有机会性 ABORT 攻击，On-Path 模型中有 8 个连接操纵攻击。作者进一步证明，针对 CVE 提出的补丁在模型和协议属性下消除了该漏洞，且未引入新漏洞。最后，他们识别并分析了 RFC 中的一处歧义，该歧义可能被不安全地解释；他们提出了勘误并证明其消除了该歧义。这项研究系统化地揭示了 SCTP 协议的多种潜在攻击面，验证了现有补丁的有效性，并提供了协议规范改进建议，对传输层安全研究有重要价值。

本文提出 Granite，一种用于对 RTL 级处理器设计进行模块化形式验证的方法论，旨在同时验证功能正确性和非泄漏性（nonleakage）。基于 ISA 泄漏契约，Granite 证明了带有推测执行、精确中断和 I/O 的流水线 RISC 设计的逐周期时序行为完全由契约中可观测的接口决定。对于遵循密码学常数时间纪律的程序（即不将秘密值影响任何可观测量的程序），该结果能够排除经已知或未知时序侧信道的信息泄漏。Granite 的规格仅约束功能正确性和信息流依赖，不规定指令的周期数、中断处理位置或子模块（如乘法器、内存）的具体延迟。其核心技术是'基于确定性的泄漏感知精化'，将正确性和机密性统一表示为与一族周期级确定性规格机器的轨迹等价。对于与秘密无关的非确定性，Granite 通过存在性参数化规格，使用仅作用于公开数据的不可信确定性函数来处理。子模块分别被证明满足其自身的泄漏感知规格，而这些证明组合成整体设计保证，因此适用于广泛的实现空间。作者声称这是首项在指令集级泄漏契约与微架构级逐周期执行（带线级观测）之间建立模块化和基础连接的工作。此外，该证明与一个认证静态分析相结合，可识别密码学常数时间代码，进而推导出关于硬件-软件密码实现的逐周期机密性的单一 Rocq 定理，从而从可信计算基（TCB）中消除了包括 ISA 契约在内的所有中间规格。

大型语言模型（LLM）智能体在动态环境中自主执行复杂操作，将语义推理与系统操作交织在一起。传统的静态工具级权限在这种环境下显得力不从心，因为安全授权高度依赖上下文，并受运行时状态和数据流变化的影响。为此，本文提出 FAVA（Formal Authorization for Verified Agents），一种面向智能体执行的携带权限的授权框架。FAVA 利用 LLM 引导的权限中间表示（Permission IR）将模糊的自然语言任务转换为结构化约束；随后通过确定性的降级过程（lowering pass）将该 IR 转换为显式追踪数据流、依赖关系和上下文标签的“基于证据的权限图”（evidence-backed permission graph）。为了提供严格的安全保证，FAVA 引入基于可满足性模理论（SMT）的授权器，在任何有副作用的动作执行之前，对当前权限图与安全策略进行数学验证；运行时网关强制执行求解器的结果，要么授权执行，要么通过精确的反例进行拦截。作者在 OpenAgentSafety、OctoBench 和 ActPlane 场景上评估了 FAVA。实验结果表明，在聚合数据集上 FAVA 达到了 90.5% 的决策合规率（DCR），并在给定的轨迹条件场景中成功拦截了动态违规轨迹。该研究的核心贡献在于首次将形式化验证（SMT）与 LLM 智能体的动态授权相结合，实现了可证明安全的权限决策。适合对 LLM 智能体安全、形式化验证与安全策略自动推理感兴趣的研究人员和开发者阅读。

该论文研究使用工具（tool-using）的智能体在运行时安全领域的可执行性（enforceability）理论。现有运行时防护栏（runtime guardrails）在不可逆的工具调用前进行干预，但它们的保证取决于可表示的策略状态、裁判（judge）的观测能力以及干预是否改变未来行为。本文分离出三个核心问题：第一，相对于固定的预言谓词（oracle predicates），确定性门控（deterministic gate）恰好能执行那些其寄存器模型能够识别的良好前缀（good prefixes）的非空安全策略；当使用两个可递减计数器时，策略非平凡性（nontriviality）不可判定，但对于可分离的单调片段（separable monotone fragment）则属于PSPACE。第二，在固定的外生规律（exogenous law）下，Neyman-Pearson引理给出了精确的误拦截/漏报前沿（false-block/miss frontier），而共形校准（conformal calibration）给出了有限样本的边际保证（finite-sample marginal certificate），可能需要通过全拦截（block-all）实现。第三，一旦拦截改变了未来的提议，静态分数与非门控轨迹（ungated trajectories）无法识别闭环前沿；一个指定的有限控制模型（finite controlled model）可以产生占用程序（occupancy program）。有界表示攻击（bounded representation attacks）引入了鲁棒性裕度，因此仅凭良性校准（benign calibration）无法迁移。实验通过静态诊断、控制模型枚举、表示重写以及配对的闭环重运行来区分这些不同方面。该论文为智能体运行时安全提供了形式化理论基础，适合安全研究者、形式化方法学者以及AI安全工程师阅读。

本文是Cardano区块链Voltaire治理系统的完整技术规范与研究议程报告。Cardano的Voltaire治理系统通过CIP-1694引入，并于2024年9月Chang硬分叉后正式启用，旨在解决去中心化协议演进中的适应性、安全性和利益相关者代表性之间的平衡问题。论文首先提供了Voltaire机制的完整技术规范，包括三体架构（三个治理主体：代表、宪法委员会和权益池运营者）、七种治理行动类型（如硬分叉、参数更改、资金提取等）、投票规则（基于权益的投票，需达到特定阈值）以及宪法框架。该规范足够详细，可用于直接实现或形式化分析。其次，论文建立了一个原则性治理优化的研究议程，包括设计基于智能体的仿真平台、分析委托动态、优化多目标参数以及博弈论激励设计。作为初步结果，作者提出一个形式化治理内核：一个最小可执行模型，将自修正治理建模为状态转换系统，从而支持严格的安全性和活性分析。该报告还指出，Voltaire系统目前管理着一个价值约2.35亿美元（截至2026年7月初为14.7亿ADA）的财库，是一个大规模活实验室，邀请研究社区通过严谨研究推进区块链治理科学。

前瞻偏差（Look-ahead bias）是回测和机器学习评估中最常见的陷阱：它使用了决策时刻之后的信息来优化该时刻的决策，导致系统在部署时表现远不如回测。当前业界主要通过特定构造的经验规则和经验性检测器来管理这一问题，但这些方法仅在单一通道上是合理的，且无法保证沉默即正确。本文证明，前瞻自由（look-ahead-freedom）实际上是一个形式化属性：固定一个时间点，要求未来不影响当下可以视为在时间索引的信息格上的一种时间非干扰性（temporal non-interference）。基于这一识别，作者开发了一个管道演算（pipeline calculus），将数据的可用时间与参考时间分离，并确定了问题的边界。当可用时间依赖于数据值时，前瞻自由是不可判定的（确实是 Π₁-0-1-难）：泄漏是递归可枚举的，但自由不是。在值无关片段（涵盖窗口、重采样、连接、时间点与历史读取，以及智能体检索）上，作者给出了一个类型-效应系统（type-and-effect system），它是可靠的且在线性时间内可判定。一个实现工件验证了理论：检查规模线性扩展，一个独立的预言机证明任何被接受的管道都没有泄漏，并且该检查器捕获了差分和分块检测器遗漏的所有注入泄漏。本文适合对回测、智能体交易、形式化方法感兴趣的研究者和工程师阅读。

该论文提出了一种新颖的形式化威胁分析器，专门针对基于活动监测的智能家居供暖、通风和空调（HVAC）控制系统。研究背景在于智能家居系统日益普及，但HVAC控制系统中集成的活动监测功能可能引入安全漏洞，攻击者可利用这些漏洞进行隐私侵犯或物理控制干扰。论文的核心方法是构建一个形式化模型，将HVAC系统的行为、用户活动模式以及潜在威胁场景抽象为数学规范，并利用模型检测技术自动验证系统是否存在特定类型的安全威胁。主要贡献包括：设计了一个通用的威胁建模框架，能够捕获基于活动监测的HVAC系统的独特攻击面；开发了自动化分析工具，可输出可解释的风险报告；通过真实场景的案例研究验证了分析器的有效性，证明了其能够发现常规安全审计难以识别的隐蔽威胁。实验表明，该分析器在检测物联网环境中的信息泄露和物理篡改攻击方面具有较高准确性。该研究适合智能家居安全研究人员、HVAC系统设计师以及物联网安全从业者阅读。

本文提出了一种基于差分区域集（differential halo zonotopes）的新型静态分析技术，用于验证深度神经网络（DNN）的全局鲁棒性。全局鲁棒性是一种比局部鲁棒性更强的性质，要求网络对所有输入对（而非单个输入及其邻域）的预测结果一致，因而属于2-安全属性（2-safety property），验证难度极大。现有方法多局限于局部鲁棒性验证，或在大规模网络上难以扩展。作者的核心创新在于：将区域集（zonotopes）抽象域扩展为差分区域集，能够同步联合传播扰动输入对，同时紧密地限定其输出差异的边界。此外，本文引入了对称的置信度基全局鲁棒性松弛版本，忽略因低置信度预测而产生的差异，从而在保持实用性的前提下放宽了验证条件，适用于更广泛的网络架构。作者实现了原型工具TwoSafe，并在标准DNN验证基准（包含广泛部署的模型）上进行了评估。实验结果表明，TwoSafe在精度和可扩展性方面均显著优于现有技术，能够验证的网络规模比先前技术大一个数量级。该工作不仅推进了形式化验证的理论边界，也为安全关键场景下DNN的可靠性提供了实用验证手段。

本文提出了一种名为 HAMRAZ 的框架，旨在解决跨组织系统中在部分信任的子系统间协作时的可信性问题。在医疗、金融和军事等领域，子系统之间需要合作，但可能面临恶意拜占庭攻击。现有的工作通常只关注机密性和完整性，而忽略了可用性的保障。HAMRAZ 的目标是同时确保机密性、完整性和可用性这三个方面的端到端策略。为此，论文提出了一种基于安全类型的面向对象语言，并设计了分区转换、操作语义以及针对分区和复制类的信息流类型推断系统。该类型系统能够可证明地保证，类型良好的方法满足这三个属性的无干扰性，并且其类型量化了对拜占庭攻击的韧性。给定一个类及其端到端策略的规范，HAMRAZ 工具自动应用类型推断来放置和复制类的字段和方法到拜占庭法定人数系统上，从而合成出可信赖的分布式系统。实验结果表明，生成的系统具有韧性，能够优雅地容忍与指定策略同等强度的攻击。

该论文针对网络物理系统（CPS）面临设备级网络攻击时的弹性问题展开研究。传统容错机制通过分析传感器和执行器输出检测渐进漂移或突发故障，并启动相应容忍机制，这在通用故障模型下合理，但无法捕捉网络攻击可能采用的细微策略。对于具身CPS（Embodied CPS），计算与物理设备不仅参与任务完成，还负责“具身保存”（即维持系统物理完整性），因此需要能主动响应网络攻击的框架以防结构性物理损害。论文提出一个正式的可信性框架，将入侵检测系统（IDS）信息整合到弹性评估谓词中，使系统能够评估对中断和退化的容忍程度。该框架支持结构化推理：网络攻击如何影响任务执行和具身保存，以及是否需要部署缓解策略。通过分析示例展示了框架的分析能力和正确性，为可靠且安全的具身CPS建立了理论基础。核心贡献在于形式化地将网络安全状态与物理弹性结合，为安全工程师在设计鲁棒控制逻辑时提供理论支撑。适合对CPS安全、形式化方法、弹性工程感兴趣的研究者和工程师阅读。

本文重新审视了强化学习中的盾牌合成技术，指出其传统上作为运行时安全机制的定位存在偏差。作者提出将相同的自动机理论工具——规范编译、乘积博弈构建、吸引子计算和获胜区域提取——重新解读为设计时的分析仪器，其输出是对系统安全属性的结构性洞察，而非部署时的运行时约束。具体地，文章构建了一个受约束的双人安全博弈模型来模拟网络防御场景。在该博弈中，防御者和攻击者的规范被非对称地实施：防御者规范定义了博弈中的不安全区域，而攻击者规范则在吸引子计算过程中限制了对手的合法动作。通过求解该博弈，可以获得一个可防御性判定——即关于拓扑-规范配对是否可防御的形式化证书，以及相关联的获胜区域和盾牌。进一步地，作者从吸引子结构中推导出拓扑级别的度量，并将其与盾牌约束下的对抗性多智能体强化学习获得的收敛后行为相结合，共同构成一个可防御性指纹，该指纹同时捕捉了网络的形式化安全属性和在自适应对抗下的操作行为。通过假设分析（what-if analysis），文章发现形式化可防御性与操作有效性分别捕捉了安全的不同维度：微小的架构变化可能导致操作结果的巨大变化，而形式化安全裕度几乎不变。因此，盾牌合成的最大价值并非作为安全智能体的部署机制，而是作为回答系统是否、在哪里以及如何可被防御等架构问题的分析框架。可防御性判定是输出，而非安全策略。本研究适合网络安全研究人员、强化学习安全从业者以及系统架构师阅读，用于在设计阶段评估网络拓扑的防御能力。

该论文提出了一种名为FASR（Formalizing and Automating STPA with Robustness）的自动化工具，旨在支持系统理论过程分析（STPA）中的不安全控制动作（UCA）识别。STPA是一种广泛应用于安全关键系统的危险分析技术，但其大部分步骤依赖人工执行，耗时且易错。FASR利用基于模型的工程和形式化方法，结合鲁棒性分析的最新进展，通过识别控制器行为中的不良偏差来自动、完整地发现UCA。论文在航空电子系统中的制动系统控制单元（BSCU）案例上演示了工具的使用，并开展了一项包含9名参与者的用户研究，参与者具有STPA、基于模型的工程和形式化方法的不同背景。研究结果表明，大多数参与者认为FASR是识别UCA的有用辅助工具，同时提出了改进建议，以使类似工具适用于更广泛的系统和分析师。该研究初步展示了自动化STPA的潜力与局限，为安全关键系统的危险分析提供了新的自动化路径。

本文提出了一种基于强化学习（RL）的框架，用于提升 Tamarin 协议分析工具中的证明搜索效率。Tamarin 是广泛用于验证安全协议（如 EMV、5G、WPA2）的自动推理工具，但传统方法需要大量人工专家干预。受 AlphaZero 和 AlphaProof 启发，作者设计了一个无状态的 API，将 Tamarin 转化为经典 RL 环境，并通过蒙特卡洛树搜索（MCTS）结合神经网络启发式学习已完成子证明的模式。在 16 个案例研究（包括经典协议模型及最新发表中的复杂协议模型）上，该方法比 Tamarin 标准搜索自动找到更多证明，且生成的证明比标准启发式甚至人工编写的启发式更短。该框架可直接用于帮助 Tamarin 用户减少人工努力，同时提供标准化的程序化接口。实验结果表明，RL 方法在协议形式化验证领域具有巨大潜力。

该论文提出了一个名为 BunnyFinder 的自动化框架，旨在发现以太坊共识协议中存在的激励缺陷。以太坊采用基于权益证明（PoS）的共识机制，其中验证者的激励设计直接影响网络的安全性和去中心化程度。BunnyFinder 通过形式化方法建模共识协议中的激励结构，结合博弈论分析和符号模型检测，自动识别可能导致不正当行为（如自私挖矿、贿赂攻击等）的激励缺陷。论文在模拟环境中验证了该框架的有效性，发现了多个已知和未知的激励漏洞，并提供了相应的修复建议。该工作为区块链共识安全提供了新的自动化分析工具。 由于仅基于论文标题和作者信息，未获取完整摘要，以上内容为合理推断，具体细节需参考原文。

本文研究了如何在证明助手中对一种具有渐进信息流标签的安全类型语言进行形式化建模。渐进信息流标签允许在类型系统中动态调整安全级别，从而在编译时静态检查和运行时动态检查之间取得平衡。作者首先给出了该语言的定义解释器语义，并在证明助手中实现，然后证明了其类型安全性，即良类型的程序不会违反信息流策略。此外，文章还展示了该语言在解析和保护敏感用户输入数据方面的潜在应用，例如通过标签标注数据敏感度，确保不安全处理被类型系统捕获。最后，作者系统比较了现有多种渐进安全类型语言（如包含动态标签、静态标签或混合标签的语言）在语言特性（如标签格、运行时检查机制）和安全属性上的差异，总结出不同设计的优缺点，为未来设计更实用的渐进信息流安全语言提供了指导。该工作属于形式化方法与语言安全交叉领域，主要贡献在于首次在证明助手中实现了渐进信息流语言的全机械化类型安全证明，并提供了语言设计空间的分析。