Using Model Checking Tools to Triage the Severity of Security Bugs in the Xen Hypervisor

Byron Cook, Bjoern Doebel, Daniel Kroening, Norbert Manthey, Martin Pohlack, Elizabeth Polgreen, Michael Tautschnig, Pawel Wieczorkiewicz

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

In practice, few security bugs found in source code are urgent, but quickly identifying which ones are is hard. We describe the application of bounded model checking to triaging reported issues quickly at the cloud service provider Amazon Web Services (AWS). We focus on the job of reactive security experts who need to determine the severity of bugs found in the Xen hypervisor. We show that, using our publicly available extensions to the model checker CBMC, a security expert can obtain traces to construct security tests and estimate the severity of the reported finding within 15 minutes. We believe that the changes made to the model checker, as well as the methodology for using tools in this scenario, will generalise to other organisations and environments.
Original languageEnglish
Title of host publicationProceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020
EditorsAlexander Ivrii, Ofer Strichman
PublisherTU Wien Academic Press
Pages185-193
Number of pages9
ISBN (Electronic)978-3-85448-042-6
DOIs
Publication statusPublished - 23 Sep 2020
Event20th Confernce on Formal Methods in Computer-Aided Design - Virtual conference
Duration: 21 Sep 202024 Sep 2020
https://fmcad.forsyte.at/FMCAD20/

Publication series

NameConference Series: Formal Methods in Computer-Aided Design
PublisherTU Wien Academic Press
Volume1
ISSN (Electronic)2708-7824

Conference

Conference20th Confernce on Formal Methods in Computer-Aided Design
Abbreviated titleFMCAD 2020
CityVirtual conference
Period21/09/2024/09/20
Internet address

Fingerprint

Dive into the research topics of 'Using Model Checking Tools to Triage the Severity of Security Bugs in the Xen Hypervisor'. Together they form a unique fingerprint.

Cite this