UCL Discovery
UCL home » Library Services » Electronic resources » UCL Discovery

Using model checking tools to triage the severity of security bugs in the Xen hypervisor

Cook, B; Döbel, B; Kroening, D; Manthey, N; Pohlack, M; Polgreen, E; Tautschnig, M; (2020) Using model checking tools to triage the severity of security bugs in the Xen hypervisor. In: Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020. (pp. pp. 185-193). TU Wien Academic Press: Vienna, Austria. Green open access

[thumbnail of 26_Using model checking tools to triage the severity of security bugs in the Xen hypervisor.pdf]
Preview
Text
26_Using model checking tools to triage the severity of security bugs in the Xen hypervisor.pdf - Published version

Download (342kB) | Preview

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.

Type: Proceedings paper
Title: Using model checking tools to triage the severity of security bugs in the Xen hypervisor
Event: Formal Methods in Computer-Aided Design 2020
Open access status: An open access version is available from UCL Discovery
DOI: 10.34727/2020/isbn.978-3-85448-042-6_26
Publisher version: https://doi.org/10.34727/2020/isbn.978-3-85448-042...
Language: English
Additional information: This article is licensed under a Creative Commons Attribution 4.0 International License (https://creativecommons.org/licenses/by/4.0/)
Keywords: computer-aided system design
UCL classification: UCL
UCL > Provost and Vice Provost Offices > UCL BEAMS
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science
URI: https://discovery.ucl.ac.uk/id/eprint/10119837
Downloads since deposit
8Downloads
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item