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.

We introduce a proof-producing symbolic execution tool for formal verification of P4 programs. The tool has been implemented using the interactive theorem prover HOL4 and results are proved sound with respect to the HOL4P4 formalisation of the P4 language. Most notably, this is a general tool for proving functional correctness that can be applied to entire real-world P4 programs.

We present the first semantics of the network data plane programming language P4 able to adequately capture all key features of P416, the most recent version of P4, including external functions (externs) and concurrency. These features are intimately related since, in P4, extern invocations are the only points at which one execution thread can affect another. Reflecting P4's lack of a general-purpose memory and the presence of multithreading the semantics is given in small-step style and eschews the use of a heap. In addition to the P4 language itself, we provide an architectural level semantics, which allows the composition of P4-programmed blocks, models end-to-end packet processing, and can take into account features such as arbitration and packet recirculation. A corresponding type system is provided with attendant progress, preservation, and type-soundness theorems. Semantics, type system, and meta-theory are formalized in the HOL4 theorem prover. From this formalization, we derive a HOL4 executable semantics that supports verified execution of programs with partially symbolic packets able to validate simple end-to-end program properties.

We introduce a formal semantics of P4 for the HOL4 interactive theorem prover. We exploit properties of the language, like the absence of call by reference and the copy-in/copy-out mechanism, to define a heapless small-step semantics that is abstract enough to simplify verification, but that covers the main aspects of the language: interaction with the architecture via externs, table match, and parsers. Our formalization is written in the Ott metalanguage, which allows us to export definitions to multiple interactive theorem provers. The exported HOL4 semantics allows us to establish machine-checkable proofs regarding the semantics, properties of P4 programs, and soundness of analysis tools.

Enabling Hoare-style reasoning for low-level code is attractive since it opens the way to regain structure and modularity in a domain where structure is essentially absent. The field, however, has not yet arrived at a fully satisfactory solution, in the sense of avoiding restrictions on control flow (important for compiler optimization), controlling access to intermediate program points (important for modularity), and supporting total correctness. Proposals in the literature support some of these properties, but a solution that meets them all is yet to be found. We introduce the novel Hoare-style program logic , which interprets postconditions relative to program points when these are first encountered. The logic can support both partial and total correctness, derive contracts for arbitrary control flow, and allows one to freely choose decomposition strategy during verification while avoiding step-indexed approximations and global invariants. The logic can be instantiated for a variety of concrete instruction set architectures and intermediate languages. The rules of  have been verified in the interactive theorem prover HOL4 and integrated with the toolbox HolBA for semi-automated program verification, making it applicable to the ARMv6 and ARMv8 instruction sets.

Enabling Hoare-style reasoning for low-level code is attractive since it opens the way to regain structure and modularity in a domain where structure is essentially absent. The field, however, has not yet arrived at a fully satisfactory solution, in the sense of avoiding restrictions on control flow (important for compiler optimization), controlling access to intermediate program points (important for modularity), and supporting total correctness. Proposals in the literature support some of these properties, but a solution that meets them all is yet to be found.We introduce the novel Hoare-style program logic L_a, which interprets postconditions relative to program points when these are first encountered. The logic supports both partial and total correctness, derives contracts for arbitrary control flow, and allows one to freely choose decomposition strategy during verification while avoiding step-indexed approximations and global invariants. The logic can be instantiated for a variety of concrete instruction set architectures and intermediate languages. The rules of L_a have been verified in the interactive theorem prover HOL4 and integrated with the toolbox HolBA for semi-automated program verification, which supports the ARMv6, ARMv8 and RISC-V instruction sets.

The emergence of programmable network elements and their usage in critical infrastructure is increasing the demand for formal guarantees of their correctness. This paper presents the first P4 software switch connected by proof to a formal semantics. This is accomplished by adjusting and optimizing the HOL4P4 semantics to create an efficient interpreter that can be compiled using the verified CakeML compiler. We demonstrate practical performance in a set of experiments, achieving several orders of magnitude improvement in throughput over existing semantics-based interpreters, with only small performance penalties compared to the BMv2 reference switch written in C++.