From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Dear all,
I’m happy to announce a new AFP entry from TU Darmstadt.
The entry consists of a framework to specify and verify security properties.
Cheers,
René
An Isabelle/HOL Formalization of the Modular Assembly Kit for Security Properties
by Oliver Bračevac, Richard Gay, Sylvia Grewe, Heiko Mantel, Henning Sudbrock, and Markus Tasch
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.
Last updated: Nov 21 2024 at 12:39 UTC