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

• Erstellungsjahr: 2024

Zusammenfassung der Projektergebnisse

Viele der heute üblichen Webanwendungen erfordern die Zusammenarbeit mehrerer Parteien. So ermöglichen etwa sogenannte Single-Sign-On-Systeme wie “Anmelden mit Apple” Benutzern, sich bei Websites wie tripadvisor.com mit einem bestehenden Account bei einem Identity Provider (IdP) anzumelden. Dabei wird die Interaktion zwischen den Parteien, hier der Webseite, dem IdP und dem Webbrowser des Benutzers durch ein (Web-)Protokoll geregelt, in diesem Fall das OpenID Connect (OIDC) Webprotokoll. Dabei ist die Sicherheit solcher Protokolle entscheidend, z.B. um Identitätsdiebstahl zu verhindern. Die Komplexität des Web macht es jedoch unmöglich, Sicherheit allein durch “genaues Betrachten” von Protokollen oder Befolgen von Best Practices sicherzustellen. Hier bietet formale Analyse einen Weg, Protokolle als sicher zu beweisen. Für Webprotokolle erfordert dies die Modellierung der Webumgebung: Webbrowser, Java- Script, Webserver, HTTP(S) usw. Zu Beginn dieses Projektes gab es lediglich eine handvoll solcher Modelle, und diese waren meist sehr abstrakt, mit Ausnahme des Web-Infrastruktur- Modells (WIM), das wir in Vorarbeiten entwickelt hatten. Basierend darauf war das Hauptziel dieses Projekts, das WIM weiterzuentwickeln und zu verwenden, um die Sicherheit wichtiger internationaler Protokollstandards formal zu analysieren, einschließlich (1) OIDC, das von Apple, Microsoft, Google und Facebook mit Milliarden von Benutzern verwendet wird, (2) OAuth 2.0, das zur Autorisierung von Drittanbieterzugriff auf Benutzerdaten, z.B. GMail, verwendet wird und (3) die Financial-grade API 1.0, die u.a. für E-Government und im Bankwesen mit hunderten Millionen Benutzern verwendet wird. In allen diesen Analysen haben wir bisher unbekannte Angriffe identifiziert, als sicher bewiesene Lösungen vorgeschlagen und an die Standardisierungsgremien gemeldet, was zu verbesserten Protokollstandards führte. Für OAuth 2.0 waren die Angriffe so schwerwiegend, dass das Standardisierungsgremium ein Notfalltreffen einberief, aus dem der nun jährlich stattfindende OAuth Security Workshop hervorging. Weiterhin haben wir mit der Entwicklung unseres Tools DY* erste Schritte unternommen, um das WIM zu mechanisieren und so werkzeuggestützte Sicherheitsanalysen zu ermöglichen. DY* ist ein Tool für formale Sicherheitsanalysen von Protokollen, kombiniert zwei zuvor getrennte Paradigmen für solche Tools und überwindet damit mehrere Einschränkungen bestehender Tools. Daher eignet sich DY* nicht nur als Grundlage für die Mechanisierung des WIM, sondern ist auch über den Rahmen dieses Projekts hinaus von großem Interesse.

Projektbezogene Publikationen (Auswahl)

• Analyzing the BrowserID SSO System with Primary Identity Providers Using an Expressive Model of the Web. Lecture Notes in Computer Science, 43-65.
  Fett, Daniel; Küsters, Ralf & Schmitz, Guido
  
• SPRESSO. Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security, 1358-1369.
  Fett, Daniel; Küsters, Ralf & Schmitz, Guido
  
• A Comprehensive Formal Security Analysis of OAuth 2.0. Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, 1204-1215.
  Fett, Daniel; Küsters, Ralf & Schmitz, Guido
  
• Guest Blog: Formal Analysis of the OpenID Financialgrade API. 2017. Invited blog post
  D. Fett; P. Hosseyni & R. Küsters
  
• The Web SSO Standard OpenID Connect: In-depth Formal Security Analysis and Security Guidelines. 2017 IEEE 30th Computer Security Foundations Symposium (CSF), 189-202.
  Fett, Daniel; Kusters, Ralf & Schmitz, Guido
  
• “An Expressive Formal Model of the Web Infrastructure”. PhD thesis. University of Stuttgart, Germany, 2018
  D. Fett
  
• An Extensive Formal Security Analysis of the OpenID Financial-Grade API. 2019 IEEE Symposium on Security and Privacy (SP).
  Fett, Daniel; Hosseyni, Pedram & Kusters, Ralf
  
• “Privacy-Preserving Web Single Sign-On: Formal Security Analysis and Design”. PhD thesis. University of Stuttgart, Germany, 2019
  G. Schmitz
  
• $\text{DY}^{\star}$: A Modular Symbolic Verification Framework for Executable Cryptographic Protocol Code. 2021 IEEE European Symposium on Security and Privacy (EuroS&P), 523-542.
  Bhargavan, Karthikeyan; Bichhawat, Abhishek; Do Quoc, Huy; Hosseyni, Pedram; Küsters, Ralf; Schmitz, Guido & Würtele, Tim
  
• A Tutorial-Style Introduction to $$\textsf {DY}^\star $$. Lecture Notes in Computer Science, 77-97.
  Bhargavan, Karthikeyan; Bichhawat, Abhishek; Do Quoc, Huy; Hosseyni, Pedram; Küsters, Ralf; Schmitz, Guido & Würtele, Tim
  
• An In-Depth Symbolic Security Analysis of the ACME Standard. Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security, 2601-2617.
  Bhargavan, Karthikeyan; Bichhawat, Abhishek; Do Quoc, Huy; Hosseyni, Pedram; Küsters, Ralf; Schmitz, Guido & Würtele, Tim
  
• DY* Code
  K. Bhargavan; A. Bichhawat; Q. H. Do; P. Hosseyni; R. Küsters; G. Schmitz & T. Würtele
  
• Layered Symbolic Security Analysis in $$\textsf {DY}^\star $$. Lecture Notes in Computer Science, 3-21.
  Bhargavan, Karthikeyan; Bichhawat, Abhishek; Hosseyni, Pedram; Küsters, Ralf; Pruiksma, Klaas; Schmitz, Guido; Waldmann, Clara & Würtele, Tim