### Abstract

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.

### License

BSD License

### Topics

- Computer science/Security
- Computer science/Programming languages/Type systems

### Session SIFUM_Type_Systems

- Preliminaries
- Security
- Compositionality
- Language
- TypeSystem
- LocallySoundModeUse

## Cite

×

SIFUM_Type_Systems-AFP

    @article{SIFUM_Type_Systems-AFP,
      author  = {Sylvia Grewe and Heiko Mantel and Daniel Schoepe},
      title   = {A Formalization of Assumptions and Guarantees for Compositional Noninterference},
      journal = {Archive of Formal Proofs},
      month   = {April},
      year    = {2014},
      note    = {\url{https://isa-afp.org/entries/SIFUM_Type_Systems.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Apr 25, 2014 : Isabelle2013-2
- Apr 24, 2014 : Isabelle2013-2