Characteristics of Basic Security Predicates


The Modular Assembly Kit For Security Properties (MAKS) is a framework
for specifying security relevant information flow properties as closure
properties of sets of traces. The framework provides so called Basic
Security Predicates (BSPs) that act as basic building blocks for
specifying information flow properties. These BSPs in itself represent
simple information flow properties and can be combined to express more
advanced security properties. Applying the framework in practice shows
that the BSPs defined in MAKS' classical version are not always
sufficient to specify the required information flow properties.  Hence,
various extensions to MAKS' classical version exist but no criteria
specifying when a information flow property is considered a BSP.

In this talk we will propose different characteristics of Basic
Security Predicates and discuss their intuition as well as their design
choices. Moreover, we will exemplify the identified characteristics by
showing that a novel information flow property is indeed a BSP w.r.t.
our proposed characteristics.