HOL4P4: Mechanized Small-Step Semantics for P4
Article No.: 102, Pages 223 - 249
Abstract
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.
References
[1]
Anoud Alshnakat, Didrik Lundberg, Roberto Guanciale, Mads Dam, Karl Palmskog, and Arve Gengelbach. 2024. HOL4P4. https://doi.org/10.5281/zenodo.10796440
[2]
Anoud Alshnakat, Didrik Lundberg, Roberto Guanciale, Mads Dam, Karl Palmskog, and Arve Gengelbach. 2024. HOL4P4. https://github.com/kth-step/HOL4P4/releases/tag/OOPSLA2024
[3]
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. ACM SIGCOMM Computer Communication Review, 44, 3 (2014), 87–95. https://doi.org/10.1145/2656877.2656890
[4]
The P4 Language Consortium. 2023. P4subscript 16 Language Specification. https://p4.org/p4-spec/docs/P4-16-v1.2.4.html
[5]
Pierre Courtieu, Maria Virginia Aponte, Tristan Crolard, Zhi Zhang, Fnu Robby, Jason Belt, John Hatcliff, Jerome Guitton, and Trevor Jennings. 2013. Towards The Formalization of SPARK 2014 Semantics With Explicit Run-time Checks Using Coq. In Proceedings of the 2013 ACM SIGAda Annual Conference on High Integrity Language Technology (HILT ’13, Vol. 33). 21–22. https://doi.org/10.1145/2658982.2527278
[6]
Ryan Doenges, Mina Tahmasbi Arashloo, Santiago Bautista, Alexander Chang, Newton Ni, Samwise Parkinson, Rudy Peterson, Alaia Solko-Breslin, Amanda Xu, and Nate Foster. 2021. Petr4: Formal Foundations for P4 Data Planes. In Proceedings of the ACM on Programming Languages. 5, Article 41, https://doi.org/10.1145/3434322
[7]
Ryan Doenges, Tobias Kappé, John Sarracino, Nate Foster, and Greg Morrisett. 2022. Leapfrog: Certified Equivalence for Protocol Parsers. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI 2022). 950–965. https://doi.org/10.1145/3519939.3523715
[8]
Claire Dross and Johannes Kanig. 2020. Recursive Data Structures in SPARK. In Computer Aided Verification (CAV 2020). 178–189. https://doi.org/10.1007/978-3-030-53291-8_11
[9]
Matthias Eichholz, Eric Campbell, Nate Foster, Guido Salvaneschi, and Mira Mezini. 2019. How to Avoid Making a Billion-Dollar Mistake: Type-Safe Data Plane Programming with SafeP4. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). https://doi.org/10.4230/LIPIcs.ECOOP.2019.12
[10]
Matthias Eichholz, Eric Hayden Campbell, Matthias Krebs, Nate Foster, and Mira Mezini. 2022. Dependently-Typed Data Plane Programming. In Proceedings of the ACM on Programming Languages. 6, ACM New York, NY, USA, 1–28. https://doi.org/10.1145/3498701
[11]
Lucas Freire, Miguel Neves, Lucas Leal, Kirill Levchenko, Alberto Schaeffer-Filho, and Marinho Barcellos. 2018. Uncovering Bugs in P4 Programs with Assertion-based Verification. In Proceedings of the Symposium on SDN Research (SOSR ’18). Article 4, https://doi.org/10.1145/3185467.3185499
[12]
Karuna Grewal, Loris D’Antoni, and Justin Hsu. 2022. P4BID: Information Flow Control in P4. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI 2022). 46–60. https://doi.org/10.1145/3519939.3523717
[13]
The P4.org Architecture Working Group. 2018. P4subscript 16 Portable Switch Architecture (PSA). https://p4.org/p4-spec/docs/PSA-v1.1.0.html
[14]
Georges-Axel Jaloyan, Claire Dross, Maroua Maalej, Yannick Moy, and Andrei Paskevich. 2020. Verification of Programs with Pointers in SPARK. In Formal Methods and Software Engineering. 55–72. https://doi.org/10.1007/978-3-030-63406-3_4
[15]
Ali Kheradmand and Grigore Rosu. 2018. P4K: A Formal Semantics of P4 and Applications. arXiv preprint, https://doi.org/10.48550/arXiv.1804.01468
[16]
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 Proceedings of the 2018 Conference of the ACM Special Interest Group on Data Communication (SIGCOMM ’18). 490–503. https://doi.org/10.1145/3230543.3230582
[17]
Nuno Lopes, Nikolaj Bjørner, Nick McKeown, Andrey Rybalchenko, Dan Talayco, and George Varghese. 2016. Automatically verifying reachability and well-formedness in P4 Networks. Technical Report, https://www.microsoft.com/en-us/research/publication/automatically-verifying-reachability-well-formedness-p4-networks/
[18]
Maroua Maalej, Tucker Taft, and Yannick Moy. 2018. Safe Dynamic Memory Management in Ada and SPARK. In Reliable Software Technologies – Ada-Europe 2018. 37–52. https://doi.org/10.1007/978-3-319-92432-8_3
[19]
William Marsh and IM O’Neill. 1994. Formal semantics of SPARK. Program Validation Ltd
[20]
Andres Nötzli, Jehandad Khan, Andy Fingerhut, Clark Barrett, and Peter Athanas. 2018. p4pktgen: Automated Test Case Generation for P4 Programs. In Proceedings of the Symposium on SDN Research (SOSR ’18). Article 5, https://doi.org/10.1145/3185467.3185497
[21]
p4c contributors. 2021. P4-16 declaration of the P4 v1.0 switch model. https://github.com/p4lang/p4c/blob/main/p4include/v1model.p4
[22]
Rudy Peterson, Eric Hayden Campbell, John Chen, Natalie Isak, Calvin Shyu, Ryan Doenges, Parisa Ataei, and Nate Foster. 2023. P4Cub: A Little Language for Big Routers. In Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2023). 303–319. https://doi.org/10.1145/3573105.3575670
[23]
Fabian Ruffy, Jed Liu, Prathima Kotikalapudi, Vojtech Havel, Hanneli Tavante, Rob Sherwood, Vladyslav Dubina, Volodymyr Peschanenko, Anirudh Sivaraman, and Nate Foster. 2023. P4Testgen: An Extensible Test Oracle For P4-16. In Proceedings of the ACM SIGCOMM 2023 Conference. 136–151. https://doi.org/10.1145/3603269.3604834
[24]
Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar, and Rok Strnisa. 2010. Ott: Effective tool support for the working semanticist. Journal of Functional Programming, 20, 1 (2010), 71–122. https://doi.org/10.1017/S0956796809990293
[25]
Apoorv Shukla, Seifeddine Fathalli, Thomas Zinner, Artur Hecker, and Stefan Schmid. 2020. P4Consist: Toward Consistent P4 SDNs. IEEE Journal on Selected Areas in Communications, 38, 7 (2020), 1293–1307. https://doi.org/10.1109/JSAC.2020.2999653
[26]
Radu Stoenescu, Matei Popovici, Lorina Negreanu, and Costin Raiciu. 2016. SymNet: Scalable symbolic execution for modern networks. In Proceedings of the 2016 ACM SIGCOMM Conference (SIGCOMM ’16). 314–327. https://doi.org/10.1145/2934872.2934881
[27]
Bingchuan Tian, Jiaqi Gao, Mengqi Liu, Ennan Zhai, Yanqing Chen, Yu Zhou, Li Dai, Feng Yan, Mengjing Ma, Ming Tang, Jie Lu, Xionglie Wei, Hongqiang Harry Liu, Ming Zhang, Chen Tian, and Minlan Yu. 2021. Aquila: A Practically Usable Verification System for Production-Scale Programmable Data Planes. In Proceedings of the 2021 ACM SIGCOMM 2021 Conference (SIGCOMM ’21). 17–32. https://doi.org/10.1145/3452296.3472937
[28]
Qinshi Wang, Mengying Pan, Shengyi Wang, Ryan Doenges, Lennart Beringer, and Andrew W. Appel. 2023. Foundational Verification of Stateful P4 Packet Processing. In 14th International Conference on Interactive Theorem Proving (ITP 2023). 268, 32:1–32:20. https://doi.org/10.4230/LIPIcs.ITP.2023.32
[29]
Nofel Yaseen, Liangcheng Yu, Caleb Stanford, Ryan Beckett, and Vincent Liu. 2022. FP4: Line-rate Greybox Fuzz Testing for P4 Switches. arXiv preprint, https://doi.org/10.48550/arXiv.2207.13147
[30]
Zhi Zhang, Robby, John Hatcliff, Yannick Moy, and Pierre Courtieu. 2017. Focused Certification of an Industrial Compilation and Static Verification Toolchain. In Software Engineering and Formal Methods. 17–34. https://doi.org/10.1007/978-3-319-66197-1_2
Index Terms
- HOL4P4: Mechanized Small-Step Semantics for P4
Recommendations
HOL4P4: semantics for a verified data plane
EuroP4 '22: Proceedings of the 5th International Workshop on P4 in EuropeWe 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 ...
Deriving Pretty-Big-Step Semantics from Small-Step Semantics
Proceedings of the 23rd European Symposium on Programming Languages and Systems - Volume 8410Big-step semantics for languages with abrupt termination and/or divergence suffer from a serious duplication problem, addressed by the novel 'pretty-big-step' style presented by Charguéraud at ESOP'13. Such rules are less concise than corresponding ...
Equivalence of formal semantics definition methods
AbstractThere are numerous methods of formally defining the semantics of computer languages. Each method has been designed to fulfil a different purpose. For example, some have been designed to make reasoning about languages as easy as possible; others ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
April 2024
1492 pages
Copyright © 2024 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: 29 April 2024
Published in PACMPL Volume 8, Issue OOPSLA1
Check for updates
Badges
Author Tags
Qualifiers
- Research-article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 323Total Downloads
- Downloads (Last 12 months)323
- Downloads (Last 6 weeks)69
Reflects downloads up to 18 Nov 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in