An Isabelle/HOL Formalization of the Modular Assembly Kit for Security Properties

Oliver Bračevac 📧, Richard Gay 📧, Sylvia Grewe 📧, Heiko Mantel 📧, Henning Sudbrock 📧 and Markus Tasch 📧

May 7, 2018

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


The "Modular Assembly Kit for Security Properties" (MAKS) is a framework for both the definition and verification of possibilistic information-flow security properties at the specification-level. MAKS supports the uniform representation of a wide range of possibilistic information-flow properties and provides support for the verification of such properties via unwinding results and compositionality results. We provide a formalization of this framework in Isabelle/HOL.


BSD License


Session Modular_Assembly_Kit_Security