现代软件系统通常由多种编程语言混合构建（如 Python 与 C、Java 与 C 的交互），这种跨语言架构会因语言间的语义差异和隐式交互引入难以察觉的漏洞。传统静态分析器受限于不同语言语义的异构性，往往无法有效建模跨语言的数据流；动态分析方法则受限于测试输入的覆盖率，难以发现深层或隐晦的缺陷。针对这一空白，论文提出 PolyFlow——一个神经符号（neuro-symbolic）框架，将大语言模型（LLM）与静态分析协同结合，用于跨语言信息流（数据流）的静态推理。其核心思路是：首先基于给定多语言系统的控制流表示，利用 LLM 识别由复杂语言特性（如指针别名、回调、异常路径、隐式类型转换等）造成的隐式流事实，从而增强基础程序表示；随后在增强后的表示上传播数据流，实现跨语言边界的信息流分析。为克服 LLM 固有的 token 限制、幻觉等问题，PolyFlow 采用静态分析指导的作用域裁剪、上下文管理和逐条事实校验，并引入多 LLM 专家小组进行协商式验证，提高结果的可靠性。作者在真实世界的 Python-C 和 Java-C 混合系统上开展实验，结果表明 PolyFlow 在成本效益上具有优势，且优于多种现有基线（包括纯静态分析、纯 LLM 方法以及动态测试），并成功发现了所有基线均遗漏的未知跨语言漏洞。该研究的主要贡献包括提出首个结合 LLM 与静态分析的跨语言信息流分析框架、设计多 LLM 协商验证机制，以及在真实系统上验证其有效性和实际漏洞发现能力。适合软件安全研究人员、静态分析工具开发者以及关注多语言供应链安全的蓝队工程师阅读。

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

本文研究分离式信息流策略的强制执行问题。分离式策略允许一个值最多依赖于两个秘密之一，而不能同时依赖于两者，例如分析师只能查阅一个客户的文件而不能同时查阅两个，或者分割的秘密只能释放其中一部分。这类策略不满足格结构，Hunt和Sands提出使用信息量quantale来给出其语义，但未能解决强制执行层的实现。本文构建了该quantale所要求的流敏感类型系统家族，并揭示了关键的通用类型对象在分离场景下分裂为两个不同对象，对强制执行产生重要影响。在程序变量上的自由交换quantale上，作者证明了整个类型机制对所有策略均成立，包括单调重命名、规范推导、主类型和内部完备性。而在具有幂等生成元的自由对象上，认证的界更为精确且保持健全，因为它能正确记录同一来源的两次读取仅对应一个析取项。然而，这一精度提升无法在独立属性家族内部实现：任何支持单调重命名的标记映射都无法认证比第一个机制更精确的界，且在生成元精确同态特化下两者主类型重合。在道德墙和秘密共享标签下，对析取源的第二次读取将导致所有此类证书失效，从而拒绝本应满足策略的程序。作者还指出，直接采用格时代的通用类型对象会进一步商掉分支析取的信息。为恢复精度，他们提出将特化推迟到判断级别，由此得到的读取映射是满足健全性的最小并保持映射。该工作为分离式策略提供了首个完整的流敏感类型系统框架，并为信息流控制中的此类策略验证奠定了理论基础。

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

本文研究云环境下物联网（IoT）访问控制策略中的信息流安全问题。许多云服务商（如AWS IoT Core）提供访问控制机制，但其配置不当可能导致严重安全漏洞。作者指出，在设备具有不同信任级别或隶属于不同子系统的场景中，仅独立验证单个权限是否充足是不够的，因为恶意或受损设备可能通过合法授权路径间接向非预期设备传递数据，形成非期望的信息流。为此，该工作正式建模了AWS IoT Core的组件（包括策略、主题、设备等），并定义了一种信息流图（Information Flow Graph），用于捕获访问控制策略所允许的设备间通信关系。通过利用SMT求解器构建该图的有限表示，作者实现了对设备间信息流可达性的自动化验证，从而检测潜在的非预期信息泄露路径。作者将该方法实现为名为IOT:POKER的工具，并在一个现实场景和若干真实世界策略上进行了评估，结果表明该工具能够有效发现策略配置中的信息流漏洞。本文的贡献包括：形式化IoT访问控制策略的信息流模型、基于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沙箱、数据来源和信息流控制。该工作为智能体安全提供了新的形式化方法，适合编程语言和安全领域的研究者阅读。

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