### Abstract

We present interpretations of type systems for secure information flow in Hoare logic, complementing previous encodings in relational program logics. We first treat the imperative language IMP, extended by a simple procedure call mechanism. For this language we consider base-line non-interference in the style of Volpano et al. and the flow-sensitive type system by Hunt and Sands. In both cases, we show how typing derivations may be used to automatically generate proofs in the program logic that certify the absence of illicit flows. We then add instructions for object creation and manipulation, and derive appropriate proof rules for base-line non-interference. As a consequence of our work, standard verification technology may be used for verifying that a concrete program satisfies the non-interference property.
The present proof development represents an update of the formalisation underlying our paper [CSF 2007] and is intended to resolve any ambiguities that may be present in the paper.

### License

BSD License

### Topics

- Computer science/Programming languages/Logics
- Computer science/Security

### Session SIFPL

- IMP
- VDM
- VS
- ContextVS
- Lattice
- HuntSands
- OBJ
- VDM_OBJ
- PBIJ
- VS_OBJ
- ContextOBJ

## Cite

×

SIFPL-AFP

    @article{SIFPL-AFP,
      author  = {Lennart Beringer and Martin Hofmann},
      title   = {Secure information flow and program logics},
      journal = {Archive of Formal Proofs},
      month   = {November},
      year    = {2008},
      note    = {\url{https://isa-afp.org/entries/SIFPL.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
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1
- Feb 16, 2013 : Isabelle2013
- May 24, 2012 : Isabelle2012
- Oct 11, 2011 : Isabelle2011-1
- Feb 11, 2011 : Isabelle2011
- Jul 1, 2010 : Isabelle2009-2
- Dec 12, 2009 : Isabelle2009-1
- Apr 29, 2009 : Isabelle2009
- Nov 13, 2008 : Isabelle2008