Towards Guaranteeing Information Flow Properties by Architectural Design


For ensuring that no secrets are leaked by a system, it is crucial to 
control the information flow caused by using the system. A possible way 
to do so is to formalize and verify desired information flow properties 
for a system of concern; an often extensive and expensive task. To aid 
the verification process, one could take advantage of the system's 
architecture and obtain certain information flow guarantees by design.
This motivates to identify and formalize the information flow 
guarantees induced by a system's architecture in the Modular Assembly 
Kit for Security Properties (MAKS).

MAKS as a framework provides the necessary means to express complex 
information flow properties as conjunction of simpler information flow 
properties, so called Basic Security Predicates (BSPs).

In this talk we present several extensions to the MAKS framework. 
In particular, we present the BSPs "Left Move" and "Right Move" and 
their relationship to the classical BSPs. Thereby, we consolidate 
unpublished work by Mantel and Sprick. Moreover, we present the novel 
BSP "Replacement by Compatible and Admissible Sequences of Events". 
These extensions serve as foundation to formalize the information flow 
guarantees induced by several specialized and classes of architectures 
in the remainder of the thesis.