Formal Verification of Software-Defined Network Elements and Machine Code
Tid: Må 2025-12-08 kl 13.00
Plats: Kollegiesalen, Brinellvägen 8, Stockholm
Videolänk: https://kth-se.zoom.us/j/61627100868
Språk: Engelska
Ämnesområde: Datalogi
Respondent: Didrik Lundberg , Teoretisk datalogi, TCS, Saab AB, Sweden
Opponent: Professor Emeritus Andrew Appel, Princeton University, Princeton, NJ, USA
Handledare: Associate Professor Roberto Guanciale, Teoretisk datalogi, TCS; Professor Mads Dam, Teoretisk datalogi, TCS
Abstract
Mjukvara, programmerbarhet och uppkoppling genomsyrar i allt högre grad samhället. Under loppet av en livstid har allt från fordon till telefoner utvecklats från enheter med fast funktion till programmerbara enheter som alltid är uppkopplade. Som följd av detta bestäms deras funktionalitet helt av deras mjukvara, vilken kan förändras med uppdateringar och installering av applikationer. Mjukvaran i sig skrivs i allt högre grad av utkontrakterade konsulter eller till och med av AI, med sårbarheter som dyker upp och åtgärdas dagligen.
Hur kan man ens påbörja att säkra modern digital utrustning? De högsta nivåerna av säkerhetscertifiering kräver formell verifiering - matematiska bevis som utesluter sårbarheter baserat på modeller av hårdvara eller semantik för programmeringsspråk. Detta är kostsamt och tidskrävande, och tillämpas därför främst på små, kritiska komponenter. Vägen till skalbarhet går genom att basera sina assuransutlåtanden på högautomatiserade verifieringsverktyg vars korrekthet endast beror på minimala, granskningsbara betrodda kodbaser.
Arbetet i denna avhandling fokuserar på skapandet av formella verifieringsverktyg inom domänerna maskinkod och nätverk. Den gemensamma nämnaren är användningen av en interaktiv teorembevisare för att säkerställa resultatens tillförlitlighet. Specifikt presenterar avhandlingen (i) metoder för att dela upp verifieringsuppgifter för ostrukturerade program, särskilt tillämpat på maskinkod, och (ii) en formell modell av det domänspecifika språket P4 för nätverk, tillsammans med (iii) ett bevisproducerande exekveringsverktyg och slutligen (iv) en komplett verktygskedja för att verifierbart kompilera ett verifierat P4-program ner till en mjukvaruswitch.