Mechanized modeling and security proofs for web protocols

Abstract

The Web plays a central role in modern life - not only for news and social interactions, but also in security-critical applications such as banking and healthcare. Many of these applications rely on standardized protocols, for example, for authentication and authorization. Hence, the security of many applications on the Web depends on the security of these protocols. Studying the security of protocols - not just on the Web - has been an active area of research for over four decades. An important branch of this research focuses on applying formal methods to obtain rigorous, formally proven security guarantees. However, in the context of Web protocols, the complexity of the underlying infrastructure - with multiple layers of sub-protocols and intricate interactions between involved parties (e.g., in-browser communication between websites) - poses significant challenges for such analyses. Yet this complexity must be captured, since even subtle design details may have security implications, as demonstrated by past attacks. This thesis advances the state of the art in Web protocol security analysis in several ways. First, we present a formal security analysis of the FAPI 2.0 protocol family, developed and used in high-risk domains such as banking and healthcare. Our analysis accompanied the development of the FAPI 2.0 protocols and is based on the most comprehensive and detailed security analysis framework for Web protocols to date, the Web Infrastructure Model (WIM) - a pen-and-paper Dolev-Yao-style model that captures many aspects of the Web environment, and in particular, many details of the inner workings of Web browsers. To faithfully model FAPI 2.0, we extend the WIM in several ways, for example, by introducing communication channels for push messaging and support for so-called HTTP Message Signatures. These extensions are derived from relatively recent, yet already established Web standards, and are therefore of independent interest for keeping the WIM up to date. Our analysis - the largest based on the WIM so far - uncovered multiple new attacks that led to fixes in the now-finalized FAPI 2.0 standards, and started an ongoing effort within the standardization body responsible for FAPI 2.0 to apply formal analysis to more and more of their standards. At the same time, this work illustrates the limitations of pen-and-paper proofs: our analysis spans more than 100 pages of hand-written, manually verified proofs. Hence, mechanized verification promises more reliable results, but existing mechanized tools struggle with the level of detail and resulting model size required for realistic Web models. To bridge this gap, we contribute to the development of DY*, a mechanized Dolev-Yao-style protocol analysis framework that supports implementation-level executable models, highly modular proofs over an explicit global trace, an extensible equational theory, and can cope well with unbounded data structures, loops, and recursion. While the long-term goal is to develop DY* into a Web protocol analysis framework - akin to the WIM, but fully mechanized - it has already been used in several nontrivial case studies, including the first formal analysis of the Signal protocol with an unbounded number of ratcheting rounds. Finally, as a first step toward such a mechanized Web protocol analysis framework based on DY*, we use DY* to analyze the immensely popular ACME certificate issuance protocol. In the course of this analysis, we extend DY* with authenticated channels, an enhanced equational theory to more precisely capture the properties of digital signatures, and develop a methodology to execute DY* models against real-world implementations. Our analysis is the first of the final ACME standard and ranks among the most detailed mechanized protocol security analyses to date - our executable model can even interact with real-world servers. Das Web ist aus dem modernen Leben nicht mehr wegzudenken und wird längst nicht mehr nur für News und sozialen Austausch genutzt, sondern auch in immer mehr höchst sensiblen Anwendungen, etwa im Banken- und Gesundheitssektor. Viele dieser Anwendungen nutzen dabei standardisierte Protokolle, zum Beispiel zur Authentifizierung und Autorisierung. Folglich hängt die Sicherheit dieser Anwendungen maßgeblich von der Sicherheit der verwendeten Protokolle ab. An der Untersuchung der Sicherheit von Protokollen - nicht nur im Web - wird bereits seit über vier Jahrzehnten geforscht. Eines der wichtigsten daraus entstandenen Forschungsfelder befasst sich mit der Nutzung formaler Methoden, um Sicherheitseigenschaften von Protokollen präzise zu fassen und zu beweisen. Eine besondere Herausforderung für die Analyse von Web-Protokollen - also solchen, die sich Web-Technologien zunutze machen - stellt dabei die inhärente Komplexität der zugrundeliegenden Web-Infrastruktur dar, etwa in Form von mehreren Ebenen an Teil-Protokollen, vielfältigen Interaktionsmöglichkeiten zwischen den beteiligten Parteien, oder der direkten Kommunikation zwischen Websites innerhalb eines Webbrowsers. Bereits entdeckte Angriffe zeigen dabei, dass selbst unscheinbare Details der Web-Infrastruktur dabei sicherheitsrelevant sein können, dementsprechend muss deren angesprochene Komplexität in einer Analyse abgebildet sein. Mit der vorliegenden Arbeit tragen wir in mehrerlei Hinsicht zum Stand der Wissenschaft zur formalen Sicherheitsanalyse von Web-Protokollen bei: Zunächst präsentieren wir eine formale Sicherheitsanalyse der FAPI 2.0-Protokollfamilie. Die FAPI 2.0-Web-Protokolle wurden entwickelt (und werden eingesetzt) zur Authentifizierung und Autorisierung in hochsensiblen Umgebungen, etwa beim Umgang mit Gesundheitsdaten; wir haben die Entwicklung dieser Protokolle mit unserer Analyse begleitet und unterstützt. Wir bauen unsere Analyse auf dem bislang umfangreichsten und detailliertesten Framework zur Sicherheitsanalyse von Web-Protokollen auf, dem Web Infrastructure Model (WIM). Das WIM ist ein Pen-and-Paper Dolev-Yao-Modell, das viele Aspekte der Web-Umgebung umfasst und insbesondere auch wichtige Details im Verhalten von Webbrowsern abbildet. Um die FAPI 2.0-Protokolle realitätsnah modellieren zu können, erweitern wir dabei das WIM an mehreren Stellen, etwa um Kommunikationskanäle für Push-Nachrichten und Unterstützung für die sogenannten HTTP Message Signatures. Diese Erweiterungen stützen sich auf aktuelle Web-Standards und tragen daher auch unabhängig von den FAPI 2.0-Protokollen dazu bei, das WIM aktuell zu halten. Unsere Analyse der FAPI 2.0-Protokolle ist die bislang umfangreichste WIM-basierte Sicherheitsanalyse und hat zur Entdeckung mehrerer bislang unbekannter Angriffe und in der Folge zu entsprechenden Anpassungen der inzwischen finalisierten FAPI 2.0-Standards geführt. Unsere Analyse hat zudem dazu beigetragen, dass das für FAPI 2.0 zuständige Standardisierungsgremium nun daran arbeitet, noch weitere der dort entwickelten Protokolle formal analysieren zu lassen. Gleichzeitig zeigt unsere Arbeit aber auch die Grenzen von Pen-and-Paper-Beweisen auf: Unsere Analyse umfasst über 100 Seiten manuell geführter Beweise, deren Überprüfung naturgemäß sehr aufwendig ist. Mechanisierte Verifikation verspricht hier zuverlässigere Ergebnisse - allerdings stoßen existierende Tools bei einer detaillierten Modellierung der Web-Umgebung an ihre Grenzen. Darum tragen wir zur Entwicklung von DY* bei, einem mechanisierten Dolev-Yao Analysetool mit erweiterbarer Equational Theory, hochgradig modularen Beweisen, einem expliziten globalen Trace, und guter Unterstützung für unbeschränkte Datenstrukturen, Schleifen und Rekursion. DY*-Modelle sind dabei ausführbar und können hochgradig detailliert sein, bis hin zum Detailgrad einer Implementierung. Auch wenn DY* langfristig als Basis für ein Framework für die Sicherheitsanalyse von Web-Protokollen - ähnlich zum WIM, aber mechanisiert - dienen soll, wurde es bereits für mehrere umfangreiche Protokoll-Sicherheitsanalysen (abseits des Web) verwendet, unter anderem in der ersten formalen Analyse des Signal-Protokolls ohne Beschränkung der Ratcheting-Runden. Zuletzt - und als ersten Schritt, um zukünftig Web-Protokolle auf Basis von DY* zu analysieren - präsentieren wir unsere Sicherheitsanalyse des weit verbreiteten ACME-Zertifikatsmanagement-Protokolls. Im Rahmen dieser Analyse erweitern wir DY* um authentifizierte Kommunikationskanäle, eine präzisere Equational Theory für Signaturen und entwickeln eine Methodik, um Interaktion zwischen DY*-Modellen und realen Implementierungen zu ermöglichen. Unsere ACME-Analyse ist die erste formale Sicherheitsanalyse des finalen ACME-Standards und gehört zu den detailliertesten mechanisierten Analysen in der Literatur - unser Modell ist sogar detailliert genug, um das Protokoll mit realen Servern als Gegenüber auszuführen.