The Duality of Information Flow: Reconciling Robust Downgrading with Non-Interference
2026-07-20 • Programming Languages
Programming LanguagesCryptography and Security
AI summaryⓘ
The authors address how security systems called information flow type systems guarantee that sensitive data in programs isn't leaked or tampered with. Existing methods handle confidentiality and integrity separately, creating complexity, and often need to weaken guarantees to support practical needs, which hurts modular design. They propose a new unified approach using ideas from modal type theory, combining two modalities to handle both confidentiality and integrity together. This approach also naturally supports powerful ways to safely relax security rules without breaking modular reasoning, proving strong security properties through logical arguments.
Non-interferenceInformation flow type systemsConfidentialityIntegrityDowngradingModal type theoryOpen and closed modalitiesLogical relationsRobust declassificationModularity
Authors
Hemant Gouni, Frank Pfenning, Jonathan Aldrich
Abstract
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.