More Web Proxy on the site http://driver.im/

research-article

Open access

Petr4: formal foundations for p4 data planes

Authors:

Mina Tahmasbi Arashloo,

Santiago Bautista,

Alexander Chang,

Samwise Parkinson,

Alaia Solko-Breslin,

Nate FosterAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 5, Issue POPL

Article No.: 41, Pages 1 - 32

https://doi.org/10.1145/3434322

Published: 04 January 2021 Publication History

Abstract

P4 is a domain-specific language for programming and specifying packet-processing systems. It is based on an elegant design with high-level abstractions like parsers and match-action pipelines that can be compiled to efficient implementations in software or hardware. Unfortunately, like many industrial languages, P4 has developed without a formal foundation. The P4 Language Specification is a 160-page document with a mixture of informal prose, graphical diagrams, and pseudocode, leaving many aspects of the language semantics up to individual compilation targets. The P4 reference implementation is a complex system, running to over 40KLoC of C++ code, with support for only a few targets. Clearly neither of these artifacts is suitable for formal reasoning about P4 in general.

This paper presents a new framework, called Petr4, that puts P4 on a solid foundation. Petr4 consists of a clean-slate definitional interpreter and a core calculus that models a fragment of P4. Petr4 is not tied to any particular target: the interpreter is parameterized over an interface that collects features delegated to targets in one place, while the core calculus overapproximates target-specific behaviors using non-determinism.

We have validated the interpreter against a suite of over 750 tests from the P4 reference implementation, exercising our target interface with tests for different targets. We validated the core calculus with a proof of type-preserving termination. While developing Petr4, we reported dozens of bugs in the language specification and the reference implementation, many of which have been fixed.

References

[1]

Carolyn Jane Anderson, Nate Foster, Arjun Guha, Jean-Baptiste Jeannin, Dexter Kozen, Cole Schlesinger, and David Walker. 2014. NetKAT: Semantic Foundations for Networks. In ACM POPL. 113-126. https://doi.org/10.1145/2535838.2535862

Digital Library

[2]

Ryan Becket, Aarti Gupta, Ratul Mahajan, and David Walker. 2017. A General Approach to Network Configuration Verification. In SIGCOMM. 155-168. https://doi.org/10.1145/3098822.3098834

Digital Library

[3]

Steve Bishop, Matthew Fairbairn, Hannes Mehnert, Michael Norrish, Tom Ridge, Peter Sewell, Michael Smith, and Keith Wansbrough. 2018. Engineering with Logic: Rigorous Test-Oracle Specification and Validation for TCP/IP and the Sockets API. JACM 66, 1 (Dec. 2018 ), 1 : 1-1 : 77. https://doi.org/10.1145/3243650

Digital Library

[4]

Nikolaj Bjorner and Karthick Jayaraman. 2015. Checking Cloud Contracts in Microsoft Azure. In ICDCIT. Springer-Verlag, 21-32. https://doi.org/10.1007/978-3-319-14977-6_2

Digital Library

[5]

Pat Bosshart, Dan Daly, Glen Gibb, Martin Izzard, Nick McKeown, Jennifer Rexford, Cole Schlesinger, Dan Talayco, Amin Vahdat, George Varghese, and David Walker. 2014. P4: Programming Protocol-Independent Packet Processors. SIGCOMM CCR 44, 3 ( July 2014 ), 87-95. https://doi.org/10.1145/2656877.2656890

Digital Library

[6]

Cisco Systems. 2018. Cisco DNA Analytics and Assurance. Available at https://www.cisco.com/c/en/us/solutions/enterprisenetworks/dna-analytics-assurance.html.

[7]

Luis Damas. 1984. Type Assignment in Programming Languages. Ph.D. Dissertation. University of Edinburgh. Available at http://hdl.handle.net/ 1842 /13555.

[8]

Catherine Dodge and Stephen Quigg. 2018. A Simpler Way to Assess the Network Exposure of EC2 Instances: AWS Releases New Network Reachability Assessments in Amazon Inspector. Archived at https://web.archive.org/web/https://aws.amazon.com/blogs/security/amazon-inspector-assess-network-exposureec2-instances-aws-network-reachability-assessments/.

[9]

Ryan Doenges, Mina Tahmasbi Arashloo, Santiago Bautista, Alexander Chang, Newton Ni, Samwise Parkinson, Rudy Peterson, Alaia Solko-Breslin, Amanda Xu, and Nate Foster. 2020. Petr4: Formal Foundations for P4 Data Planes. arXiv: 2011. 05948 [cs.PL]

[10]

A. Fogel, S. Fung, L. Pedrosa, M. Walraed-Sullivan, R. Govindan, R. Mahajan, and T. Millstein. 2015. A General Approach to Network Configuration Analysis. In NSDI. 469-483.

[11]

Nate Foster. 2019. Type error due to inference/substitution? Github bug report. Archived at https://web.archive.org/web/https: //github.com/p4lang/p4c/issues/ 2036.

[12]

Jacob Van Gefen, Luke Nelson, Isil Dillig, Xi Wang, and Emina Torlak. 2020. Synthesizing JIT Compilers for In-Kernel DSLs. In CAV. https://doi.org/10.1007/978-3-030-53291-8_29

[13]

Aaron Gember-Jacobson, Raajay Viswanathan, Aditya Akella, and Ratul Mahajan. 2016. Fast Control Plane Analysis Using an Abstract Representation. In SIGCOMM. 300-313. https://doi.org/10.1145/2934872.2934876

Digital Library

[14]

Michael Greenberg and Austin J. Blatt. 2020. Executable Formal Semantics for the POSIX Shell. In POPL. https://doi.org/10. 1145/3371111

Digital Library

[15]

Arjun Guha, Mark Reitblatt, and Nate Foster. 2013. Machine-Verified Network Controllers. In PLDI. 483-494.

[16]

Arjun Guha, Claudiu Saftoiu, and Shriram Krishnamurthi. 2010. The Essence of JavaScript. In ECOOP. https://doi.org/10. 1007/978-3-642-14107-2_7

[17]

Andreas Haas, Andreas Rossberg, Derek L. Schuf, Ben L. Titzer, Michael Holman, Dan Gohman, Luke Wagner, Alon Zakai, and JF Bastien. 2017. Bringing the Web up to Speed with WebAssembly. In PLDI. 185-200. https://doi.org/10.1145/ 3062341.3062363

Digital Library

[18]

Stefan Heule, Konstantin Weitz, Waqar Mohsin, Lorenzo Vicisano, and Amin Vahdat. 2019. Leveraging P4 to Automatically Validate Networking Switches. Presentation at ONF Connect. Slides available at https://www.opennetworking.org/wpcontent/uploads/2019/09/2.30pm-Stefan-Heule-P4-Presentation.pdf.

[19]

Mukesh Hira and LJ Wobker. 2015. Improving Network Monitoring and Management with Programmable Data Planes. P4 Language Consortium Blog. Available at https://p4.org/p4/inband-network-telemetry/.

[20]

Xin Jin, Xiaozhou Li, Haoyu Zhang, Nate Foster, Jeongkeun Lee, Robert Soulé, Changhoon Kim, and Ion Stoica. 2018. NetChain: Scale-Free Sub-RTT Coordination. In NSDI. 35-49. https://www.usenix.org/conference/nsdi18/presentation/jin

[21]

Xin Jin, Xiaozhou Li, Haoyu Zhang, Robert Soulé, Jeongkeun Lee, Nate Foster, Changhoon Kim, and Ion Stoica. 2017. NetCache: Balancing Key-Value Stores with Fast In-Network Caching. In SOSP. 121-136. https://doi.org/10.1145/3132747. 3132764

Digital Library

[22]

Jacques-Henri Jourdan and François Pottier. 2017. A Simple, Possibly Correct LR Parser for C11. ACM Transactions on Programming Languages and Systems (TOPLAS) 39, 4 ( 2017 ), 1-36. https://doi.org/10.1145/3064848

Digital Library

[23]

Gilles Kahn. 1987. Natural Semantics. In Symposium on Theoretical Aspects of Computer Science (STACS). Springer-Verlag, 22-39. https://doi.org/10.1007/BFb0039592

[24]

Peyman Kazemian, George Varghese, and Nick McKeown. 2012. Header Space Analysis: Static Checking for Networks. In NSDI. 113-126. https://www.usenix.org/conference/nsdi12/technical-sessions/presentation/kazemian

[25]

Ali Kheradmand and Grigore Rosu. 2018. P4K: A Formal Semantics of P4 and Applications. ( 2018 ). arXiv: 1804. 01468 [cs.NI]

[26]

Xavier Leroy. 2009. Formal Verification of a Realistic Compiler. Commun. ACM 52, 7 ( 2009 ), 107-115.

[27]

Hongqiang Harry Liu, Yibo Zhu, Jitu Padhye, Jiaxin Cao, Sri Tallapragada, Nuno P. Lopes, Andrey Rybalchenko, Guohan Lu, and Lihua Yuan. 2017. CrystalNet: Faithfully Emulating Large Production Networks. In SOSP. 599-613. https: //doi.org/10.1145/3132747.3132759

Digital Library

[28]

Jed Liu, William Hallahan, Cole Schlesinger, Milad Sharif, Jeongkeun Lee, Robert Soulé, Han Wang, Călin Caşcaval, Nick McKeown, and Nate Foster. 2018. p4v: Practical Verification for Programmable Data Planes. In ACM SIGCOMM. 490-503. https://doi.org/10.1145/3230543.3230582

Digital Library

[29]

Haohui Mai, Ahmed Khurshid, Rachit Agarwal, Matthew Caesar, P. Brighten Godfrey, and Samuel Talmadge King. 2011. Debugging the Data Plane with Anteater. In SIGCOMM. 290-301. https://doi.org/10.1145/2018436.2018470

Digital Library

[30]

Nick McKeown, Dan Talayco, George Varghese, Nuno Lopes, Nikolaj Bjørner, and Andrey Rybalchenko. 2016. Automatically Verifying Reachability and Well-Formedness in P4 Networks. Technical Report MSR-TR-2016-65. https://www.microsoft. com/en-us/research/wp-content/uploads/2016/09/p4nod.pdf

[31]

Robin Milner, Mads Tofte, and David Macqueen. 1997. The Definition of Standard ML. MIT Press, Cambridge, MA, USA.

Digital Library

[32]

Andres Nötzli, Jehandad Khan, Andy Fingerhut, Clark Barrett, and Peter Athanas. 2018. p4pktgen: Automated Test Case Generation for P4 Programs. In ACM SOSR. 5 : 1-5 :7. https://doi.org/10.1145/3185467.3185497

Digital Library

[33]

Daejun Park, Andrei Ştefănescu, and Grigore Roşu. 2015. KJS: A Complete Formal Semantics of JavaScript. In PLDI. 346-356. https://doi.org/10.1145/2737924.2737991

Digital Library

[34]

Benjamin C. Pierce and David N. Turner. 2000. Local Type Inference. ACM Transactions on Programming Languages and Systems (TOPLAS) 22, 1 (Jan. 2000 ), 1-44. https://doi.org/10.1145/345099.345100

Digital Library

[35]

Gordon D Plotkin. 1981. A Structural Approach to Operational Semantics. ( 1981 ).

[36]

Fabian Rufy, Tao Wang, and Anirudh Sivaraman. 2020. Gauntlet: Finding Bugs in Compilers for Programmable Packet Processing. In OSDI. https://www.usenix.org/conference/osdi20/presentation/rufy

[37]

Dana Scott and Christopher Strachey. 1971. Toward a Mathematical Semantics for Computer Languages. Vol. 1. Oxford University Computing Laboratory, Programming Research Group Oxford.

[38]

Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa Nardelli, and Magnus O Myreen. 2010a. x86-TSO: a Rigorous and Usable Programmer's Model for x86 Multiprocessors. Commun. ACM 53, 7 ( 2010 ), 89-97. https://doi.org/10.1145/ 1785414.1785443

Digital Library

[39]

Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar, and Rok Strniša. 2010b. Ott: Efective Tool Support for the Working Semanticist. J. Funct. Program. 20, 1 (Jan. 2010 ), 71-122. https: //doi.org/10.1017/S0956796809990293

Digital Library

[40]

Christian Skalka, John Ring, David Darias, Minseok Kwon, Sahil Gupta, Kyle Diller, Stefen Smolka, and Nate Foster. 2019. Proof Carrying Network Code. In ACM CCS. 1115-1129. https://doi.org/10.1145/3319535.3363214

Digital Library

[41]

Radu Stoenescu, Dragos Dumitrescu, Matei Popovici, Lorina Negreanu, and Costin Raiciu. 2018. Debugging P4 programs with Vera. In SIGCOMM. https://doi.org/10.1145/3230543.3230548

Digital Library

[42]

Aldo Svaldi. 2019. A Single Network Card Caused CenturyLink's Nationwide Outage. The Denver Post. Archived at https://web.archive.org/web/20190202225936/https://www.denverpost.com/ 2019 /01/11/centurylink-network-outagedenver/.

[43]

The P4 Language Consortium. 2018. P4 Language Specification, Version 1.1.0. Available at https://p4.org/p4-spec/docs/P4-16-v1.1.0-spec.html.

[44]

Xi Wang, Haogang Chen, Alvin Cheung, Zhihao Jia, Nickolai Zeldovich, and M. Frans Kaashoek. 2012. Undefined Behavior: What Happened to My Code?. In Proceedings of the Asia-Pacific Workshop on Systems. 1-7. https://doi.org/10.1145/ 2349896.2349905

Digital Library

[45]

Xi Wang, David Lazar, Nickolai Zeldovich, Adam Chlipala, and Zachary Tatlock. 2014. Jitk: A Trustworthy In-Kernel Interpreter Infrastructure. In OSDI. 33-47. https://www.usenix.org/conference/osdi14/technical-sessions/presentation/ wang_xi

Cited By

Alshnakat ALundberg DGuanciale RDam M(2024)HOL4P4: Mechanized Small-Step Semantics for P4Proceedings of the ACM on Programming Languages10.1145/36498198:OOPSLA1(223-249)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649819
Larsen JGuanciale RHaller PScalas A(2023)P4R-Type: A Verified API for P4 Control Plane ProgramsProceedings of the ACM on Programming Languages10.1145/36228667:OOPSLA2(1935-1963)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622866
Ye CHe FChandra SBlincoe KTonella P(2023)P4b: A Translator from P4 Programs to BoogieProceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3611643.3613091(2172-2176)Online publication date: 30-Nov-2023
https://dl.acm.org/doi/10.1145/3611643.3613091
Show More Cited By

Index Terms

Petr4: formal foundations for p4 data planes
1. Networks
  1. Network architectures
    1. Programming interfaces
2. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions

Recommendations

The P4->NetFPGA Workflow for Line-Rate Packet Processing
FPGA '19: Proceedings of the 2019 ACM/SIGDA International Symposium on Field-Programmable Gate Arrays

P4 has emerged as the de facto standard language for describing how network packets should be processed, and is becoming widely used by network owners, systems developers, researchers and in the classroom. The goal of the work presented here is to make ...
P4-To-VHDL

Automatic generation of parser and deparser blocks capable to process traffic at speed of 100Gbps.Protocol independent (can be used not only in computer networks).Easy implementation of the final application because both modules (parser and deparser) ...
Hardware-Accelerated Cryptography for Software-Defined Networks with P4
Innovative Security Solutions for Information Technology and Communications
Abstract
The paper presents a hardware-accelerated cryptographic solution for Field Programmable Gate Array (FPGA) based network cards that provide throughput up to 200 Gpbs. Our solution employs a Software-Defined Network (SDN) concept based on the high-...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 5, Issue POPL

January 2021

1789 pages

EISSN:2475-1421

DOI:10.1145/3445980

Issue’s Table of Contents

Copyright © 2021 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 04 January 2021

Published in PACMPL Volume 5, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

12
Total Citations
View Citations
1,644
Total Downloads

Downloads (Last 12 months)362
Downloads (Last 6 weeks)42

Reflects downloads up to 05 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Alshnakat ALundberg DGuanciale RDam M(2024)HOL4P4: Mechanized Small-Step Semantics for P4Proceedings of the ACM on Programming Languages10.1145/36498198:OOPSLA1(223-249)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649819
Larsen JGuanciale RHaller PScalas A(2023)P4R-Type: A Verified API for P4 Control Plane ProgramsProceedings of the ACM on Programming Languages10.1145/36228667:OOPSLA2(1935-1963)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622866
Ye CHe FChandra SBlincoe KTonella P(2023)P4b: A Translator from P4 Programs to BoogieProceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3611643.3613091(2172-2176)Online publication date: 30-Nov-2023
https://dl.acm.org/doi/10.1145/3611643.3613091
Ruffy FLiu JKotikalapudi PHavel VTavante HSherwood RDubina VPeschanenko VSivaraman AFoster NSchulzrinne HKohler EMaltz DMisra V(2023)P4Testgen: An Extensible Test Oracle For P4-16Proceedings of the ACM SIGCOMM 2023 Conference10.1145/3603269.3604834(136-151)Online publication date: 10-Sep-2023
https://dl.acm.org/doi/10.1145/3603269.3604834
Lin JNarayanan VIkarashi YRagan-Kelley JBernstein GMccann J(2023)Semantics and Scheduling for Machine Knitting CompilersACM Transactions on Graphics10.1145/359244942:4(1-26)Online publication date: 26-Jul-2023
https://dl.acm.org/doi/10.1145/3592449
Peterson RCampbell EChen JIsak NShyu CDoenges RAtaei PFoster NKrebbers RTraytel DPientka BZdancewic S(2023)P4Cub: A Little Language for Big RoutersProceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3573105.3575670(303-319)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3573105.3575670
Györgyi CLaki SSchmid S(2023)Toward Highly Reliable Programmable Data Planes: Verification of P4 Code Generation2023 IEEE 9th International Conference on Network Softwarization (NetSoft)10.1109/NetSoft57336.2023.10175397(1-5)Online publication date: 19-Jun-2023
https://doi.org/10.1109/NetSoft57336.2023.10175397
Alshnakat ALundberg DGuanciale RDam MPalmskog KChiesa MFeibish S(2022)HOL4P4Proceedings of the 5th International Workshop on P4 in Europe10.1145/3565475.3569081(39-45)Online publication date: 9-Dec-2022
https://dl.acm.org/doi/10.1145/3565475.3569081
Grewal KD'Antoni LHsu JJhala RDillig I(2022)P4BID: information flow control in p4Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523717(46-60)Online publication date: 9-Jun-2022
https://dl.acm.org/doi/10.1145/3519939.3523717
Houshmand FSaberlatibari JLesani MJhala RDillig I(2022)Hamband: RDMA replicated data typesProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523426(348-363)Online publication date: 9-Jun-2022
https://dl.acm.org/doi/10.1145/3519939.3523426
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents