Ein werkzeugunterstütztes ausdrucksstarkes Modell für die Webinfrastruktur

• Antragsteller: Professor Dr. Ralf Küsters
• Fachliche Zuordnung: Sicherheit und Verlässlichkeit, Betriebs-, Kommunikations- und verteilte Systeme
• Förderung: Förderung von 2015 bis 2020
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 276807658

Das World Wide Web ist eine zentrale und unverzichtbare Informations- und Kommunikationstechnologie für moderne Gesellschaften. Dementsprechend hat die Bedeutung von Sicherheit und Privacy im Web deutlich zugenommen. Das Web stellt eine komplexe Infrastruktur dar, bei der etwa DNS-Server, Webserver und Webbrowser mittels unterschiedlicher Technologien interagieren und kommunizieren. Angesichts zahlreicher Angriffe auf die Webinfrastruktur und auf Webanwendungen und der wachsenden Komplexität des Web ist eine rigorose und systematische Analyse von Sicherheits- und Privacy-Eigenschaften sowohl der Webinfrastruktur als auch von Webanwendungen essentiell. Um derartige Analysen durchführen zu können, bedarf es eines formalen Modells der Webinfrastruktur, welches es erlaubt, Sicherheits- und Privacy-Eigenschaften von Webstandards und Webanwendungen präzise zu formalisieren und schließlich zu beweisen. In vorangegangen Arbeiten des Antragstellers und im Vorgängerprojekt wurde ein solches Modell entwickelt und erfolgreich eingesetzt, um u.a. weit verbreitete Webstandards und -applikationen zu analysieren. Dabei wurden in fast allen Fällen schwerwiegende Sicherheitslücken aufgedeckt. Diese wurden geschlossen und es konnten für die verbesserten Systeme zum ersten Mal Sicherheits- und Privacy-Eigenschaften bewiesen werden. Allerdings müssen Sicherheitsbeweise im entwickelten Modell bisher manuell durchgeführt werden, ohne Werkzeugunterstützung. Dies bringt verschiedene Nachteile mit sich, wie etwa eine erhöhte Fehleranfälligkeit sowie einen Mangel an Wiederverwendbarkeit und Zugänglichkeit der Modelle und Resultate für Nichtexperten. Das wesentliche Ziel dieses Projektes ist deshalb die Entwicklung einer geeigneten Werkzeugunterstützung, die manuelle Beweise unnötig macht. Genauer soll das Webmodell in der funktionalen Programmiersprache F* formalisiert werden, die Mechanismen für die Programmverifikation direkt eingebaut hat. Im Rahmen des Projektes wird das werkzeugunterstützte Webmodell dann verwendet, um wichtige Webanwendungen und -standards zu analysieren. Zudem soll es eingesetzt werden, um verifizierte Implementationen automatisch aus Modellen von Webanwendungen abzuleiten, Testfälle für Webanwendungen zu generieren sowie aus fehlgeschlagenen Sicherheitsbeweisen Angriffe zu erzeugen.

• DFG-Verfahren: Sachbeihilfen