Software, programmability and connectivity are increasingly pervasive aspects of society. In the span of a lifetime, everything from vehicles to phones has evolved from fixed-function to generally programmable devices that are always online. As a result, their functionality is entirely determined by their software, which may change from update to update and depending on what applications you have installed. The software itself is increasingly written by outsourced consultants or even by AI, with vulnerabilities appearing and being fixed on a daily basis.

Where does one even begin to secure modern digital equipment? The highest levels of assurance certification demand formal verification - mathematical proofs that rule out vulnerabilities based on models of hardware or programming-language semantics. This is costly and time-consuming, and so is applied mainly to small, critical components. The way to gain scalability is to base your assurance statements on highly automated verification tools whose correctness depends only on minimal, auditable trusted code bases.

The work in this thesis is focused on the creation of formal verification tools in the domains of machine code and networking. The common denominator is the use of an interactive theorem prover to gain assurance of the results. Specifically, the thesis presents (i) methods to decompose verification tasks for unstructured programs, especially as applied to machine code, and (ii) a formal model of the P4 domain-specific networking language, accompanied by (iii) a proof-producing symbolic execution tool and finally (iv) a complete toolchain to verifiably compile a verified P4 program down to a software switch.

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.