Title:
Towards Guaranteeing Information Flow Properties by Architectural Design

Abstract:
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; 
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 derive a formal 
model of architectures and to investigate the information flow properties 
induced by instances of this model.
	
In this talk we briefly recap extensions to the Modular Assembly Kit of 
Security Properties (MAKS) that we have presented in the intermediate 
talk of this thesis. Moreover, we present a formal model of architectures 
that focuses on architectural properties relevant for information flow.
Based upon the presented extensions to MAKS, we present sound information 
flow guarantees for arbitrary instances of this model of architectures.

Following the results of the thesis we take a closer look on the current 
state of MAKS and give an overview of our plans for the future.