Email Gateway (Aug 18 2022 at 12:37): Email Gateway (Aug 18 2022 at 12:37):From: Tobias Nipkow <nipkow@in.tum.de>
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.
http://afp.sourceforge.net/entries/SIFPL.shtml
Last updated: May 03 2024 at 12:27 UTC