Demystifying Information Flow Downgrading using the Real--Ideal Paradigm

Abstract

The real--ideal paradigm, an approach to security specification developed in the cryptography community, has the benefit that it can express sophisticated confidentiality and integrity requirements, even for decentralized systems. We show that this paradigm is the basis for a powerful and intuitive new semantic framework for language-based security. Our new framework cleanly and extensionally captures existing security definitions, including not only noninterference but also less understood information flow properties that involve downgrading, such as robust declassification and nonmalleable information flow. Past semantics for these properties have relied on intensional downgrading events. Further, we show that all of these properties can be enforced by a practical information-flow type system for a while-language that supports downgrading. Surprisingly, correctness of this type system is also characterized as a real--ideal simulation, with an important implication: the security of heterogeneous, decentralized systems with a strong (real) attacker can be understood by reasoning about a weak (ideal) attacker whose power is restricted to interaction with downgrading. This result explains the usefulness of nonmalleable information flow and related security properties. The results are fully formalized using the Rocq prover and are publicly available.