Diese Seite auf deutsch
SearchInfoZert B
Spezifikation und Verifikation von Informationsflüssen
| Start date: | 01.08.2006 |
| End date: | 30.09.2008 |
| Duration: | Two years |
| Funded by: | DFG (Deutsche Forschungsgemeinschaft) |
| Local project leader: | Prof. Dr. Alexander Knapp |
| External scientists / cooperations: |
Prof. Dr. Martin Hofmann |
Abstract
Spezifikation und Verifikation von Informationsflüssen
Description
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.