TU Darmstadt / ULB / TUprints

Type-Safe Data Plane Programming

Eichholz, Matthias (2022)
Type-Safe Data Plane Programming.
Technische Universität Darmstadt
doi: 10.26083/tuprints-00022873
Ph.D. Thesis, Primary publication, Publisher's Version

[img] Text
eichholz-dissertation.pdf
Copyright Information: CC BY-SA 4.0 International - Creative Commons, Attribution ShareAlike.

Download (4MB)
Item Type: Ph.D. Thesis
Type of entry: Primary publication
Title: Type-Safe Data Plane Programming
Language: English
Referees: Mezini, Prof. Dr. Mira ; Foster, Prof. Nate
Date: 2022
Place of Publication: Darmstadt
Collation: vii, 227 Seiten
Date of oral examination: 12 October 2022
DOI: 10.26083/tuprints-00022873
Abstract:

Since the mid-1990s, there have been efforts to enable more flexible processing of network packets by making packet processing programmable. With the advent of software-defined networking (SDN), this idea has now become a reality. Early approaches initially focused on control plane programming, with the goal of implementing centralized network policies at a high level of abstraction without having to use low-level, device-specific configuration mechanisms. For this purpose, various network programming languages have been developed, which provide correctness guarantees and make the formal verification of network policies possible. More recently, it is also possible to program the network data plane. Being able to define the structure of network packet headers freely, opens up a whole new range of applications, from implementing new network protocols up to moving application logic directly into the network. Until today, the P4 language has become the de facto standard for programming data planes. While P4 provides declarative abstractions for programming data planes, P4 lacks basic safety guarantees to help avoid errors and implement correct applications for the data plane. Modern programming languages use static type systems to provide languages with basic safety guarantees that completely eliminate the occurrence of entire categories of errors. Surprisingly, however, the use of type systems in the field of network programming has hardly been investigated. This dissertation investigates what appropriate type systems must look like in order to provide data plane programming languages—in particular, P4—with static correctness guarantees. As a first step, we present SafeP4, a domain-specific language for programmable data planes that is equipped with a static type system that guarantees that all headers that are read or written are valid, which is a common cause of errors. We then present Π4, whose type system is based on dependent types and is thus able to bridge the gap in terms of expressiveness between SafeP4 and full-fledged verification tools. At the same time, Π4 enables modular verification of programs. Our evaluation using open source programs confirms that accessing invalid packet headers is a common source of errors in practice and that the SafeP4’s type system is capable of identifying buggy programs. Using case studies, we show that Π4’s type system is capable of expressing and verifying a variety of real-world correctness properties.

Alternative Abstract:
Alternative AbstractLanguage

Seit Mitte der 1990er Jahre gibt es Bestrebungen, eine flexiblere Verarbeitung von Netzwerkpaketen zu ermöglichen, indem Paketverarbeitung programmierbar wird. Mit dem Aufkommen von Software-Defined-Networking (SDN) ist diese Idee nun Realität geworden. Frühe Ansätze haben sich zunächst auf die Programmierung der Control-Plane konzentriert, mit dem Ziel, auf hohem Abstraktionsniveau zentrale Netzwerkrichtlinien zu realisieren, ohne systemnahe, gerätespezifische Konfigurationsmechanismen nutzen zu müssen. Hierfür entstanden diverse Programmiersprachen, die Korrektheitsgarantien gewähren und die formale Verifikation der Netzwerkrichtlinien ermöglichen. In jüngster Zeit ist es zudem auch möglich die Netzwerk-Data-Plane zu programmieren. Durch die Möglichkeit die Struktur von Netzwerkpaketheadern frei zu definieren, eröffnen sich eine Vielzahl neuer Anwendungsmöglichkeiten, von der Implementierung neuartiger Netzwerkprotokolle bis hin zur Auslagerung von Anwendungsfunktionalität direkt in das Netzwerk. Bis heute hat sich die Sprache P4 als Standard für die Programmierung von Data-Planes durchgesetzt. Zwar bietet P4 deklarative Abstraktionen für die Programmierung von Data-Planes, allerdings fehlen P4 grundlegende Sicherheitsgarantien, die dabei helfen Fehler zu vermeiden und korrekte Anwendungen für die Data-Plane zu implementieren. Modernen Programmiersprachen nutzen statische Typsysteme, um Sprachen mit grundlegenden Sicherheitsgarantien auszustatten, die das Auftreten ganzer Fehlerkategorien vollständig ausschließen. Überraschenderweise wurde der Einsatz von Typsysteme im Bereich der Netzwerkprogrammierung jedoch bislang kaum untersucht. Diese Dissertation untersucht wie geeignete Typsysteme aussehen müssen, um Data-Plane-Programmiersprachen – insbesondere P4 – mit statischen Korrektheitsgarantien auszustatten. Im ersten Schritt präsentieren wir SafeP4, eine domänenspezifische Sprache für programmierbare Data-Planes, die mit einem statischen Typsystem ausgestattet ist, das garantiert, dass alle Header, die gelesen oder geschrieben werden gültig sind, was eine häufige Ursache für Fehler ist. Im zweiten Schritt präsentieren wir Π4, dessen Typsystem auf Dependent-Types basiert und damit in der Lage ist, die Lücke hinsichtlich der Ausdrucksstärke zwischen SafeP4 und vollwertigen Verifikationswerkzeugen zu schließen. Gleichzeitig ermöglicht Π4 die modulare Verifikation von Programmen. Unsere Auswertung anhand von Open-Source-Programmen bestätigt, dass der Zugriff auf ungültige Paketheader in der Praxis eine häufige Fehlerquelle ist und das SafeP4s Typsystem in der Lage ist, fehlerhafte Programme zu identifizieren. Anhand von Fallstudien zeigen wir zudem, dass Π4s Typsystem imstande ist eine Vielzahl praktisch relevanter Korrektheitseigenschaften auszudrücken und zu verifizieren.

German
Status: Publisher's Version
URN: urn:nbn:de:tuda-tuprints-228736
Classification DDC: 000 Generalities, computers, information > 004 Computer science
Divisions: 20 Department of Computer Science > Software Technology
Date Deposited: 08 Dec 2022 13:46
Last Modified: 12 Dec 2022 08:52
URI: https://tuprints.ulb.tu-darmstadt.de/id/eprint/22873
PPN: 502472901
Export:
Actions (login required)
View Item View Item