kth.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
P4R-Type: A Verified API for P4 Control Plane Programs
DTU Compute, Technical University of Denmark, Richard Petersens Plads, Bygning 321, Kongens Lyngby, 2800, Denmark.
KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.ORCID iD: 0000-0002-8069-6495
KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.ORCID iD: 0000-0002-2659-5271
DTU Compute, Technical University of Denmark, Richard Petersens Plads, Bygning 321, Kongens Lyngby, 2800, Denmark.
2023 (English)In: Proceedings of the ACM on Programming Languages, E-ISSN 2475-1421, Vol. 7, no OOPSLA2, article id 290Article in journal (Refereed) Published
Abstract [en]

Software-Defined Networking (SDN) significantly simplifies programming, reconfiguring, and optimizing network devices, such as switches and routers. The de facto standard for programming SDN devices is the P4 language. However, the flexibility and power of P4, and SDN more generally, gives rise to important risks. As a number of incidents at major cloud providers have shown, errors in SDN programs can compromise the availability of networks, leaving them in a non-functional state. The focus of this paper are errors in control-plane programs that interact with P4-enabled network devices via the standardized P4Runtime API. For clients of the P4Runtime API it is easy to make mistakes that may lead to catastrophic failures, despite the use of Google's Protocol Buffers as an interface definition language. This paper proposes P4R-Type, a novel verified P4Runtime API for Scala that performs static checks for P4 control plane operations, ruling out mismatches between P4 tables, allowed actions, and action parameters. As a formal foundation of P4R-Type, we present the FP4R calculus and its typing system, which ensure that well-typed programs never get stuck by issuing invalid P4Runtime operations. We evaluate the safety and flexibility of P4R-Type with 3 case studies. To the best of our knowledge, this is the first work that formalises P4Runtime control plane applications, and a typing discipline ensuring the correctness of P4Runtime operations.

Place, publisher, year, edition, pages
Association for Computing Machinery (ACM) , 2023. Vol. 7, no OOPSLA2, article id 290
Keywords [en]
P4, P4Runtime, Semantics, Software-defined networking, Type systems
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:kth:diva-339489DOI: 10.1145/3622866ISI: 001087279100070Scopus ID: 2-s2.0-85175024779OAI: oai:DiVA.org:kth-339489DiVA, id: diva2:1811408
Note

QC 20231113

Available from: 2023-11-13 Created: 2023-11-13 Last updated: 2024-02-29Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records

Guanciale, RobertoHaller, Philipp

Search in DiVA

By author/editor
Guanciale, RobertoHaller, Philipp
By organisation
Theoretical Computer Science, TCS
In the same journal
Proceedings of the ACM on Programming Languages
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 99 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf