本论文针对云平台 IoT 访问控制策略中的信息流安全问题展开研究。在物联网环境中，设备可能具有不同的信任级别或被划分到不同子系统，仅孤立地验证单项权限是否允许不足以发现跨设备间的非预期信息流动。作者以 AWS IoT Core 为具体对象，对其组件进行了形式化建模，并定义了一种信息流图（information flow graph），用于刻画访问控制策略所允许的设备间通信。通过利用 SMT 求解器构建该图的有限表示，研究者能够对设备之间的信息流进行可判定的验证，从而识别潜在的安全漏洞。作者将该方法实现为名为 IOT:POKER 的工具，并在一个真实场景及多条真实世界策略上进行了评估。论文的主要贡献包括：形式化建模 AWS IoT Core 的访问控制组件、提出基于信息流图的安全性质验证方法、将 SMT 求解用于解决图的无限状态问题，以及实现和实验验证所提方案的有效性。该研究适合云安全研究人员、IoT 平台开发者和安全审计人员阅读，有助于在配置阶段发现由访问控制策略不当引发的跨设备信息泄露风险。

该论文探讨了程序安全中非干扰属性（non-interference）与信息降级（downgrading）之间的经典矛盾。非干扰是机密性和完整性的最高安全保证，但严格的非干扰会阻止大多数实际程序完成其功能，因为它们需要泄露或修改信息。传统方法将类型系统按机密性和完整性分为两条独立路径，带来重复的推理机制和复杂的规范。此外，降级机制往往打破抽象边界，损害模块化推理。作者引入参数化信息流（parametric information flow），基于模态类型理论的最新进展，特别是开放模态（open modality）和封闭模态（closed modality）的丰富交互。关键洞察是：这两种模态的联合作用足以重构全谱信息流推理，形成统一框架同时处理机密性和完整性。该框架在不扩展理论的前提下，恢复了降级机制以及鲁棒去分类（robust declassification）等高级推理工具的类似物，加强了先前的结果。通过二元逻辑关系参数证明非干扰，将鲁棒性实现为由模态中介的普通2-超性质。工作表明，先进的降级机制与抽象、模块化的机制完全兼容，并且后者在完全强度的非干扰下自然产生。适合对类型系统、信息流控制、程序验证和语言安全感兴趣的研究人员阅读。

本文提出了一种基于类型系统的安全信息流分析方法，用于处理动态可扩展安全格（security lattice）。该方法扩展了Kobayashi基于类型的π-演算安全信息流分析，π-演算是一种支持顺序和并发计算的表达性模型，具有简洁的语法、基于归约的语义和双模拟等价作为机密性的鲁棒形式化（非干涉性）。核心贡献在于允许在系统执行过程中动态创建新的安全级别并将其插入安全格中，而原始系统仅考虑简单的二元格（仅包含High和Low）。文章详细处理了格本身的扩展，并进行了刻意推广。实验部分通过形式化证明验证了该类型系统的正确性，确保信息流安全。适合对并发系统信息流安全、类型系统、π-演算感兴趣的研究人员阅读。

该论文针对持久内存（Persistent Memory）这一新兴内存范式中的信息流安全（information flow security）问题展开研究。持久内存能够提升运行时效率并支持程序在断电或系统崩溃后恢复，但现有研究多聚焦于功能正确性验证，而信息流安全这一正交概念尚未得到充分探索。论文提出了一种面向无结构语言（即使用goto而非循环）的信息流逻辑，该语言模拟了简单的汇编语言。作者将该逻辑应用于x86汇编，并引入“重排序干扰自由（reordering interference freedom, rif）”的概念，以推理指令在乱序传播到内存时的潜在信息泄露。进一步地，论文展示了相同的rif概念可以用于推理持久内存上的信息流安全。实验部分（如有）未在摘要中详细说明，但该工作为持久内存系统的安全分析提供了理论基础。适合对持久内存、信息流安全、形式化方法感兴趣的研究人员阅读。

本文针对硬件信息流（information-flow）的形式化验证中可扩展性不足的问题，提出了一种名为“受保护等价谓词”（Guarded Equivalence Predicates）的方法。在硬件安全验证中，自组合（self-composition）技术将信息流验证转化为两个电路副本之间的安全性质检查，产生的关系性证明义务对通用的属性推演引擎（PDR）而言难以仅从位级逻辑中发现。最近基于PDR的技术利用副本对称性和全局跨副本等价谓词来利用这种重复结构，但当对应内部信号在整个可达状态空间中都不一致时，这些谓词效果有限，且无法捕获仅在特定控制上下文中相关的等式。作者观察到，在硬件信息流验证中，上下文相关关系自然存在：内部信号对可能只需在某个控制阶段、事务窗口、循环状态或协议区域内保持一致。为此，本文引入了受保护等价谓词，将该类关系暴露给PDR。与将提议的上下文等式作为假设不同，验证器将相应的失配条件作为辅助阻塞义务提交。保护条件是从关系性反例归纳（CTI）中通过CTI局部提取和状态分裂搜索提取的；只有后端证明不可达的候选者才会影响证明过程。在12个信息流验证基准测试和两个PDR后端的实验中，受保护谓词将两个上下文相关的基准超时转化为在1800秒时限内34.2-89.5秒内完成的证明，并在其他基准上将证明时间最多减少10.8倍。该方法为硬件安全验证提供了一种系统性的可扩展策略，尤其适用于需要检查不同运行轨迹下数据流一致性的复杂控制逻辑。

本文针对本地差分隐私（LDP）协议缺乏系统化比较方法的问题，提出了基于定量信息流（QIF）的分析框架。当前LDP领域通常使用隐私预算ε作为隐私度量，但ε仅能约束最坏情况下的区分性；其他比较则依赖效用驱动分析，即针对给定隐私预算ε评估机制保留数据效用的能力。这两种方法都无法全面评估协议面对不同攻击者模型时的安全性。本文通过将LDP机制建模为概率信道，利用细化（Blackwell序）概念建立更原则化的分类，从而判断一个协议是否在所有可能的攻击者面前本质上优于另一个协议，并讨论其对效用分析的影响。具体地，作者对七种主流协议进行了形式化QIF分析，包括广义随机响应（GRR）、局部哈希变体（BLH、OLH）、一元编码方案（SUE、OUE）以及直方图编码阈值化（THE）。分析发现，一些先前被认为“最优”的协议实际上与其他协议不可比或被严格主导。该工作弥合了LDP与形式化方法社区之间的鸿沟，实现了对本地隐私系统的原则化、攻击者感知推理。

本文提出了一种名为“基于语言的智能体控制”（LBAC）的新型编程模型，旨在解决智能体应用中的安全控制问题。传统的编程语言中，静态类型和运行时强制执行已被用于确保程序满足用户指定的策略（如访问控制、信息流、数据来源等）。LBAC的核心思想是将这些保证扩展到智能体应用：要求智能体生成的程序本身在周围脚手架代码的上下文中是良好类型的。不安全的程序在执行前会被类型检查器拒绝，从而允许策略统一应用于整个应用程序，包括智能体生成的行为和开发者编写的脚手架。同时，LBAC保留了相当大的表达能力：智能体可以执行任意的无副作用计算，并递归调用子智能体，这些子智能体在相同或更严格的策略下保留完整的工具访问权限。本文通过三个案例研究展示了LBAC：基于文件系统能力的I/O沙箱、数据来源和信息流控制。该工作为智能体安全提供了新的形式化方法，适合编程语言和安全领域的研究者阅读。

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