University of Cambridge > Talks.cam > Isaac Newton Institute Seminar Series > Model Checking: Using Model Checking Tools to Triage the Severity of Security Bugs in Xen Hypervisor

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2022 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity