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

Add to your list(s) Download to your calendar using vCal

• Elizabeth Polgreen (University of Edinburgh)
• Friday 22 July 2022, 10:15-11:00
• Seminar Room 2, Newton Institute.

If you have a question about this talk, please contact nobody.

VSO2 - Verified software

: In practice, few security bugs found in source code are urgent, but quickly identifying which ones are is hard. In security-critical applications, this can be the difference between deciding to wake up an entire engineering team in the middle of the night or not. In this talk, I will 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.

This talk is part of the Isaac Newton Institute Seminar Series series.

This talk is included in these lists:

• All CMS events
• Featured lists
• INI info aggregator
• Isaac Newton Institute Seminar Series
• School of Physical Sciences
• Seminar Room 2, Newton Institute
• bld31

Note that ex-directory lists are not shown.