The goal of this project is the development of technology enabling the specification of information flow policies in a state-oriented manner as well as the verification of policy conformance of system implementations.

It also aims to allow for generating certificates for policy-compliant system components with little personal effort on the code producer side, which can then producer-independently and automatically be checked by any code consumer prior to code execution.

The key innovation lies in the connection of information flow analysis and independently checkable certificates for target code, as well as in developing the necessary refinement techniques.

In the end, we plan on being able to create certificates for Java bytecode derived from a UML-based modeling process.

People involved

• Lennart Beringer
• Robert Grabowski
• Martin Hofmann
• Alexander Knapp
• Florian Lasinger
• David von Oheimb

Publications

• Noninterference for Mobile Code with Dynamic Security Domains, Robert Grabowski, 2008
• Information Flow Security for Imperative Languages, Robert Grabowski, 2007
• Secure information flow and program logics, Lennart Beringer and Martin Hofmann, IEEE 2007
• An Automated Checker for DSD, Florian Lasinger and Robert Grabowski, 2008
• Quotient Automata for Non-Interference, Florian Lasinger and Alexander Knapp, 2008