Compositionality of Information Flow Security with Assumptions and 
Guarantees in Isabelle/HOL


Compositionality is an important attribute of information flow 
properties in practice. Since information flow properties are becoming 
more complex to increase precision, proofs about compositionality are 
getting harder to check and more error-prone. To show a possible 
remedy to this, the talk presents a machine-checked formalization of 
SIFUM-security [Mantel, Sands, Sudbrock] including the 
compositionality proof in Isabelle/HOL. This increases confidence in 
the results and shows that proof assistants are sufficiently advanced 
to handle such topics with only minor overhead. The presentation will 
focus on how to model the definitions in Isabelle/HOL and how the 
compositionality proof is structured.