Mechanized Logical Relations for Termination-Insensitive Noninterference
Journal Paper
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.
The bibtex source for this publication:
@article{DBLP:journals/pacmpl/GregersenBTB21,
author = {Simon Oddershede Gregersen and Johan Bay and Amin Timany and Lars Birkedal},
title = {Mechanized logical relations for termination-insensitive noninterference},
journal = {Proc. {ACM} Program. Lang.},
volume = {5},
number = {{POPL}},
pages = {1--29},
year = {2021},
url = {https://doi.org/10.1145/3434291},
doi = {10.1145/3434291},
timestamp = {Wed, 17 Feb 2021 08:54:05 +0100},
biburl = {https://dblp.org/rec/journals/pacmpl/GregersenBTB21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}