An Isabelle/HOL formalization of Strong Security

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 [2] formalizes noninterference for concurrent systems. We present an Isabelle/HOL formalization of strong security for arbitrary security lattices ([2] uses a two-element security lattice). 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 ex-pressions. It can easily be instantiated with different syntactic approx-imations for these side conditions. The soundness proof of such an instantiation boils down to showing that these syntactic approxima