This page in English
SucheInfoZert B
Spezifikation und Verifikation von Informationsflüssen
| Projektstart: | 01.08.2006 |
| Projektende: | 30.09.2008 |
| Laufzeit: | Zwei Jahre |
| Projektträger: | DFG (Deutsche Forschungsgemeinschaft) |
| Projektverantwortung vor Ort: | Prof. Dr. Alexander Knapp |
| Beteiligte Wissenschaftler / Kooperationen: |
Prof. Dr. Martin Hofmann |
Zusammenfassung
Spezifikation und Verifikation von Informationsflüssen
Beschreibung
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.
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.