A Formalization of Strong Security


Title: A Formalization of Strong Security
Authors: Sylvia Grewe (grewe /at/ st /dot/ informatik /dot/ tu-darmstadt /dot/ de), Alexander Lux (lux /at/ mais /dot/ informatik /dot/ tu-darmstadt /dot/ de), Heiko Mantel (mantel /at/ mais /dot/ informatik /dot/ tu-darmstadt /dot/ de) and Jens Sauer (sauer /at/ mais /dot/ informatik /dot/ tu-darmstadt /dot/ de)
Submission date: 2014-04-23
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. Strong security from Sabelfeld and Sands formalizes noninterference for concurrent systems.

We present an Isabelle/HOL formalization of strong security for arbitrary security lattices (Sabelfeld and Sands use a two-element security lattice in the original publication). The formalization includes compositionality proofs for strong security and a soundness proof for a security type system that checks strong security 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.

  author  = {Sylvia Grewe and Alexander Lux and Heiko Mantel and Jens Sauer},
  title   = {A Formalization of Strong Security},
  journal = {Archive of Formal Proofs},
  month   = apr,
  year    = 2014,
  note    = {\url{https://isa-afp.org/entries/Strong_Security.html},
            Formal proof development},
  ISSN    = {2150-914x},
License: BSD License
Used by: WHATandWHERE_Security
Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.