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

Full description

Saved in:
Bibliographic Details
Main Authors: Beringer, L., Hofmann, M.
Format: Conference Proceeding
Language:English
Subjects:
Automatic logic units
Collaboration
Computer networks
Computer security
Concrete
Data security
Encoding
Impedance
Information security
Large-scale systems
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:1063-6900
2377-5459
DOI:10.1109/CSF.2007.30