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.

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: