本文针对具身网络物理系统（机器人等）在遭受主动网络攻击时面临的特殊安全困境展开研究。与纯信息系统不同，这类系统的攻击后果不仅涉及数据泄露，还可能直接威胁物理完整性与人身安全。现有安全方案（如入侵检测系统）虽擅长发现异常，却普遍缺乏运行时机制来判断：攻击造成的扰动是否可容忍、系统性能退化是否仍处于安全运行边界之内。这一缺失导致系统在攻击持续期间陷入“优雅失败瘫痪”（graceful failure paralysis）——无法区分安全的降级状态与灾难性危害。为填补该空白，作者提出并实现了 RobResilience：在 Webots 仿真环境中，基于 PR2 机器人与 ROS2 搭建的形式化弹性框架实现。该框架在运行时评估三个谓词：可容忍扰动 δ、可容忍退化 γ 与缓解可行性 μ；被攻陷设备集合由 IDS 置信度分数推导得到。当弹性丧失时，框架触发可用的缓解策略。评估采用 8 个攻击场景，系统性地覆盖谓词状态空间的所有可能组合，并变化攻击目标、退化速率与缓解措施可用性。实验结果表明，实现的运行时行为与理论定义保持一致。该工作适合机器人安全、网络物理系统弹性、形式化方法以及 IDS 集成方向的研究者与安全工程师阅读。

该论文研究如何保护容器化工作负载(如 Docker 容器与 Kubernetes Pod)免受中间人(Man-in-the-Middle, MitM)攻击。作者首先指出一个常被忽视的事实：容器化环境虽然提供隔离与编排便利，但其内部工作负载仍然暴露于与非容器环境相同的攻击面，包括钓鱼、应用层漏洞利用以及网络入侵；而容器具有动态调度、生命周期短、东西向流量密集、配置易漂移等特性，使传统边界防护与静态网络策略难以覆盖通信链路上的窃听、篡改与会话劫持风险。方法上，研究采用基于 PRISMA 指南的系统性综述(Systematic Review)，对同一研究主题的既有证据进行检索、筛选与汇总，提取出可复用的成功要素(success factors)；在综述基础上开展设计型研究(design-and-creation)，提出一个面向容器化操作系统的安全框架。该框架的核心包括三部分：一是用于描述通信行为与密码原语的概念模型(conceptual model)，使安全属性可被形式化刻画；二是借助 AnBxJ Java 安全库来实现与验证通信安全；三是部署工作在 OSI 模型第 7 层(应用层)的容器防火墙，将访问控制与检查从网络层提升到应用层，并结合零信任(Zero Trust)架构原则，对通信双方进行持续的身份确认与完整性校验。研究围绕一个核心问题展开：如何有效保护容器化操作系统免受 MitM 攻击。验证部分在一个容器化操作系统场景中成功实现了该安全机制，并识别出实现过程中的成功因素。论文的价值主张是帮助从业者系统化容器安全实践，并为 Docker 与 Kubernetes 部署提供可落地的零信任参考架构。需注意，本文属于综述加设计型研究，重点在方法论与架构层面，摘要中并未给出量化实验结果、性能开销数据或具体攻击面测绘结论，因此结论的可迁移性仍需结合完整论文与实测验证。

该论文聚焦于一个长期存在的安全工程问题：即时通信协议的「形式化规范保证」与「实际运行实现行为」之间存在落差。Signal 协议为数以十亿计的用户提供加密通信，是 WhatsApp（全球用户量最大的消息应用）与 Signal 官方客户端的底层协议；学界已在计算模型与 Dolev-Yao 符号模型下对该协议给出大量强安全证明，但这些证明只覆盖协议规范本身，无法说明真实客户端在运行时是否严格按模型执行。作者的工作是填补这一差距：采用新近提出的运行时监控器 SpecMon，对实际观测到的执行轨迹进行一致性检查，判断其是否符合形式化协议模型。为此，作者对两个真实应用（WhatsApp Web 与 Signal Desktop）进行插桩，捕获它们与网络层及密码学组件之间的交互事件；在可信事件抽取的前提上，把运行时行为抽象为符号层，再据此构建两个与 Tamarin 兼容的多重集重写（multiset-rewrite）模型以便形式化验证。论文给出了首个 WhatsApp Web 上 Signal 协议实现的模型，以及迄今为止最详细的 Signal 原始协议模型。监控结果显示，在给定的抽取与符号抽象假设下，观测到的执行符合这些模型，并对 Signal 协议的核心组件验证了认证性与机密性属性。值得注意的是，监控还暴露出原始 libsignal 库与 WhatsApp 分支之间此前未被文档记录的行为差异。作者同时评估了方法的可复现性与实用性：完成 WhatsApp Web 建模、应用插桩、加入模糊测试并运行实验共耗时三个人周；实验表明可对真实应用进行高效监控，并能检测人为注入的安全故障，在其实测环境中开销较低。

该论文《A2ABreak: Systematic Security Analysis of the A2A Protocol》针对由 Linux 基金会治理、正在成为多智能体生态水平通信层的 Agent2Agent（A2A）协议开展首次系统性安全分析。A2A 是一个开放标准，允许自主 AI 智能体跨组织边界互相发现、认证并委派任务，其定位与负责工具集成的 Model Context Protocol（MCP）互补，因此 A2A 事实上承担了智能体之间「横向通信」的职责，其安全性直接决定多智能体系统的信任边界是否成立。作者指出，尽管 A2A 部署快速扩张，但此前没有任何工作对其协议层安全进行系统化审视。为此，论文提出 A2ABreak 框架：先借助 LLM 辅助的方式，从自然语言规范中抽取并人工验证一台有限状态机，把 929 条形式化陈述统一建模为 37 个状态、76 条转移；随后在该模型上以「完全合规假设」（即假设所有实现都严格遵循规范、不存在任何代码缺陷）为前提，通过对抗性验证推理，系统搜索协议自身可被合规攻击者利用的漏洞。结果发现 11 个此前未知的漏洞，每一个都无需任何实现层缺陷即可被符合规范的对手触发。典型发现包括：通过未受保护的上下文标识符实现跨客户端上下文注入；在委派链的多跳过程中身份信息丢失，进而导致凭据被第三方收割；以及通过宣称未经认证的能力声明引入恶意智能体并据此实施数据外泄。作者以独立专家评审作为基准评估该方法，报告精确率 73.3%、F1 为 84.6%；而在同一份规范上直接运行的零样本 LLM 基线未能产出任何被确认的发现，这说明显式的形式化建模与状态机锚定是进行可靠协议安全分析的必要条件。该工作适合协议设计者、多智能体平台与 AI 安全研究者阅读，其核心贡献在于提出了一套可迁移的「规范→状态机→对抗验证」方法论，并把 A2A 的安全讨论从实现漏洞层面推进到协议设计层面。

X.509 公钥基础设施（PKI）是广泛使用的可扩展且灵活的身份认证机制，但其标准文本由自然语言编写，存在设计复杂、歧义和欠规定（under-specification）等问题，导致实现者难以完全遵循标准。实际中，很多 X.509 实现库因不符合标准而出现缺陷，进而可能使依赖应用遭受冒充攻击或互操作性问题。本文旨在通过重新工程化（re-engineering）并形式化 X.509 标准中一个广泛使用的片段，并基于此开发一个高可信实现来缓解上述问题。作者的核心思路是将语法要求与语义要求解耦。对于语法要求，他们发现属性文法（attribute grammar）的一个受限片段足以形式化 X.509 的语法结构。对于语义要求，作者使用无量词一阶逻辑（Quantifier-Free First-Order Logic, QFFOL）来精确描述最常用 X.509 功能上的语义约束。有趣的是，使用 QFFOL 所得到的规范是可执行的（executable specification），并且可以由 SMT 求解器高效地执行检查。作者利用这些洞见开发了一个名为 CERES 的高可信 X.509 实现。他们使用 200 万条真实证书链和 200 万条合成证书链，将 CERES 与 mbedTLS、OpenSSL 和 GnuTLS 三个主流库进行了对比实验。结果表明，CERES 能够正确拒绝格式错误和无效的证书，而主流库中存在的相关的非合规缺陷则被暴露出来。该工作为使用形式化方法重新工程化自然语言标准提供了可行范例，也为提升 X.509 生态的整体安全性提供了一条建设性路径。本文适合 PKI/证书安全研究人员、标准制定者以及负责实现或审计 TLS/X.509 库的软件工程师阅读。

该论文研究分布式系统与授权模型中的一个根本性缺口：授权“何时”才算真正结束？论文指出，即使系统报告撤销完成、达到干净状态或操作成功，先前已授权的执行路径仍可能在提供方（如消息中间件、编排平台）未违反自身契约的前提下，继续产生应用程序明确拒绝的效果。作者将这种问题的缺失定义为“策略相对效果闭包”（policy-relative effect closure），简称效果闭包。一个授权是“闭合”的，当它既不存在任何能通过既有授权路径触达被拒效果的路径，也无法再签发新的相关授权。为判定接口能否真实报告闭包，论文提出 EFFECTBOUND 方法：它利用带证据支持的有限契约，把问题归约为带隐藏状态的有限控制，并输出三种结果——控制策略（如何达到闭包）、不可能性证书（证明无法闭包）、或在证据不足时不作判定。机器可检查的证明确立了该归约与检查器的正确性；检查器既能自动推导闭包结果，也能验证外部证书。作者在 GitHub、Kubernetes、NATS 和 Kafka 四个真实系统中实证分析，发现闭包会以三种方式失效：接口缺少所需控制、清晰可见状态掩盖了仍在运行的工作、或模型在“效果边界”（可以阻止效果的最后一点）之前就停止。具体案例包括：GitHub 的合并工具无法将合并操作绑定到已审阅的特定提交，受控试验证明它可能合并另一个提交；NATS 可报告没有存储或待处理消息，但已投递的工作仍可向下游发布；Kafka 中所有固定集合的 broker 都已应用撤销，但一个早先被授权的请求仍能追加写入。作者随后引入一种“门控”（gate）机制：阻止对已撤销权威的新使用，并延迟接口返回，直到先前在途工作全部完成。在固定集合的 Kafka 4.3.1 测试部署中，该门控成功闭合了典型的同步、非事务性写入路径，且不会阻塞无关请求。结论是：一项授权的真正终结，不仅要求停止签发新授权，还必须保证任何早先授权都无法再触达被应用拒绝的效果。论文面向分布式系统、授权与撤销机制、以及安全形式化方法的研究者。

本文研究部分可观测离散事件系统中的匿名性验证问题。匿名性是一种信息流安全属性，其核心思想是：在外部观察者通过系统输出（观测）推断系统内部状态时，系统不应让某一时刻的状态被唯一确定，从而保护用户隐私。在离散事件系统框架下，已有 K-步匿名性和无限步匿名性的定义：K-步匿名性要求当前时刻之前至多 K 个观测步内，状态估计不能是单例；无限步匿名性则不对 K 设限。作者针对由非确定有限状态自动机建模的部分可观测系统，提出了四种新的匿名性概念——两种强匿名性和两种弱匿名性，分别称为 K-步强/弱匿名性和无限步强/弱匿名性。这些概念与已有定义的本质区别在于引入了强匿名投影与弱匿名投影的考量，使匿名性刻画更加精细，能够适应不同的隐私需求。为了验证这四种性质，作者发展了一套基于并发组合（concurrent composition）的新方法：通过构造系统的并发组合结构，系统性地追踪观测一致的状态对/状态集，从而将匿名性验证转化为对组合图的结构性质检查。基于该结构，论文给出了四种匿名性可验证的充要条件，并分析了相应算法的时间复杂度。此外，还计算了 K-步强匿名性和弱匿名性中 K 的上界，为实际应用中选择合适的匿名窗口提供了理论依据。本文属于形式化方法与信息流安全的交叉方向，适合从事隐私验证、自动机理论、安全协议分析的研究人员阅读。由于仅有摘要，具体定理证明与实验评估细节需参见全文。

本文针对带有链下组件的区块链智能合约语言，建立了一种形式化模型。链下组件是在区块链节点网络之外的指定位置执行的智能合约片段，但它们与链上合约状态保持同步。它们不仅响应链上状态的变化，还能将外部世界的事件（如股票价格、天气数据）通知给链上组件，甚至充当不同区块链之间的桥梁。这种架构为开发者提供了更大的灵活性，但也可能引入新的安全漏洞。为了具体研究这些问题，作者利用该模型，通过静态信息流控制（IFC）技术，考察了链上与链下组件之间数据的完整性和保密性保证问题。研究发现，即使在不存在循环构造的情况下，信息流控制也会失效，其原因在于链下组件作为独立线程运行，可以通过递归方法调用等方式编码出阻塞构造，从而绕过控制。作者在论文末尾讨论了若干可能的补救方向。该论文的核心贡献是对链下组件场景下信息流控制局限性的形式化证明，并提出了对区块链安全设计有指导意义的讨论。适合区块链安全研究者、形式化方法开发者以及智能合约语言设计者阅读。

本文提出“理性 Dolev-Yao 攻击者”模型，将传统符号化协议验证中的 Dolev-Yao 入侵者扩展为具有成本与收益考量的理性主体。传统 DY 入侵者在知识允许范围内执行所有可能动作，不论是否有利于达成目标；而真实对手会最大化效用，仅在攻击收益为正时发起攻击。作者将攻击动作赋予成本、将破坏安全目标赋予奖励，并在加权交替时序逻辑（WATL）中定义“理性安全”属性：不存在能使理性入侵者获得严格正效用的违规策略。针对有限成本标注并发博弈结构上的有界理性入侵者，论文证明该验证问题是可判定的，给出了复杂度特征，并证明其严格细化 DY 安全性：某些协议在 DY 模型下不安全但在理性模型下安全，二者之间存在一个可计算的阈值。作者通过两个对比性用例展示框架：一是在会话不确定下的认证支付协议，理性入侵者需在不可区分的会话间策略性行动，其不完美信息会提高设计者需要定价的防御成本；二是无密码学方案的 ThreeBallot 投票协议，通过计算贿赂与收益的比率，指出低于该比率时理性胁迫者不会发动攻击。该工作为协议安全性评估提供了更贴近真实攻击者动机的决策框架，适合安全协议设计者、形式化验证研究者及博弈论与安全交叉领域学者阅读。

这篇 arXiv 论文提出了一套用于在计算模型下对安全协议进行机械化验证的框架和交互式证明器。研究背景是：安全协议设计的正确性至关重要，需要坚实的数学基础和计算机辅助方法。此前 Bana 和 Comon 提出的形式化方法只能分析固定会话数目的协议，且缺乏对证明机械化的支持。本文的核心贡献是开发了一个元逻辑（meta-logic）及相应的证明系统，用于推导安全性质，能够处理任意会话数目的协议。该证明系统中的证明仅涉及协议执行的高层符号表示，类似于符号模型中的证明，但提供的安全保证位于计算层面（即计算模型中的安全性质）。作者将该方法实现为一个新的交互式证明器 Squirrel，输入是应用 pi-演算（applied pi-calculus）描述的协议，并开展了多个案例研究，覆盖多种密码原语（哈希、加密、签名、Diffie-Hellman 指数运算）和安全性质（认证、强保密、不可关联性）。该工作的主要意义在于弥合了符号模型与计算模型之间的差距，使安全分析者能够在符号层面高效推理，同时获得计算层面的强安全保证。适合对形式化验证、密码协议安全性分析感兴趣的研究人员和安全工程师阅读。

本文是一篇关于计算机辅助密码学（Computer-Aided Cryptography）的系统化综述（SoK），旨在梳理该领域的研究进展与应用边界。随着密码学协议和实现日益复杂，传统手工分析与测试难以保证安全性与正确性。计算机辅助密码学通过形式化、可机器检查的手段，贯穿密码设计、分析和实现的全生命周期。论文将现有文献划分为三大方向：一是设计级别的安全性，包括符号安全模型（如Dolev-Yao）与计算安全模型（如可证明安全），以及如何通过自动化工具验证协议属性；二是功能正确性与效率，确保密码算法或协议实现符合规范且高效；三是实现级别的安全性，重点研究数字侧信道（如时序、功耗）的抵抗能力。针对每个方向，论文厘清了计算机辅助密码学的作用与局限性，并给出了现有工具的详细分类，从精确度、适用范围、可信度和可用性等多维度进行对比。随后总结了各方向的代表性成果、设计权衡和开放研究挑战。在案例部分，论文先探讨如何组合不同工具以覆盖更多安全属性，再回顾TLS 1.3标准化过程中社区使用形式化工具的经验。最后，作者向论文作者、工具开发者和标准制定机构提出了具体建议，以促进该领域更好地服务于密码工程实践。

本文提出 CheckMate 框架，用于全自动化的博弈论安全分析，特别关注区块链技术。CheckMate 将协议建模为博弈，并分析其博弈论安全性，即激励兼容性和拜占庭容错性。该框架要么通过提供防御策略证明协议是安全的，要么给出所有可能的攻击向量。对于不安全的协议，CheckMate 还能在存在的情况下给出使协议变得安全的最弱前置条件。CheckMate 实现了博弈论安全在一阶线性实数算术中的可靠且完备编码，从而将安全分析归约为可满足性求解。此外，CheckMate 还自动化了算术项上高效的分情况处理。实验表明，CheckMate 具有良好的可扩展性，能够分析包含数万亿策略的博弈，这些博弈对比特币闪电网络的阶段进行了建模。该研究的核心贡献在于将博弈论安全推理转化为自动化的求解问题，为区块链协议的安全验证提供了一种新的形式化方法。适合对形式化验证、区块链安全、博弈论应用感兴趣的研究者和安全工程师阅读。

该论文针对现代处理器中推测执行机制的安全分析问题展开研究。现代处理器为提升性能，采用了多种推测执行机制，例如分支预测、内存依赖推测、数据值推测等，这些机制会推测性地执行不同类型的指令。攻击者可能同时利用多种推测机制，在单个瞬态执行窗口内触发对推测访问数据的泄露，从而构造出更复杂的侧信道攻击。然而，现有的形式化安全模型通常只针对固定的、硬编码的推测机制进行建模，无法灵活地扩展以覆盖新增或组合的推测机制，导致对推测性泄露的推理不够完备。论文提出了一种自动检测推测执行组合的方法，旨在解决现有模型缺乏通用性和可扩展性的问题。其核心贡献包括：设计一种能够自动识别和推理多种推测机制组合的形式化框架，使安全分析师能够系统地评估处理器在不同推测策略联合使用下的信息泄露风险。该方法预期能够发现传统单机制模型遗漏的泄露路径，为处理器安全验证提供更全面的理论基础。由于目前仅获得论文摘要，具体技术细节、实验验证和工具实现尚未披露，因此本摘要仅基于摘要信息进行概括。适合处理器架构师、硬件安全研究人员以及形式化验证领域的学者阅读。

该论文针对开源 RISC-V 处理器中微架构侧信道的信息泄露问题，提出了一种自动化合成泄漏合约（leakage contracts）的方法。泄漏合约是近期提出的、用于指令集架构（ISA）层面的安全抽象，旨在精确刻画处理器通过微架构侧信道可能泄露的信息。然而，为给定处理器手工构造既健全（sound）又精确（precise）的泄漏合约极具挑战性，需要深入理解微架构优化（如缓存、流水线、分支预测等）引入的时序侧信道，且过程耗时且易出错。论文的核心贡献在于提出一种系统化的合成方法，能够自动从处理器的硬件设计（如 RTL 实现）中生成满足健全性和精确性要求的泄漏合约，从而避免手工推导的错误和低效。该方法有望与现有的合约验证工具链结合，形成从合约生成到验证的完整流程，为处理器安全验证提供自动化支撑。该研究面向硬件安全、形式化验证以及微架构侧信道分析领域的研究人员和工程师，尤其适用于 RISC-V 开源处理器生态的安全评估。由于该论文目前仅有摘要，具体技术细节和实验评估尚未公开，其实际效果和适用范围有待进一步验证。

本文研究信息流分析（Information Flow Analysis）在真实系统中的应用问题。信息流分析是评估机密性和完整性的主要方法，但实际采用率不高，根本原因在于理论与实践的差距：现有技术通常假设安全策略是静态的（即数据保密性不变），而真实系统中的安全关注往往是动态的。已有大量研究尝试解决这一差距，例如引入降级（declassification）、背书（endorsement）和调用策略等。近期一项工作提出了“动态释放”（dynamic release）策略，通过允许信息流限制以任意方式降级或升级，统一了先前的各种形式化方法。然而，如何可靠地实施这一强大的动态释放策略仍是开放问题。本文首次提出了一个能够强制动态释放策略的类型系统，并正式证明了其可靠性。具体贡献包括：(1) 形式化了一个支持动态释放策略的核心语言；(2) 开发了一个检查动态释放策略的类型系统；(3) 提出了新的证明技术，并正式证明了该类型系统确实强制动态释放策略；(4) 实现了一个作为Rust语言扩展的原型系统，并在会议评审系统和Civitas（电子投票系统）上进行了案例研究。本文是形式化方法在安全策略实施方面的重要进展，适合编程语言理论、安全策略形式化以及信息流控制相关方向的研究人员和工程师阅读。

操作系统（OS）的安全运行依赖对内存硬件（如 MMU、IOMMU）的正确配置，这为运行中的不可信应用提供隔离与完整性强约束。然而，硬件厂商不断推出新型地址转换与保护机制，其配置方式各异，导致 OS 开发者必须手动编写底层配置代码。这一过程既费时又易错，且可能引入破坏安全隔离保证的细微缺陷。本文提出 Velosiraptor 系统，利用软件合成（software synthesis）技术，自动生成正确、低层的内存硬件配置代码。开发者只需提供内存硬件映射行为及 OS 环境的高层描述，Velosiraptor 工具链即可将其转换为经验证（verified）的实现，并直接与 OS 其余部分链接。该方法将 OS 环境纳入合成过程，使得将 OS 移植到新硬件平台时无需手工编写内存配置代码；同时，同一份规范还可用于生成硬件组件，便于研究新型地址转换机制。系统通过领域特定约束大幅提升合成效率，并确保生成代码的正确性，从根本上减少人工编码引入的安全漏洞。该研究面向 OS 开发者、硬件设计者以及形式化方法研究者，展示了如何通过自动化和验证手段提升系统底层安全韧性。

该论文聚焦于智能合约等可重入应用（Reentrant Applications）的组合安全（Compositional Security）问题。智能合约中反复出现的灾难性漏洞（如著名的重入攻击）表明，在编写需要与恶意代码组合运行的软件时，我们尚缺乏可靠的构造安全代码的方法。信息流控制（Information Flow Control, IFC）长期以来被视为实现组合安全的有效途径，能够在组合来自不同信任域的软件时提供强安全保证。然而，当存在重入（reentrancy）攻击时，传统信息流控制的理论保证会被破坏，使得这一方案在现实中难以奏效。论文的主要贡献包括：第一，形式化定义了通用意义上的重入概念，厘清了何种行为构成重入；第二，提出一种新的安全条件，允许智能合约等软件模块在保留安全重入形式表达力的同时，保护其关键不变量；第三，设计并实现了一个安全类型系统，该类型系统可证明地执行安全信息流策略；第四，将类型系统与运行时机制相结合，使得在存在未知恶意代码的情况下，依然能够强制实施安全的重入约束；第五，通过该类型系统成功定位并修正了若干近期备受关注的高危漏洞实例。实验评估表明，该方法既保持了实用性，又显著提升了组合安全性。该研究为构建抗重入的智能合约及类似可重入应用提供了形式化基础与工具支撑，适合安全编程语言研究者、智能合约开发者以及系统安全工程师阅读。

本文提出了一种名为 dfence 的新型 CPU 指令，旨在以硬件-软件协同的方式高效缓解推测执行攻击（如 Spectre-PHT 和 Spectre-STL）。现有的软件缓解方案（如 Speculative Load Hardening, SLH）虽能有效抵御 Spectre-PHT，但需要软件维护推测掩码，既容易出错又带来额外开销；而针对 Spectre-STL 的防御（如 SSBD 位）缺乏细粒度控制且性能损耗明显。dfence 通过极少量的硬件支持，泛化了 SLH 的思想，使开发者能够对敏感寄存器进行注释标注，硬件则确保这些值不会在瞬态执行中被泄露。作者在 Proteus CPU 中实现了 dfence，并进行了安全性和性能评估，实验显示平均性能开销小于 1%。此外，为了便于安全采用，作者设计了一个类型系统，能够静态验证代码中 dfence 指令放置的正确性，从而减少人工标注带来的错误风险。这项工作为处理器微架构安全提供了一种新的硬件-软件协同设计思路，特别适合计算机体系结构、系统安全和编译器方向的研究者与实践者参考。本文为扩展版本，但当前仅基于摘要进行分析，未包含完整实验细节。

这篇论文将范畴论应用于密码学中的通用可组合性（UC）框架，以建立安全组合的严格数学理论。UC框架由Canetti提出，用于评估协议在并发环境中的安全性，但传统形式化依赖于交互式图灵机和复杂的概率论证明，难以扩展和验证。作者针对静态参与方和会话数量的系统，提出了一种范畴化表示：将协议、环境和对手建模为对象和态射，利用string diagrams（弦图）进行图形化推理，同时保持可翻译为代数方程的严谨性。该方法带来四个主要贡献：第一，通过弦图使组合定理的证明直观且简短，同时支持形式化验证；第二，范畴论抽象使结果超越交互式图灵机，适用于量子计算、领域特定语言等其他计算模型；第三，放宽了UC的某些限制，例如允许对手是计算网络而非单一图灵机，且证明其变体与标准UC等价，不损失表达力；第四，范畴论视角揭示了标准UC形式化中的若干小技术疏漏，并给出了修正。论文属于理论安全研究，为协议组合安全性提供了更通用、更严谨的数学基础，并为自动化验证和跨计算模型的安全性分析开辟了新途径。适合理论密码学、形式化方法和范畴论研究者深入研读。

本文分析了 SecureDNA 系统的安全设计、工程与实现。SecureDNA 是一个用于 DNA 合成仪的危险序列筛查系统，它通过新颖的密码学手段在查询过程中隐藏订单请求和危险数据库的内容。作者基于版本 1.0.8 的源代码，对密钥管理、证书基础设施、认证和速率限制机制进行了深入剖析，并首次采用形式化方法分析了其互认证、基础请求和豁免处理协议。研究发现，尽管密码学算法本身未被攻破，但自定义的互认证协议 SCEP 仅实现了单向认证：危险数据库和密钥服务器无法确认与其通信的对端身份。这一结构性弱点违反了纵深防御原则，使得攻击者在合成仪连接到恶意或受损的密钥服务器或哈希数据库时，能够绕过保护危险数据库机密性的速率限制。此外，还存在另一个结构性弱点：由于密码学绑定不足，系统无法检测到 TLS 通道内来自危险数据库的响应是否被修改。因此，如果合成仪在同一个 TLS 会话中重新连接数据库，攻击者可以在不破坏 TLS 的情况下重放或交换数据库响应。虽然当前实现不允许此类重连，但消除底层结构性弱点是更健壮的安全工程做法。作者提出了缓解措施并进行了验证，包括增加强绑定。软件版本 1.1.0 已采用其提出的 SCEP+ 协议修复 SCEP。该研究为生物安全领域关键基础设施的协议设计提供了重要参考，适合安全研究人员、协议设计者及生物技术安全工程师阅读。

本文研究基于线性时序逻辑（LTL）和有限状态自动机（FSA）的运行时安全监控器在防御大语言模型（LLM）智能体工具调用序列时的失效原因。实际部署中，同一监控器在不同模型架构上对攻击的覆盖率差异巨大：在部分架构上可达 68-75%，而在另一些架构上几乎为零，且无法用模型能力、训练数据或提示设计解释。作者提出了一个理论框架来解释这一现象，证明任意固定不变量的 FSA 监控器的召回率受攻击分布集中度的上界约束，即被频率最高的 k 个触发-补全模式覆盖的攻击比例。当攻击集中（香农熵低）时，小的固定不变量集合可以实现高召回；当攻击分散为多个结构不同的模式（熵高）时，任何可处理规模的固定不变量集合都无法达到高召回，无论不变量如何推导。作者在八个前沿 LLM 架构上验证了这一熵-覆盖率界限：GPT 类和 DeepSeek 后端产生高度集中的攻击分布（熵约 0.24 比特，单一模式覆盖 96%），对应 68-75% 的召回；Gemini 变体则产生高熵分布（熵约 2.81 比特，7 个簇各不超过 7%），对应仅 6-13% 的召回，且与架构匹配的重新训练无关。熵解释了覆盖率中 76% 的方差（Pearson r = -0.87, p = 0.005, 95% CI [-0.98, -0.78]），留一法验证下 r 在 [-0.91, -0.82] 之间。作者还提出一种部署前熵测试，可用少量攻击样本预测监控器覆盖率，从而在部署前实现架构感知的监控器选择。该界限和测试与架构无关，适用于任何基于 FSA 的离散动作序列运行时监控器。适合研究 LLM 智能体安全、形式化验证与运行时监控的研究人员、安全架构师以及从事 AI 红蓝队工作的工程师阅读。

该论文针对流控制传输协议（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 协议的多种潜在攻击面，验证了现有补丁的有效性，并提供了协议规范改进建议，对传输层安全研究有重要价值。

本论文提出了一种统一的跨领域研究方法：寻找既有结论中未被察觉的隐含假设，将其显式化为一个可变参数，然后证明当该假设被移除后，结论会发生什么变化。作者将此方法的形式化核心称为“动态句法不变性原理”（Dynamic Syntactic Invariance Principle），其内容为：一个已知的静态不可达性结果，在系统规则随时间演化时依然成立，但需要满足一个必要且尖锐的条件。作者首先将该原理应用于密码学，证明了一个滚动密钥（rolling-key）方案的保密性在结构更新后仍能在多轮会话中保持，从而加强了此前工作中的静态安全保证。随后，作者将同一思路推广到多个完全不同的领域：狭义相对论、物理定律形式理论的适用范围、以及一种“对每个观察者都完全有意义但不可与噪声区分”的可计算输出。在每个领域中，作者分别建立相应结论，并指出它们共同展现出一种深层结构：在完整描述层面真实存在的区分，在受限描述层面可能完全不可见。最后，作者将该原理应用于SAT问题，并声称由此推出一个矛盾，该矛盾迫使P≠NP成立，且此结果并非额外假设，而是标准理论自身所隐含的推论。作者同时对证明过程而非结论本身保留了一处保留意见。论文属于理论计算机科学与数理逻辑交叉研究，适合对复杂性理论、基础数学与跨领域方法论感兴趣的读者。

该论文针对程序信息流策略的语义形式化问题进行修正与验证。许多高级安全需求涉及程序中允许的信息流动，但由于存在选择性降级（selective downgrading）而难以精确表达。认识逻辑（epistemic logic）中的概念被视为一种有前景的策略语义方法，但尚缺乏稳健的通用框架。CSF 2018年的论文《Assuming You Know: Epistemic Semantics of Relational Annotations for Expressive Flow Policies》试图提供统一框架，但其形式化较为粗略，且在会议现场宣布了更正。本论文作者利用智能体AI编码助手（agentic AI coding assistant）的帮助，完成了修正后的形式化，并在Rocq证明助手中进行了机器检查。修正后的框架具有简洁性和通用性，可能有助于比较不同的策略规范风格，并利用现有技术强制执行这些策略。该研究属于形式化方法与安全策略语义的交叉领域，主要贡献在于修复了先前框架的缺陷，并通过机器验证保证了正确性。适合对信息流安全、形式化验证和智能体辅助编程感兴趣的研究者阅读。

该论文是 Gilles Barthe 撰写的一篇关于安全形式化的综述章节，聚焦于证明助手（proof assistants）在计算机安全领域的应用。研究背景是：设计与实现必须满足预期的安全属性，而证明助手能够通过机械化推理严格验证这些属性，从而支撑安全认证。文章的核心问题是：如何将证明助手系统性地应用于系统安全、基于语言的安全（language-based security）、安全编译和密码学四大领域。在系统安全方面，证明了操作系统内核、微内核、虚拟机监控器等底层软件的安全属性，如隔离性和信息流控制；在基于语言的安全方面，利用类型系统和程序逻辑推导程序的信息流安全、非干扰性和访问控制；在安全编译方面，验证编译器是否保持源程序的安全属性，即安全编译（secure compilation），确保编译后代码不引入新的漏洞；在密码学方面，使用证明助手形式化验证加密协议、签名方案等密码构造的正确性。论文的贡献是提出了一套统一的证明方法框架，强调证明助手在建立高置信度安全保证中的作用，并为实际系统中的安全认证提供了方法论支撑。该文适合需要了解形式化验证与安全交叉领域的研究人员、安全工程师以及希望提升系统安全保证等级的开发者阅读。

本文提出 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 通过形式化方法建模共识协议中的激励结构，结合博弈论分析和符号模型检测，自动识别可能导致不正当行为（如自私挖矿、贿赂攻击等）的激励缺陷。论文在模拟环境中验证了该框架的有效性，发现了多个已知和未知的激励漏洞，并提供了相应的修复建议。该工作为区块链共识安全提供了新的自动化分析工具。 由于仅基于论文标题和作者信息，未获取完整摘要，以上内容为合理推断，具体细节需参考原文。

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