Sprungmarken

Servicenavigation

Fachbereich Informatik Institut für Softwaretechnik
Institut für Softwaretechnik

Forschungsgruppe
Software Engineering

Hauptnavigation


Bereichsnavigation



This page in English

Informationen

Kontakt

Universität Koblenz-Landau

Institut für Softwaretechnik

Universitätsstraße 1
D-56070 Koblenz



Ansprechpartner

Links

Hauptinhalt

Modular Modeling of Delegation Security in Software Development (MoDelSec)

DFG-SPP RS3 (2010-2012)



Projektbeschreibung


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:

  • Eine Theorie zur Unterstützung der modularen Analyse der Delegation von Berechtigungen in Secure-Information-Flow-Modellen
  • Die Integration in den Ansatz zur Entwicklung sicherer Software basierend auf formaler Verifikation
  • Automatisierte Werkzeuge für eine formale Verifikation basierend auf SMT (wie Z3)
  • Validierung durch Anwendung in einen E-Health-System mit Delegation der Berechtigungen


Publikationen