一句话：提出基于输出约束的子结构类型框架，统一刻画能力、定量信息泄漏、沙箱与授权协议等安全特性，并以单一逻辑关系证明其安全性。
子结构类型系统通常通过限制计算输入的使用来对资源（如内存）建模，但能力、定量信息泄漏、seccomp 式沙箱、授权协议等安全特性此前多在安全文献中分散研究。本文提出一种以约束计算输出为核心的新型资源推理，构建统一框架，将上述特性分别视为该框架的不同片段，并把它与传统的基于输入的资源推理相联系，解释为对子结构逻辑构造性 Kripke 语义的内部处理。作者用单一的逻辑关系论证同时验证了系统的能力安全、定量安全与协议安全，为安全推理的通用工具迈出第一步。
Substructural type systems provide the ability to speak about resources . By enforcing usage restrictions on inputs to computations they allow programmers to reify limited system units–such as memory–in types. We demonstrate a new form of resource reasoning founded on constraining outputs and explore its utility for practical programming. In particular, we identify a number of disparate programming features explored largely in the security literature as various fragments of our unified framework. These encompass capabilities, quantitative information leakage, sandboxing in the style of the Linux seccomp interface, authorization protocols, and more. We furthermore explore its connection to conventional input-based resource reasoning, casting it as an internal treatment of the constructive Kripke semantics of substructural logics. We verify the capability, quantity, and protocol safety of our system through a single logical relations argument. In doing so, we take the first steps towards obtaining the ultimate multitool for security reasoning.
@article{GouniPA26,
title = {Security Reasoning via Substructural Dependency Tracking},
author = {Hemant Gouni and Frank Pfenning and Jonathan Aldrich},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776669}
}