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

该论文提出了一种名为Owl的新框架，用于安全协议的组合验证。现有的计算安全协议验证工具要么缺乏模块化，要么缺乏自动化。Owl通过新颖地使用信息流类型和细化类型来实现加密安全的证明。该框架允许对安全协议进行基于类型的模块化描述，其中不相交的子协议可以被独立编程并通过自动化类型检查自动证明安全。作者为Owl提供了形式化的安全证明，基于一个核心语言，该语言支持对称和非对称密码原语、Diffie-Hellman操作以及通过随机预言机进行哈希。他们还实现了Owl的类型检查器，以及一个将协议提取到Rust的原型机制，并在14个案例研究上进行了评估，包括简化版的SSH密钥交换和Kerberos。实验结果表明，Owl能够有效地验证真实世界协议的简化版本，同时提供模块化和自动化。

该论文以PHP语言中的类型体系为研究对象，通过挖掘特定API（如extract函数）的潜在陷阱，系统分析了PHP类型系统在使用类似extract这类函数时可能引发的安全漏洞。作者通过构造一系列案例，展示了攻击者如何利用类型混淆与变量覆盖机制绕过输入过滤，最终实现代码注入与权限提升。实验量化评估了该漏洞在主流PHP框架中的影响范围，并提出了基于静态分析与运行时检查的缓解方案。本工作对PHP开发者与安全研究人员具有重要的参考价值。

本文提出了一种基于类型系统的方法来推导程序暴露的抽象“怪异机器”（weird machines）。背景是：广泛使用的关键软件系统中存在潜伏漏洞，攻击者可触发并级联这些漏洞，使程序行为异常，形成可被利用的编程模型。作者创新性地设计了一种信息流类型系统，通过追踪信息流类型来检测漏洞，并抽象漏洞间的控制流以捕获怪异机器。形式化证明表明，推导出的怪异机器能够覆盖程序可能表现出的所有怪异运行时行为。进一步，攻击模式往往简单且重复，因此可以将抽象机器建模为漏洞类型的正则表达式，这种表示与平台无关，可作为攻击的统一描述语言。最后，基于正则表达式的语言包含性等决策比针对具体程序或其他形式语言的决策高效得多。本文主要贡献在于：提供了一种自动化推导程序内部攻击能力（即怪异机器）的框架，并给出了平台无关的攻击描述方法。适合安全研究人员、编译器开发者及系统安全工程师阅读。

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