TU Darmstadt / ULB / TUbiblio

Dependently-Typed Data Plane Programming

Eichholz, Matthias ; Campbell, Eric Hayden ; Krebs, Matthias ; Foster, Nate ; Mezini, Mira (2022)
Dependently-Typed Data Plane Programming.
In: Proceedings of the ACM on Programming Languages, 6 (POPL)
doi: 10.1145/3498701
Artikel, Bibliographie

Kurzbeschreibung (Abstract)

Programming languages like P4 enable specifying the behavior of network data planes in software. However, with increasingly powerful and complex applications running in the network, the risk of faults also increases. Hence, there is growing recognition of the need for methods and tools to statically verify the correctness of P4 code, especially as the language lacks basic safety guarantees. Type systems are a lightweight and compositional way to establish program properties, but there is a significant gap between the kinds of properties that can be proved using simple type systems (e.g., SafeP4) and those that can be obtained using full-blown verification tools (e.g., p4v). In this paper, we close this gap by developing Π4, a dependently-typed version of P4 based on decidable refinements. We motivate the design of Π4, prove the soundness of its type system, develop an SMT-based implementation, and present case studies that illustrate its applicability to a variety of data plane programs.

Typ des Eintrags: Artikel
Erschienen: 2022
Autor(en): Eichholz, Matthias ; Campbell, Eric Hayden ; Krebs, Matthias ; Foster, Nate ; Mezini, Mira
Art des Eintrags: Bibliographie
Titel: Dependently-Typed Data Plane Programming
Sprache: Englisch
Publikationsjahr: 12 Januar 2022
Verlag: ACM
Titel der Zeitschrift, Zeitung oder Schriftenreihe: Proceedings of the ACM on Programming Languages
Jahrgang/Volume einer Zeitschrift: 6
(Heft-)Nummer: POPL
DOI: 10.1145/3498701
Kurzbeschreibung (Abstract):

Programming languages like P4 enable specifying the behavior of network data planes in software. However, with increasingly powerful and complex applications running in the network, the risk of faults also increases. Hence, there is growing recognition of the need for methods and tools to statically verify the correctness of P4 code, especially as the language lacks basic safety guarantees. Type systems are a lightweight and compositional way to establish program properties, but there is a significant gap between the kinds of properties that can be proved using simple type systems (e.g., SafeP4) and those that can be obtained using full-blown verification tools (e.g., p4v). In this paper, we close this gap by developing Π4, a dependently-typed version of P4 based on decidable refinements. We motivate the design of Π4, prove the soundness of its type system, develop an SMT-based implementation, and present case studies that illustrate its applicability to a variety of data plane programs.

Freie Schlagworte: P4, Dependent Types, Software-Defined Networking
Zusätzliche Informationen:

Art.No.: 40

Fachbereich(e)/-gebiet(e): 20 Fachbereich Informatik
20 Fachbereich Informatik > Softwaretechnik
DFG-Sonderforschungsbereiche (inkl. Transregio)
DFG-Sonderforschungsbereiche (inkl. Transregio) > Sonderforschungsbereiche
DFG-Sonderforschungsbereiche (inkl. Transregio) > Sonderforschungsbereiche > SFB 1053: MAKI – Multi-Mechanismen-Adaption für das künftige Internet
DFG-Sonderforschungsbereiche (inkl. Transregio) > Sonderforschungsbereiche > SFB 1053: MAKI – Multi-Mechanismen-Adaption für das künftige Internet > A: Konstruktionsmethodik
DFG-Sonderforschungsbereiche (inkl. Transregio) > Sonderforschungsbereiche > SFB 1053: MAKI – Multi-Mechanismen-Adaption für das künftige Internet > A: Konstruktionsmethodik > Teilprojekt A2: Entwurf
Hinterlegungsdatum: 18 Jul 2022 09:23
Letzte Änderung: 06 Dez 2022 13:42
PPN: 50232631X
Export:
Suche nach Titel in: TUfind oder in Google
Frage zum Eintrag Frage zum Eintrag

Optionen (nur für Redakteure)
Redaktionelle Details anzeigen Redaktionelle Details anzeigen