Trustworthy Tuesday #12 - Formally Verifying a Hypervisor

Description

In our next session on October 6th, Dominic Mulligan will give his presentation “Nitro Isolation Engine: formally verifying a production hypervisor?”. Cloud computing relies on hypervisors to enforce isolation between co-tenanted virtual machines. Hypervisors are therefore critical security infrastructure, and assurance of their correctness is paramount. Traditional engineering techniques—code review, testing, fuzzing—provide strong assurance but cannot exhaustively verify that isolation holds across all possible execution paths. Formal verification extends and complements these approaches by establishing mathematical guarantees about system behaviour. This talk presents AWS’s experience applying interactive theorem proving to verify a production hypervisor component: the Nitro Isolation Engine.  

Dominic Mulligan is Principal Applied Scientist within the Automated Reasoning Group for Amazon Web Services (AWS).

The event is happening on October 6th, starting at 2pm (UTC +2). The event will be held on Zoom. The recording will be uploaded to the EvIT website after the event.

Join us here: https://meetgi.zoom.us/j/63725933668?pwd=BTav7NSIxem2CaZCgGMQ4SY6xFTSXz.1