An Isabelle/HOL Formalization of Assumptions and Guarantees for Compositional Noninterference

Authors: Sylvia Grewe, Heiko Mantel, Daniel Schoepe

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. [1] 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.

The formalization includes the following parts:

  • Notion of SIFUM-security and preliminary concepts: Preliminaries.thy, Security.thy
  • Compositionality proof: Compositionality.thy
  • Example language: Language.thy
  • Type system for ensuring SIFUM-security and soundness proof: TypeSystem.thy
  • Type system for ensuring sound use of modes and soundness proof: LocallySoundUseOfModes.thy

You can download the complete Isabelle/HOL formalization here (SIFUM-Type-Systems.tar.gz).
You can browse the HTML version of the Isabelle/HOL theory files here.

This work has also been accepted in the Isabelle/HOL Archive of Formal Proofs:


[1] Assumptions and Guarantees for Compositional Noninterference, H. Mantel, D. Sands, and H. Sudbrock, In Proceedings of the 24th IEEE Computer Security Foundations Symposium (CSF), 2011.

A A A | Print | Imprint | Sitemap | Contact
zum Seitenanfang