Verifying a Virtualization Stack at BedRock Systems

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

• Gregory Malecha (Bed Rock Systems)
• Tuesday 05 July 2022, 16:00-17:00
• Seminar Room 1, Newton Institute.

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

VS2W01 - Vistas in Verified Software

Virtualization provides unique challenges to verification. While the specification of a virtualization stack is relatively straightforward – behave like “bare metal”, BedRock’s bare metal property™ – virtualization systems in practice are large, concurrent, and performance sensitive. In this talk, I discuss BedRock Systems’ approach to verifying the bare metal property™ of the BedRock Hypervisor™, a microkernel-based virtualization. These challenges stem from applying formal methods to an industrial, systems-level code base following microkernel best practices. BedRock uses concurrent separation logic to build highly-concurrent specifications and proofs directly on source code. BHV ™ is implemented in modern C++, is relatively large, highly concurrent, and is built modularly from multiple, coordinating applications. 

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 1, Newton Institute
• bld31

Note that ex-directory lists are not shown.