Information flow properties provide a very elegant approach to specify security requirements formally. Confidentiality as well as integrity requirements can be expressed as restrictions on the information flow within a system. In this process, one first distinguishes different security domains and then defines whether information may flow between individual domains or not. In order to verify the resulting restrictions, it is necessary to define formally what information flow means.
In this talk, I will present some recent results on information flow control. In particular, I will present a framework for the uniform and modular representation of information flow properties, local verification conditions for proving these properties, and correctness as well as completeness results.
Heiko Mantel is a researcher at the German Research Center for Artificial Intelligence, Saarbruecken. Heiko has studied at the University of Darmstadt and the University of Colorado at Boulder. Currently he is pursuing a PhD at the University of the Saarland. His research interests include formal methods, security and automated deduction.