Formal Verification of Software-Defined Network Elements and Machine Code
Time: Mon 2025-12-08 13.00
Location: Kollegiesalen, Brinellvägen 8, Stockholm
Video link: https://kth-se.zoom.us/j/61627100868
Language: English
Subject area: Computer Science
Doctoral student: Didrik Lundberg , Teoretisk datalogi, TCS, Saab AB, Sweden
Opponent: Professor Emeritus Andrew Appel, Princeton University, Princeton, NJ, USA
Supervisor: Associate Professor Roberto Guanciale, Teoretisk datalogi, TCS; Professor Mads Dam, Teoretisk datalogi, TCS
Abstract
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.