Secure information flow and program logics

11 years 9 months ago
Secure information flow and program logics
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.
Lennart Beringer, Martin Hofmann
Added 14 Aug 2010
Updated 14 Aug 2010
Type Conference
Year 2007
Where CSFW
Authors Lennart Beringer, Martin Hofmann
Comments (0)