← All papers
First page of The Duality of Information Flow: Reconciling Robust Downgrading with Non-Interference

The Duality of Information Flow: Reconciling Robust Downgrading with Non-Interference

Hemant Gouni, Frank Pfenning, Jonathan Aldrich

cs.PL Jul 20, 2026 · v1 cs.CR
The type system, binary logical relation, and non-interference metatheory of a parametric information-flow calculus are mechanized in Lean using intrinsically typed De Bruijn syntax.
Non-interference properties, spanning confidentiality and integrity, have long enjoyed a position as the high water mark of program security guarantees. Information flow type systems comprise the primary means for obtaining non-interference properties of programs, but their potential as a holy grail for secure programming has remained latent. Prior work bifurcates the type system along confidentiality and integrity, resulting in duplicate reasoning machinery and complex specifications. Furthermore, long-held wisdom dictates that non-interference must be weakened with downgrading mechanisms to accommodate the needs of practical programs, nearly all of which violate confidentiality and integrity in the course of fulfilling their purpose. This often pierces abstraction barriers and compromises modular reasoning. We introduce parametric information flow, which uses recent insights from modal type theory to shed light on these issues. In particular, we draw inspiration from work on the open and closed modalities, highlighting their rich interplay. Though each individual modality finds uses throughout the literature, our key insight is that their joint interaction suffices to reconstruct full-spectrum information flow reasoning, producing a single framework accounting for both confidentiality and integrity. Downgrading and analogues of advanced reasoning tools in the lineage of robust declassification are recovered without extensions to our theory, strengthening prior results. We show non-interference via a binary logical relations argument, realizing robustness as an ordinary 2-hyperproperty mediated by our modalities. Our work reveals state-of-the-art downgrading mechanisms to be wholly compatible with those for abstraction and modularity, arising precisely from the semantics of the latter under full-strength non-interference.

Information flow type systems usually treat confidentiality and integrity separately and weaken non-interference with downgrading mechanisms. This duplicates reasoning machinery and breaks modular reasoning.

The authors introduce parametric information flow, a Call-By-Push-Value calculus with open and closed modalities taken from modal type theory. The joint interaction of the two modalities yields a single framework covering both confidentiality and integrity. Non-interference is proved via a binary logical relations argument, with robustness treated as a 2-hyperproperty. The type system and metatheory are mechanized in Lean using intrinsically well-typed-and-scoped syntax.

Downgrading and analogues of robust declassification and transparent endorsement are recovered without extending the theory, while full-strength non-interference still holds. All metatheory results are mechanized in Lean, with proof scripts in the supplemental materials.