The German Informatics Society as part of the Ecosystem Formally Verifiable IT (EvIT) has launched a webinar series called “Trustworthy Tuesday”. Once a month, researchers will present their work in the field of formal verification. After lunch at 2 pm CET, you can join the “snackable science” format.
Students, experts and other interested parties are invited to “snack” on this new knowledge after their lunch break.
In the 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 ASW’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 via Zoom. The recording will be uploaded to the EvIT website after the event.
If you have any questions, please reach out to protect@gi.de.
