Detailseite
Projekt
Security Type Systems and Deduction
Antragsteller
Professor Tobias Nipkow, Ph.D.
Fachliche Zuordnung
Softwaretechnik und Programmiersprachen
Theoretische Informatik
Theoretische Informatik
Förderung
Förderung von 2010 bis 2015
Projektkennung
Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 183816297
Das Ziel dieses Projektes ist die durchgehende Verifikation der Informationsfluss-Sicherheit eines Web-basierten Konferenzmanagement Systems. Dabei handelt es sich um ein wichtiges Beispiel eines Web-basierten Workflowmanagement Systems und unsere Ergebnisse werden im Prinzip auf alle Systeme dieser Art anwendbar sein.Die wichtigsten Herausforderungen in der Modellierung und Verifikation solcher Systeme sind die Folgenden. Das System muss sowohl benutzbar als auch verifiziert sein. Es gibt komplexe Bedingungen, die regulieren, wann Information weitergegeben werden darf. Die Sicherheitseigenschaften sollten systematisch alle Quellen vertraulicher Information im System erfassen. Die Verifikation sollte durchgehend sein und alle Ebenen des Systems erfassen, nicht nur den Kern sondern auch das Web Interface.Die folgenden Methoden dienen dazu, diesen Herausforderungen zu begegnen. Alle komplexe Funktionalität wird im Kern konzentriert, der interaktiv verifiziert wird. Der Beweis der Abwesenheit von Informationslecks im schmalen Interface wird an automatische Werkzeuge deligiert, die von anderen Projekten im selben Schwerpunktprogramm entwickelt werden. Das System wird so in Komponenten zerlegt, dass die Kombination der interaktiven mit der automatischen Verifikation die gewünschten Sicherheitseigenschaften in kompositionaler Weise ergibt. Außerdem werde wir Methoden entwickeln, die es uns erlauben, die Verifikation unendlicher Systeme durch Abstraktion auf Model Checking Probleme für endliche Systeme zu reduzieren.Ein wichtiges Ergebnis unserer Forschung wird eine wiederverwendbarer Rahmen zur Modellierung und Verifikation Web-basierter Workflowmanagement Systeme sein.
DFG-Verfahren
Schwerpunktprogramme
