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

Abstract

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.

License

BSD License

Topics

Session Modular_Assembly_Kit_Security

Cite

× 
@article{Modular_Assembly_Kit_Security-AFP,
  author  = {Oliver Bračevac and Richard Gay and Sylvia Grewe and Heiko Mantel and Henning Sudbrock and Markus Tasch},
  title   = {An Isabelle/HOL Formalization of the Modular Assembly Kit for Security Properties},
  journal = {Archive of Formal Proofs},
  month   = {May},
  year    = {2018},
  note    = {\url{https://isa-afp.org/entries/Modular_Assembly_Kit_Security.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: