I-MAKS - Formalizing Information-flow Properties in Isabelle/HOL


In this talk I-MAKS, an Isabelle/HOL specification of Mantel's
Modular Assembly Kit for Security Properties (MAKS), is presented.
I-MAKS supports the specification of information-flow properties
in a modular fashion using so called basic security predicates
(BSPs). I-MAKS formalizes the basic concepts of MAKS, its
compositionality results and unwinding theorems. In addition,
I-MAKS provides an additional CSP-like frontend for the
specification of systems.