A Formalization of Assumptions and Guarantees for Compositional Noninterference

Sylvia Grewe 📧, Heiko Mantel 📧 and Daniel Schoepe 📧

April 23, 2014

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


Research in information-flow security aims at developing methods to identify undesired information leaks within programs from private (high) sources to public (low) sinks. For a concurrent system, it is desirable to have compositional analysis methods that allow for analyzing each thread independently and that nevertheless guarantee that the parallel composition of successfully analyzed threads satisfies a global security guarantee. However, such a compositional analysis should not be overly pessimistic about what an environment might do with shared resources. Otherwise, the analysis will reject many intuitively secure programs.

The paper "Assumptions and Guarantees for Compositional Noninterference" by Mantel et. al. presents one solution for this problem: an approach for compositionally reasoning about non-interference in concurrent programs via rely-guarantee-style reasoning. We present an Isabelle/HOL formalization of the concepts and proofs of this approach.


BSD License


Session SIFUM_Type_Systems