Das Ziel dieses Projektes ist die Berücksichtigung moderner Berechtigungssteuerung in Verbindung mit formalen Softwareentwicklungsmethoden. Der Ansatz basiert auf den Formalisierungen des Secure-Information-Flows zur Sicherheitsverifikation. Dieser bietet die Möglichkeit für besonders detaillierte Sicherheitsanalysen. Da diese Formalisierungen traditioneller Weise im Kontext von Mandatory-Access-Control (MAC) benutzt werden und diese üblicherweise keine Vergabe von Rechten auf Benutzerebene beinhalten, war die Entwicklung in diesem Kontext bislang begrenzt. Da der Secure-Information-Flow-Ansatz in den letzten Jahren immer öfter zum Einsatz kommt, ist eins der Ziele dieses Projektes diese Lücke zu füllen. Im Rahmen des Projektes wird untersucht, wie die Analyse von komplexen Zugriffsteuerungstechniken, wie der Delegation von Berechtigungen unterstützt werden kann. Ein weiteres Ziel ist es, die Ergebnisse der modularen Analyse der Secure-Information-Flow-Eigenschaften im Zusammenhang der Zugriffssteuerungsmechanismen und der Delegation der Berechtigungen zu nutzen. Die wissenschaftlichen Ergebnisse werden dann in den Rahmen der Entwicklung sicherer Software basierend auf formaler Verifikation übertragen. Durch eine konkrete Anwendung im E-Health-Bereich werden diese Entwicklungen überprüft. Diese Anwendung findet in Zusammenarbeit mit bereits bestehenden Projekten des Fraunhofer ISST statt. Die wichtigsten Ergebnisse werden sein: