Bitte benutzen Sie diese Kennung, um auf die Ressource zu verweisen: http://dx.doi.org/10.18419/opus-10197
Autor(en): Fett, Daniel
Titel: An expressive formal model of the web infrastructure
Erscheinungsdatum: 2018
Dokumentart: Dissertation
Seiten: 240
URI: http://nbn-resolving.de/urn:nbn:de:bsz:93-opus-ds-102142
http://elib.uni-stuttgart.de/handle/11682/10214
http://dx.doi.org/10.18419/opus-10197
Zusammenfassung: The World Wide Web is arguably the most important medium of our time. Billions of users rely on the security of the web each day for tasks such as banking, shopping, and business and private communication. The web is a heterogeneous infrastructure developing at a high pace. The question of whether the web infrastructure or certain web applications are secure is not easy to answer. Standards and applications today are reviewed by experts before they are deployed, but all too often even serious security vulnerabilities are simply overlooked. In this thesis, we propose a formal model for the web infrastructure which enables a rigorous formal analysis of security and privacy in the web. Our model is the most comprehensive and expressive model of the web infrastructure to date. It facilitates accurate security and privacy analyses of current web standards and applications, and can serve as a reference for web security researchers, developers of new technologies and standards, and for teaching web security concepts. As a case study we analyze the security of two important standards for federated authorization and authentication, OAuth 2.0 and OpenID Connect. Standardized by the IETF and OpenID Foundation, respectively, they are among the most widely deployed single sign-on systems in the web. For our analysis, we develop detailed formal models for both systems based on our model of the web infrastructure. These models then allow us to precisely define the security goals of authentication, authorization and session integrity. While proving security with respect to these goals, we found a total of five new attacks on the two single sign-on systems, breaking all of the security goals. In particular OAuth 2.0 had been analyzed many times before; the fact that we were able to find new attacks in OAuth 2.0 demonstrates the potential of rigorous analyses in our web infrastructure model. We develop fixes against the underlying vulnerabilities and are then able to prove the security of OAuth 2.0 and OpenID Connect. Since our results are based on a comprehensive model, our proofs can exclude large classes of attacks against OAuth and OpenID Connect, including yet unknown attack vectors. Our attacks and fixes led to the development of new security recommendations by the standardization organizations.
Das World Wide Web ist wohl das wichtigste Medium unserer Zeit. Milliarden von Nutzern verlassen sich täglich für Banking, Shopping sowie geschäftliche und private Kommunikation auf die Sicherheit des Internets. Das Web ist eine heterogene Infrastruktur, die sich in hohem Tempo entwickelt. Die Frage, ob die Web-Infrastruktur oder bestimmte Web-Anwendungen sicher sind, ist nicht einfach zu beantworten. Standards und Anwendungen werden heute von Experten überprüft, bevor sie eingesetzt werden, aber allzu oft werden auch schwerwiegende Sicherheitslücken einfach übersehen. In dieser Arbeit schlagen wir ein formales Modell für die Web-Infrastruktur vor, das eine rigorose formale Analyse der Sicherheit und Privacy im Web ermöglicht. Unser Modell ist das bisher umfassendste und ausdrucksstärkste Modell für die Web-Infrastruktur. Es ermöglicht genaue Sicherheits- und Privacyanalysen aktueller Webstandards und Anwendungen und kann als Referenz für Websicherheitsforscher, Entwickler neuer Technologien und Standards sowie für die Vermittlung von Websicherheitskonzepten dienen. Als Fallstudie analysieren wir die Sicherheit zweier wichtiger Standards für föderierte Autorisierung und Authentifizierung, OAuth 2.0 und OpenID Connect. Von der IETF bzw. OpenID Foundation standardisiert, gehören sie zu den am weitesten verbreiteten Single-Sign-On-Systemen im Web. Für unsere Analyse entwickeln wir detaillierte formale Modelle für beide Systeme auf Basis unseres Modells der Web-Infrastruktur. Diese Modelle erlauben es uns dann, die Sicherheitsziele Authentifizierung, Autorisierung und Sitzungsintegrität genau zu definieren. Während des Beweises der Sicherheit in Bezug auf diese Ziele fanden wir insgesamt fünf neue Angriffe auf die beiden Single-Sign-On-Systeme, die alle Sicherheitsziele verletzen. Insbesondere OAuth 2.0 wurde zuvor bereits vielfach analysiert; die Tatsache, dass wir noch neue Angriffe finden konnten, zeigt das Potenzial rigoroser Analysen in unserem Web-Infrastrukturmodell auf. Wir entwickeln Schutzmaßnahmen gegen die zugrunde liegenden Schwachstellen und sind dann in der Lage, die Sicherheit von OAuth 2.0 und OpenID Connect zu beweisen. Da unsere Ergebnisse auf einem umfassenden Modell basieren, können unsere Beweise große Klassen von Angriffen gegen OAuth und OpenID Connect ausschließen, einschließlich noch unbekannter Angriffsvektoren. Unsere Angriffe und Schutzmaßnahmen führten zur Entwicklung neuer Sicherheitsempfehlungen durch die Standardisierungsorganisationen.
Enthalten in den Sammlungen:05 Fakultät Informatik, Elektrotechnik und Informationstechnik

Dateien zu dieser Ressource:
Datei Beschreibung GrößeFormat 
'An Expressive Formal Model of the Web Infrastructure.pdf1,38 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repositorium sind urheberrechtlich geschützt.