[POPL 2021] Mechanized Logical Relations for Termination-Insensitive Noninterference (full)

Simon Oddershede Gregersen (Aarhus University)
Johan Bay (Aarhus University)
Simon Gregersen (Aarhus University)
Lars Birkedal (Aarhus University)
Amin Timany (Aarhus University)

We present an expressive information-flow control type system with recursive types, existential types, label polymorphism, and impredicative type polymorphism for a higher-order programming language with higher-order state. We give a novel semantic model of this type system and show that well-typed programs satisfy termination-insensitive noninterference. Our semantic approach supports compositional integration of syntactically well-typed and syntactically ill-typed—but semantically sound—components, which we demonstrate through several interesting examples. We define our model using logical relations on top of the Iris program logic framework. To capture termination-insensitivity, we develop a novel re-usable theory of Modal Weakest Preconditions. We formalize all of our theory and examples on top of the Iris program logic framework in the Coq proof assistant.