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.
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 |
Archive Staff Only
![]() |
View Item |