[isabelle] New AFP entry: Secure information flow and program logics

Secure Information Flow and Program Logics
Lennart Beringer and Martin Hofmann

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.

This 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.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.