本文针对可信执行环境（TEE）与低层语言（如 LLVM IR）结合时面临的安全分区问题展开研究。TEE 通过 enclave 提供硬件级隔离，但仅依靠它无法保证信息流安全；LLVM 这类语言允许不受限制的指针操作和非结构化控制流，进一步加剧了信息泄漏风险。同时，手工将应用划分成 enclave 部件与非 enclave 部件既繁琐又易错，且缺乏细粒度控制。作者提出一种三步走方案：首先形式化基于 LLVM IR 的 enclave 无关演算 SIR，设计新型宽松类型系统，结合信息流控制与安全感知的粗粒度内存安全，以抵御低级攻击者；然后将 SIR 扩展为 enclave 感知演算 SIREN，其非干涉性保证能抵御可观察任意非 enclave 内存的更强攻击者；最后实现类型驱动、类型保持的 SIR 到 SIREN 编译，自动生成安全的 enclave 感知程序，消除了手工分区过程，同时保持对 host-enclave 边界的细粒度控制。文中实现了 SPLITR 工具，并在 Intel SGX 硬件上用 13 个微基准和现实负载（包括 SGXGauge 应用）进行评测；SPLITR 能扩展到 OpenSSL（425,953 条 LLVM IR 指令），支持在 enclave TCB 大小、host-enclave 转换次数、边界数据移动量等目标之间权衡。对于 OpenSSL，面向转换次数优化可将其从 393 降为 187。运行时开销方面，短时运行负载主要被固定的 enclave 开销主导，而长时运行应用能更好地摊销这些开销，接近原生性能。该研究的最重要贡献是首次为 LLVM 系语言提供安全构造的自动分区形式化框架，并为编译优化、硬件隔离结合信息流控制提供了可行的工程验证。

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

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

本文提出了一种基于类型系统的安全信息流分析方法，用于处理动态可扩展安全格（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沙箱、数据来源和信息流控制。该工作为智能体安全提供了新的形式化方法，适合编程语言和安全领域的研究者阅读。