DC FieldValueLanguage
dc.contributor.advisorWeissenbacher, Georg-
dc.contributor.authorPescosta, Emmanuel-
dc.date.accessioned2020-11-13T09:42:43Z-
dc.date.issued2020-
dc.date.submitted2020-
dc.identifier.citation<div class="csl-bib-body"> <div class="csl-entry">Pescosta, E. (2020). <i>SpecBMC : bounded model checker for speculative non-interference</i> [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2020.76820</div> </div>-
dc.identifier.urihttps://doi.org/10.34726/hss.2020.76820-
dc.identifier.urihttp://hdl.handle.net/20.500.12708/16183-
dc.descriptionAbweichender Titel nach Übersetzung der Verfasserin/des Verfassers-
dc.description.abstractModerne 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.de
dc.description.abstractModern 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.en
dc.formatxiii, 143 Seiten-
dc.languageEnglish-
dc.language.isoen-
dc.subjectformale Verifikationde
dc.subjectProgramm Analysede
dc.subjectstatische Analysede
dc.subjectSoftware Verifikationde
dc.subjectspekulative Ausführungde
dc.subjectSpectrede
dc.subjecttransiente Ausführungsattackende
dc.subjectSicherheitde
dc.subjectBounded Model Checkerde
dc.subjectFormal Verificationen
dc.subjectBinary Analysisen
dc.subjectStatic Analysisen
dc.subjectSoftware Verificationen
dc.subjectSpeculative Executionen
dc.subjectSpectreen
dc.subjectTransient Execution Attacksen
dc.subjectSecurityen
dc.subjectBounded Model Checkeren
dc.titleSpecBMC : bounded model checker for speculative non-interferenceen
dc.title.alternativeSpecBMC - Bounded Model Checking von Spekulativen Ausführungende
dc.typeThesisen
dc.typeHochschulschriftde
dc.identifier.doi10.34726/hss.2020.76820-
dc.publisher.placeWien-
tuw.thesisinformationTechnische Universität Wien-
dc.contributor.assistantZuleger, Florian-
tuw.publication.orgunitE192 - Institut für Logic and Computation-
dc.type.qualificationlevelDiploma-
dc.identifier.libraryidAC16072070-
dc.description.numberOfPages143-
dc.thesistypeDiplomarbeitde
dc.thesistypeDiploma Thesisen
item.cerifentitytypePublications-
item.cerifentitytypePublications-
item.fulltextwith Fulltext-
item.grantfulltextopen-
item.openaccessfulltextOpen Access-
item.languageiso639-1en-
item.openairecristypehttp://purl.org/coar/resource_type/c_18cf-
item.openairecristypehttp://purl.org/coar/resource_type/c_18cf-
item.openairetypeThesis-
item.openairetypeHochschulschrift-
Appears in Collections:Thesis

Files in this item:


Google ScholarTM

Check


Items in reposiTUm are protected by copyright, with all rights reserved, unless otherwise indicated.