Trustworthy Tuesday #12 - Formally Verifying a Hypervisor

Beschreibung

In unserer nächsten Sitzung am 18. August wird Dominic Mulligan seinen Vortrag „Nitro Isolation Engine: formally verifying a production hypervisor?“ halten. Cloud-Computing stützt sich auf Hypervisoren, um die Isolation zwischen gemeinsam genutzten virtuellen Maschinen zu gewährleisten. Hypervisoren sind daher eine kritische Sicherheitsinfrastruktur, und die Gewährleistung ihrer Korrektheit ist von größter Bedeutung. Herkömmliche Entwicklungsmethoden – Code-Review, Tests, Fuzzing – bieten zwar eine hohe Sicherheit, können jedoch nicht ausreichend nachweisen, dass die Isolation über alle möglichen Ausführungspfade hinweg gewährleistet ist. Die formale Verifikation erweitert und ergänzt diese Ansätze, indem sie mathematische Garantien für das Systemverhalten liefert. In diesem Vortrag werden die Erfahrungen von AWS bei der Anwendung interaktiver Theorembeweise zur Verifikation einer Hypervisor-Komponente im Produktivbetrieb vorgestellt: der Nitro Isolation Engine.

Dominic Mulligan ist Leitender Anwendungswissenschaftler in der „Automated Reasoning Group“ bei Amazon Web Services (AWS).

Die Veranstaltung findet am 06. Oktober um 14:00 Uhr (UTC +2) statt. Die Veranstaltung wird über Zoom abgehalten. Die Aufzeichnung wird nach der Veranstaltung auf der ÖvIT-Website hochgeladen.

Zoom-Link: https://meetgi.zoom.us/j/63725933668?pwd=BTav7NSIxem2CaZCgGMQ4SY6xFTSXz.1