SpecBMC - A Bounded Model Checker for Speculative Non-Interference

Abstract

Moderne Prozessoren verwenden Sprungvorhersage und spekulative Ausführung für die Steigerung der Ausführungsgeschwindigkeit. Ist die Vorhersage korrekt, so kann der Prozessor die Wartezeit mittels Vorberechnung vermeiden. Ist die Vorhersage jedoch inkorrekt, so werden die vorab berechneten Ergebnisse einfach verworfen und somit ist nur die Wartezeit verschwendet. Jedoch haben Wissenschaftler im Jahr 2018 gezeigt, dass manche Seiteneffekte der spekulativen Ausführung auch nach dem Verwerfen der inkorrekten Spekulation erhalten bleiben. Diese übriggebliebenen Seiteneffekte erlauben es sensitive Informationen aus der spekulativen Ausführung heraus zu transferieren. Die sogenannten Spectre Attacken waren geboren. Obwohl Spectre zu der Klasse der Hardware-Fehler zählt, gibt es mehrere mögliche software-basierte Gegenmaßnahmen. Spectre Schwachstellen sind jedoch schwierig zu finden und zu unterbinden. Im Rahmen dieser Arbeit wird eine formale Semantikbeschreibung für spekulatives Ausführungsverhalten entwickelt. Diese Semantik erlaubt es uns sowohl Spectre-PHT als auch Spectre-STL Schwachstellen formal zu erfassen. Des weiteren definieren wir eine Eigenschaft von Programmen die es uns erlaubt, Aussagen über die Sicherheit im Bezug auf Spectre Attacken zu treffen. Ein Programm wird als sicher angesehen, falls das Programm ausgeführt auf einem Prozessor mit spekulativem Verhalten die selben erkennbaren sicherheitssensitiven Seiteneffekte erzeugt, wie das identische Programm ausgeführt auf einem Prozessor ohne jegliche Spekulation. Basierend auf der formalen Beschreibung wird ein statisches Analysewerkzeug entwickelt um Spectre Schwachstellen effizient auffinden zu können. SpecBMC wird gegen eine Vielzahl von Spectre Beispielprogrammen evaluiert, zudem zeigen wir das viele der vorgeschlagenen Gegenmaßnahmen nachweislich funktionieren. In einer abschließenden Fallstudie deckt SpecBMC eine subtile Spectre-PHT Schwachstelle im Linux Kernel auf.

Modern processors employ branch prediction and speculative execution to improve the computing performance. If the prediction is correct the processor avoids a costly delay by pre-computing the results, while in case of a mis-prediction the speculatively computed results are simply thrown away and thus only the waiting time is wasted. In the year 2018 researchers have shown, that some side effects of the mis-predicted speculative execution remain even after rollback, thereby allowing an adversary to leak sensitive information from within the speculative execution. The so-called Spectre attacks were born. Although Spectre belongs to the class of hardware bugs, some software-based countermeasures have been proposed. But Spectre vulnerabilities are hard to detect and mitigate. In the scope of this thesis a formal semantics for speculative execution is developed. The semantics allows us to formally capture Spectre-PHT and Spectre-STL vulnerabilities, which rely on control- respectively data-flow mis-predictions. Furthermore, we define a hyperproperty to reason about the security of a program in respect to speculative execution attacks. A program is considered secure, if the program executed on a CPU with speculation has the same adversary observable security sensitive side effects as if the program is executed on a CPU without speculation. Based on the formal definition, a bounded software model-checker for efficiently detecting Spectre-style vulnerabilities in binary programs is implemented. We validate SpecBMC against different Spectre examples and check if the different proposed countermeasures actually work. Finally, we conduct a small case study and reveal a subtile Spectre-PHT bug in the Linux kernel.