BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Model Checking:  Using Model Checking Tools to Triage the Severity
  of Security Bugs in Xen Hypervisor -  Elizabeth  Polgreen (University of 
 Edinburgh)
DTSTART:20220722T091500Z
DTEND:20220722T100000Z
UID:TALK176735@talks.cam.ac.uk
DESCRIPTION:: In practice\, few security bugs found in source code are urg
 ent\, 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. \nIn this talk\
 , I will describe the application of bounded model checking to triaging re
 ported issues quickly at the cloud service provider Amazon Web Services (A
 WS). We focus on the job of reactive security experts who need to determin
 e the severity of bugs found in the Xen hypervisor. We show that\, using o
 ur publicly available extensions to the model checker CBMC\, a security ex
 pert can obtain traces to construct security tests and estimate the severi
 ty 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.
LOCATION:Seminar Room 2\, Newton Institute
END:VEVENT
END:VCALENDAR