Mechanized Logical Relations for Termination-Insensitive Noninterference

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.