### 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

- Computer science/Security

### Session Modular_Assembly_Kit_Security

- Projection
- Prefix
- EventSystems
- StateEventSystems
- Views
- FlowPolicies
- BasicSecurityPredicates
- InformationFlowProperties
- BSPTaxonomy
- PropertyLibrary
- SecureSystems
- UnwindingConditions
- AuxiliaryLemmas
- UnwindingResults
- CompositionBase
- CompositionSupport
- GeneralizedZippingLemma
- CompositionalityResults

## Cite

×

Modular_Assembly_Kit_Security-AFP

    @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:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- May 9, 2018 : Isabelle2017