Reference. Structural Information Flow: A Fresh Look at Types for Non-interference

Information flow control is a long-studied approach for establishing non-interference properties of programs. For instance, it can be used to prove that a secret does not interfere with some computation, thereby establishing that the former does not leak through the latter. Despite their potential as a holy grail for security reasoning and their maturity within the literature, information flow type systems have seen limited adoption. In practice, information flow specifications tend to be excessively complex and can easily spiral out of control even for simple programs. Additionally, while non-interference is well-behaved in an idealized setting where information leakage never occurs, most practical programs must violate non-interference in order to fulfill their purpose. Useful information flow type systems in prior work must therefore contend with a definition of non-interference extended with declassification, which often offers weaker modular reasoning properties. We introduce structural information flow, which both illuminates and addresses these issues from a logical viewpoint. In particular, we draw on established insights from the modal logic literature to argue that information flow reasoning arises from hybrid logic, rather than conventional modal logic as previously imagined. We show with a range of examples that structural information flow specifications are straightforward to write and easy to visually parse. Uniquely in the structural setting, we demonstrate that declassification emerges not as an aberration to non-interference, but as a natural and unavoidable consequence of sufficiently general machinery for information flow. This flavor of declassification features excellent local reasoning and enables our approach to account for real-world information flow needs without compromising its theoretical elegance. Finally, we establish non-interference via a logical relations approach, showing off its simplicity in the face of the expressive power captured.

Cite

Cite as @gouni-2025-structural (helia, typst) · \cite{gouni-2025-structural} (LaTeX)
BibTeX
bibtex · 1 line
@article{gouni-2025-structural, title={Structural Information Flow: A Fresh Look at Types for Non-interference}, volume={9}, ISSN={2475-1421}, url={http://dx.doi.org/10.1145/3764116}, DOI={10.1145/3764116}, number={OOPSLA2}, journal={Proceedings of the ACM on Programming Languages}, publisher={Association for Computing Machinery (ACM)}, author={Gouni, Hemant and Pfenning, Frank and Aldrich, Jonathan}, year={2025}, month=Oct, pages={3954–3980} }
hayagriva YAML (typst)
yaml · 19 lines
gouni-2025-structural:
  type: article
  title: 'Structural Information Flow: A Fresh Look at Types for Non-interference'
  author:
  - Gouni, Hemant
  - Pfenning, Frank
  - Aldrich, Jonathan
  date: 2025-10
  page-range: 3954-3980
  url: http://dx.doi.org/10.1145/3764116
  serial-number:
    doi: 10.1145/3764116
    issn: 2475-1421
  parent:
    type: periodical
    title: Proceedings of the ACM on Programming Languages
    publisher: Association for Computing Machinery (ACM)
    issue: OOPSLA2
    volume: 9
Cited by (1)

Security Reasoning via Substructural Dependency Tracking gouni-2026-security

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.
PDF · DOI · pldb
Cites 39 works (2 here)
With notes (2)

Internalizing Indistinguishability with Dependent Types liu-2024-internalizing

In type systems with dependency tracking, programmers can assign an ordered set of levels to computations and prevent information flow from high-level computations to the low-level ones. The key notion in such systems is indistinguishability : a definition of program equivalence that takes into account the parts of the program that an observer may depend on. In this paper, we investigate the use of dependency tracking in the context of dependently-typed languages. We present the Dependent Calculus of Indistinguishability (DCOI), a system that adopts indistinguishability as the definition of equality used by the type checker. DCOI also internalizes that relation as an observer-indexed propositional equality type, so that programmers may reason about indistinguishability within the language. Our design generalizes and extends prior systems that combine dependency tracking with dependent types and is the first to support conversion and propositional equality at arbitrary observer levels. We have proven type soundness and noninterference theorems for DCOI and have developed a prototype implementation of its type checker.
PDF · DOI · pldb

A judgmental reconstruction of modal logic pfenning-2001-a

DOI
External (37)
gouni-2025-structural reference entries/refs/gouni-2025-structural/gouni-2025-structural.hel