Abstract: |
Research in information-flow security aims at developing methods to
identify undesired information leaks within programs from private
sources to public sinks. Noninterference captures this intuition by
requiring that no information whatsoever flows from private sources
to public sinks. However, in practice this definition is often too
strict: Depending on the intuitive desired security policy, the
controlled declassification of certain private information (WHAT) at
certain points in the program (WHERE) might not result in an
undesired information leak.
We present an Isabelle/HOL formalization of such a security property
for controlled declassification, namely WHAT&WHERE-security from
"Scheduler-Independent Declassification" by Lux, Mantel, and Perner.
The formalization includes
compositionality proofs for and a soundness proof for a security
type system that checks for programs in a simple while language with
dynamic thread creation.
Our formalization of the security type system is abstract in the
language for expressions and in the semantic side conditions for
expressions. It can easily be instantiated with different syntactic
approximations for these side conditions. The soundness proof of
such an instantiation boils down to showing that these syntactic
approximations imply the semantic side conditions.
This Isabelle/HOL formalization uses theories from the entry
Strong Security. |
BibTeX: |
@article{WHATandWHERE_Security-AFP,
author = {Sylvia Grewe and Alexander Lux and Heiko Mantel and Jens Sauer},
title = {A Formalization of Declassification with WHAT-and-WHERE-Security},
journal = {Archive of Formal Proofs},
month = apr,
year = 2014,
note = {\url{http://isa-afp.org/entries/WHATandWHERE_Security.html},
Formal proof development},
ISSN = {2150-914x},
}
|