WebAPISpec: An extensible, machine checked model of secure browser specifications

Abstract

Browser werden auf der Grundlage von Spezifikationen implementiert, die von unterschiedlichen Personengruppen verfasst wurden. Spezifikationen für verschiedene Komponentendes Browsers können aufgrund der Komplexität der Software so widersprüchlich sein, dass Sicherheitslücken entstehen. Eine Möglichkeit, die Wahrscheinlichkeit solcher Spezifikationsfehler zu verringern, besteht darin, ein formales Modell des Browsers zu erstellen, das mechanisch auf Konflikte überprüft werden kann, anstatt sich darauf zu verlassen, dass Menschen informelle schriftliche Beschreibungen auf potenzielle Probleme untersuchen.Wir schlagen ein neues Browser-Spezifikationsmodell vor, das mithilfe von Verfeinerungstypen überprüft, ob alle bereitgestellten API-Funktionen unsere definierte Sicherheits-invariante beibehalten. Das Modell ist ein Übergangssystem, in dem der Zustand die Browser-Interna und die Ereignisverfolgung sind und die API-Funktionen Zustandsübergänge sind. Wenn alle API-Funktionen sicher sind, kann jedes Skript, das nur über dieseFunktionen mit dem Browser interagiert, die Invariante nicht verletzen. Die Invariante ist eine Konjunktion bestehender Invarianten für Komponentensicherheit aus der Literatur,die wir als Subinvarianten bezeichnen.Mit diesem Ansatz können wir nachweisen, dass Skripte sicher sind, ohne den Inhalt der Skripte selbst zu modellieren. Wir sind auch in der Lage, ungebundene Spuren zu modellieren, ohne die exponentielle Explosion eines traditionelleren Ansatzes zur Erkundung des Zustandsraums. Zusätzlich dazu, dass wir das Übergangssystem nicht erforscht haben, konnten wir der Erweiterbarkeit Priorität einräumen, indem wir das Modulsystem von Coq nutzten und das Umschreiben von Beweisen bei der Einführung neuer Komponenten minimierten. Wie in unseren Hauptergebnissen dargestellt, konnten wir die Beweissuche mithilfe der Hammer-Bibliothek für die Funktionen einer bestimmten Komponente im Hinblick auf Beweise für die Subinvarianten anderer Komponenten weitgehend automatisieren.

Browsers are implemented based on specifications written by disjoint groups of people. Specifications for different components of the browser can end up being contradictory in a way that introduces security bugs because of the complexity of the software. One way to reduce the likelihood of such specification bugs is to build a formal model of the browser that can be mechanically checked for clashes instead of relying on people to examine informal written descriptions for potential problems. We propose a new browser specification model that uses refinement types to check that all provided API functions maintain our defined security invariant. The model is a transition system in which the state is the browser internals and trace of events and the state transitions are the API functions. If all API functions are safe, then any script which only interacts with the browser using those functions cannot violate the invariant. Theinvariant is a conjunction of existing component security invariants from the literature, which we refer to as subinvariants. This approach allows us to prove that scripts are safe without modeling the contents ofthe scripts themselves. We are also able to model unbound traces without the exponential blow up of more traditional state space exploration approach. In addition, we were able to prioritize extensibility by using Coq’s module system and minimizing proof rewrites as new components are introduced. As presented in our main findings, we were able to mostly automate proof search using the Hammer library for a given component’s functions with regards to proofs of other components’ subinvariants.