Links und Funktionen

You are here: Home / Publikationen / Secure information flow and program logics


Lennart Beringer and Martin Hofmann (2007)

Secure information flow and program logics

In: 20th IEEE Computer Security Foundations Symposium, CSF 2007, 6-8 July 2007, Venice, Italy, pp. 233-248, IEEE Computer Society.

We present interpretations of type systems for secure information flow in Hoare logic, complementing previous encodings in binary (e.g. relational) program logics. Treating base-line non-interference, multi-level security and flow sensitivity for a while language, we show how typing derivations may be used to automatically generate proofs in the program logic that certify the absence of illicit flows. In addition, we present proof rules for baseline non-interference for object-manipulating instructions, As a consequence, standard verification technology may be used for verifying that a concrete program satisfies the noninterference property. Our development is based on a formalisation of the encodings in Isabelle/HOL.

Document Actions