Cook, B; Döbel, B; Kroening, D; Manthey, N; Pohlack, M; Polgreen, E; Tautschnig, M; Cook, B; Döbel, B; Kroening, D; Manthey, N; Pohlack, M; Polgreen, E; Tautschnig, M; Wieczorkiewicz, P; - view fewer (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.

Download activity - last month

Export as JSONXMLCSV

Download activity - last 12 months

Export as XMLJSONCSV

Downloads by country - last 12 months

Export as CSVXMLJSON

Archive Staff Only

View Item