Document Open Access Logo

Foundational Verification of Stateful P4 Packet Processing

Authors Qinshi Wang , Mengying Pan , Shengyi Wang , Ryan Doenges , Lennart Beringer , Andrew W. Appel

PDF
Thumbnail PDF

File

LIPIcs.ITP.2023.32.pdf
  • Filesize: 0.86 MB
  • 20 pages

Document Identifiers

Author Details

Qinshi Wang
  • Princeton University, NJ, USA
Mengying Pan
  • Princeton University, NJ, USA
Shengyi Wang
  • Princeton University, NJ, USA
Ryan Doenges
  • Cornell University, Ithaca, NY, USA
Lennart Beringer
  • Princeton University, NJ, USA
Andrew W. Appel
  • Princeton University, NJ, USA

Funding

This material is based upon work supported by DARPA Contracts HR001120C0160 and HR001120C0107, and by NSF grant FMiTF-1918396.

Cite As Get BibTex

Qinshi Wang, Mengying Pan, Shengyi Wang, Ryan Doenges, Lennart Beringer, and Andrew W. Appel. Foundational Verification of Stateful P4 Packet Processing. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 32:1-32:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.ITP.2023.32

Abstract

P4 is a standardized programming language for the network data plane. But P4 is not just for routing anymore. As programmable switches support stateful objects, P4 programs move beyond just stateless forwarders into new stateful applications: network telemetry (heavy hitters, DDoS detection, performance monitoring), middleboxes (firewalls, NAT, load balancers, intrusion detection), and distributed services (in-network caching, lock management, conflict detection). The complexity of stateful programs and their richer specifications are beyond what existing P4 program verifiers can handle.
Verifiable P4 is a new interactive verification framework for P4 that (1) allows reasoning about multi-packet properties by specifying the per-packet relation between initial and final states; (2) performs modular verification, especially providing a modular description for stateful objects; (3) is foundational, i.e., with a machine-checked soundness proof with respect to a formal operational semantics of P4_{16} (the current specification of P4) in Coq. In addition, our framework includes a proved-correct reference interpreter.
We demonstrate the framework with the specification and verification of a stateful firewall that uses a sliding-window Bloom filter on a Tofino switch to block (most) unsolicited traffic.

Subject Classification

ACM Subject Classification
  • Security and privacy → Logic and verification
Keywords
  • Software Defined Networking
  • Verifiable P4
  • Stateful data plane programming

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Cristian Cadar, Daniel Dunbar, and Dawson R. Engler. KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In Richard Draves and Robbert van Renesse, editors, 8th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2008, December 8-10, 2008, San Diego, California, USA, Proceedings, pages 209-224. USENIX Association, 2008. URL: http://www.usenix.org/events/osdi08/tech/full_papers/cadar/cadar.pdf.
  2. Xiaoqi Chen, Shir Landau-Feibish, Mark Braverman, and Jennifer Rexford. Beaucoup: Answering many network traffic queries, one memory update at a time. In Proceedings of the Annual Conference of the ACM Special Interest Group on Data Communication on the Applications, Technologies, Architectures, and Protocols for Computer Communication, SIGCOMM '20, pages 226-239, New York, NY, USA, 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3387514.3405865.
  3. The P4 Language Consortium. P4_16 language specification, version 1.2.3, July 2022. URL: https://p4.org/p4-spec/docs/P4-16-v1.2.3.pdf.
  4. Graham Cormode and S. Muthukrishnan. An improved data stream summary: the count-min sketch and its applications. Journal of Algorithms, 55(1):58-75, 2005. URL: https://doi.org/10.1016/j.jalgor.2003.12.001.
  5. Ryan Doenges, Mina Tahmasbi Arashloo, Santiago Bautista, Alexander Chang, Newton Ni, Samwise Parkinson, Rudy Peterson, Alaia Solko-Breslin, Amanda Xu, and Nate Foster. Petr4: Formal foundations for P4 data planes. Proc. ACM Program. Lang., 5(POPL):1-32, 2021. URL: https://doi.org/10.1145/3434322.
  6. Ryan Doenges, Tobias Kappé, John Sarracino, Nate Foster, and Greg Morrisett. Leapfrog: certified equivalence for protocol parsers. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, pages 950-965. ACM, 2022. Google Scholar
  7. Dragos Dumitrescu, Radu Stoenescu, Lorina Negreanu, and Costin Raiciu. bf4: towards bug-free P4 programs. In Henning Schulzrinne and Vishal Misra, editors, SIGCOMM '20: Proceedings of the 2020 Annual conference of the ACM Special Interest Group on Data Communication on the applications, technologies, architectures, and protocols for computer communication, pages 571-585. ACM, 2020. URL: https://doi.org/10.1145/3387514.3405888.
  8. Matthias Eichholz, Eric Hayden Campbell, Matthias Krebs, Nate Foster, and Mira Mezini. Dependently-typed data plane programming. Proc. ACM Program. Lang., 6(POPL):40:1-40:28, 2022. URL: https://doi.org/10.1145/3498701.
  9. Kiran Gopinathan and Ilya Sergey. Certifying certainty and uncertainty in approximate membership query structures. In Shuvendu K. Lahiri and Chao Wang, editors, Computer Aided Verification - 32nd International Conference, CAV 2020, Proceedings, Part II, volume 12225 of LNCS, pages 279-303. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-53291-8_16.
  10. Intel. Intel® Tofino™ programmable ethernet switch ASIC. https://www.intel.com/content/www/us/en/products/network-io/programmable-ethernet-switch/tofino-series.html. Accessed: 2023-01-18.
  11. Bart Jacobs, Jan Smans, Pieter Philippaerts, Frédéric Vogels, Willem Penninckx, and Frank Piessens. Verifast: A powerful, sound, predictable, fast verifier for C and java. In Mihaela Gheorghiu Bobaru, Klaus Havelund, Gerard J. Holzmann, and Rajeev Joshi, editors, NASA Formal Methods - Third International Symposium, NFM 2011, Proceedings, volume 6617 of LNCS, pages 41-55. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-20398-5_4.
  12. Xin Jin, Xiaozhou Li, Haoyu Zhang, Robert Soulé, Jeongkeun Lee, Nate Foster, Changhoon Kim, and Ion Stoica. Netcache: Balancing key-value stores with fast in-network caching. In Proceedings of the 26th Symposium on Operating Systems Principles, SOSP '17, pages 121-136. ACM, 2017. URL: https://doi.org/10.1145/3132747.3132764.
  13. Patrick Kennedy. Intel Tofino2 next-gen programmable switch detailed. https://www.servethehome.com/intel-tofino2-next-gen-programmable-switch-detailed/, August 2020.
  14. Yuliang Li, Rui Miao, Changhoon Kim, and Minlan Yu. Flowradar: A better netflow for data centers. In Proceedings of the 13th Usenix Conference on Networked Systems Design and Implementation, NSDI'16, pages 311-324. USENIX Association, 2016. Google Scholar
  15. Jed Liu, William T. Hallahan, Cole Schlesinger, Milad Sharif, Jeongkeun Lee, Robert Soulé, Han Wang, Calin Cascaval, Nick McKeown, and Nate Foster. p4v: Practical verification for programmable data planes. In Sergey Gorinsky and János Tapolcai, editors, Proceedings of the 2018 Conference of the ACM Special Interest Group on Data Communication (SIGCOMM 2018), pages 490-503. ACM, 2018. URL: https://doi.org/10.1145/3230543.3230582.
  16. Rui Miao, Hongyi Zeng, Changhoon Kim, Jeongkeun Lee, and Minlan Yu. Silkroad: Making stateful layer-4 load balancing fast and cheap using switching asics. In Proceedings of the Conference of the ACM Special Interest Group on Data Communication, SIGCOMM '17, pages 15-28. ACM, 2017. URL: https://doi.org/10.1145/3098822.3098824.
  17. Hun Namkung, Zaoxing Liu, Daehyeok Kim, Vyas Sekar, and Peter Steenkiste. SketchLib: Enabling efficient sketch-based monitoring on programmable switches. In 19th USENIX Symposium on Networked Systems Design and Implementation (NSDI 22), pages 743-759, Renton, WA, April 2022. USENIX Association. URL: https://www.usenix.org/conference/nsdi22/presentation/namkung.
  18. Miguel Neves, Lucas Freire, Alberto Schaeffer-Filho, and Marinho Barcellos. Verification of P4 programs in feasible time using assertions. In Proceedings of the 14th International Conference on Emerging Networking EXperiments and Technologies, pages 73-85. ACM, 2018. Google Scholar
  19. Solal Pirelli, Akvile Valentukonyte, Katerina J. Argyraki, and George Candea. Automated verification of network function binaries. In Amar Phanishayee and Vyas Sekar, editors, 19th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2022, Renton, WA, USA, April 4-6, 2022, pages 585-600. USENIX Association, 2022. URL: https://www.usenix.org/conference/nsdi22/presentation/pirelli.
  20. Solal Pirelli, Arseniy Zaostrovnykh, and George Candea. A formally verified NAT stack. Comput. Commun. Rev., 48(5):77-83, 2018. URL: https://doi.org/10.1145/3310165.3310176.
  21. John Reynolds. Separation logic: A logic for shared mutable data structures. In LICS 2002: IEEE Symposium on Logic in Computer Science, pages 55-74, July 2002. Google Scholar
  22. Fabian Ruffy, Tao Wang, and Anirudh Sivaraman. Gauntlet: Finding bugs in compilers for programmable packet processing. In 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20), pages 683-699, 2020. Google Scholar
  23. Radu Stoenescu, Dragos Dumitrescu, Matei Popovici, Lorina Negreanu, and Costin Raiciu. Debugging P4 programs with Vera. In Proceedings of the 2018 Conference of the ACM Special Interest Group on Data Communication, pages 518-532, 2018. Google Scholar
  24. Bingchuan Tian, Jiaqi Gao, Mengqi Liu, Ennan Zhai, Yanqing Chen, Yu Zhou, Li Dai, Feng Yan, Mengjing Ma, Ming Tang, et al. Aquila: a practically usable verification system for production-scale programmable data planes. In Proceedings of the 2021 ACM SIGCOMM 2021 Conference, pages 17-32, 2021. Google Scholar
  25. Qinshi Wang. Foundationally Verified Data Plane Programming. PhD thesis, Princeton University, 2023. In preparation. Google Scholar
  26. Zhuolong Yu, Yiwen Zhang, Vladimir Braverman, Mosharaf Chowdhury, and Xin Jin. Netlock: Fast, centralized lock management using programmable switches. In Proceedings of the Annual Conference of the ACM Special Interest Group on Data Communication on the Applications, Technologies, Architectures, and Protocols for Computer Communication, SIGCOMM '20, pages 126-138, New York, NY, USA, 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3387514.3405857.
  27. Arseniy Zaostrovnykh, Solal Pirelli, Rishabh R. Iyer, Matteo Rizzo, Luis Pedrosa, Katerina J. Argyraki, and George Candea. Verifying software network functions with no verification expertise. In Tim Brecht and Carey Williamson, editors, Proceedings of the 27th ACM Symposium on Operating Systems Principles, SOSP 2019, Huntsville, ON, Canada, October 27-30, 2019, pages 275-290. ACM, 2019. URL: https://doi.org/10.1145/3341301.3359647.
  28. Arseniy Zaostrovnykh, Solal Pirelli, Luis Pedrosa, Katerina J. Argyraki, and George Candea. A formally verified NAT. In Proceedings of the Conference of the ACM Special Interest Group on Data Communication, SIGCOMM 2017, Los Angeles, CA, USA, August 21-25, 2017, pages 141-154. ACM, 2017. URL: https://doi.org/10.1145/3098822.3098833.
  29. Kaiyuan Zhang, Danyang Zhuo, Aditya Akella, Arvind Krishnamurthy, and Xi Wang. Automated verification of customizable middlebox properties with gravel. In Ranjita Bhagwan and George Porter, editors, 17th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2020, Santa Clara, CA, USA, February 25-27, 2020, pages 221-239. USENIX Association, 2020. URL: https://www.usenix.org/conference/nsdi20/presentation/zhang-kaiyuan.
  30. Linfeng Zhang and Yong Guan. Detecting click fraud in pay-per-click streams of online advertising networks. 2008 The 28th International Conference on Distributed Computing Systems, pages 77-84, 2008. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact