Security Reasoning via Substructural Dependency Tracking
Author
Abstract

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.

Year of Publication
2026
Journal
Proceedings of the ACM on Programming Languages
Volume
10
Issue
POPL
Number of Pages
29
Date Published
01/2026
URL
https://dl.acm.org/doi/10.1145/3776669
DOI
10.1145/3776669
Google Scholar | BibTeX | DOI