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

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

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