Dynamic IFC Theorems for Free!
This work provides a simplified proof method for researchers and practitioners in programming languages and security, though it is incremental as it builds on existing parametricity concepts.
The authors tackled the problem of proving soundness for dynamic information flow control (IFC) libraries by showing that noninterference and transparency theorems can be derived directly from parametricity theorems of type abstraction, resulting in very short proofs that remain concise even when mechanized in Agda.
We show that noninterference and transparency, the key soundness theorems for dynamic IFC libraries, can be obtained "for free", as direct consequences of the more general parametricity theorem of type abstraction. This allows us to give very short soundness proofs for dynamic IFC libraries such as faceted values and LIO. Our proofs stay short even when fully mechanized for Agda implementations of the libraries in terms of type abstraction.