Document Open Access Logo

How to Avoid Making a Billion-Dollar Mistake: Type-Safe Data Plane Programming with SafeP4

Authors Matthias Eichholz, Eric Campbell, Nate Foster, Guido Salvaneschi, Mira Mezini

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2019.12.pdf
  • Filesize: 0.63 MB
  • 28 pages

Document Identifiers

Author Details

Matthias Eichholz
  • Technische Universität Darmstadt, Germany
Eric Campbell
  • Cornell University, Ithaca, NY, USA
Nate Foster
  • Cornell University, Ithaca, NY, USA
Guido Salvaneschi
  • Technische Universität Darmstadt, Germany
Mira Mezini
  • Technische Universität Darmstadt, Germany

Funding

This work has been co-funded by the German Research Foundation (DFG) as part of the Collaborative Research Center (CRC) 1053 MAKI and 1119 CROSSING, by the DFG projects SA 2918/2-1 and SA 2918/3-1, by the Hessian LOEWE initiative within the Software-Factory 4.0 project, by the German Federal Ministry of Education and Research and by the Hessian Ministry of Science and the Arts within CRISP, by the National Science Foundation under grants CNS-1413972 and CCF-1637532, and by gifts from InfoSys and Keysight.

Cite AsGet BibTex

Matthias Eichholz, Eric Campbell, Nate Foster, Guido Salvaneschi, and Mira Mezini. 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). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 12:1-12:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.ECOOP.2019.12

Abstract

The P4 programming language offers high-level, declarative abstractions that bring the flexibility of software to the domain of networking. Unfortunately, the main abstraction used to represent packet data in P4, namely header types, lacks basic safety guarantees. Over the last few years, experience with an increasing number of programs has shown the risks of the unsafe approach, which often leads to subtle software bugs. This paper proposes SafeP4, a domain-specific language for programmable data planes in which all packet data is guaranteed to have a well-defined meaning and satisfy essential safety guarantees. We equip SafeP4 with a formal semantics and a static type system that statically guarantees header validity - a common source of safety bugs according to our analysis of real-world P4 programs. Statically ensuring header validity is challenging because the set of valid headers can be modified at runtime, making it a dynamic program property. Our type system achieves static safety by using a form of path-sensitive reasoning that tracks dynamic information from conditional statements, routing tables, and the control plane. Our evaluation shows that SafeP4’s type system can effectively eliminate common failures in many real-world programs.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Formal language definitions
  • Networks → Programming interfaces
Keywords
  • P4
  • data plane programming
  • type systems

Metrics

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

Related Versions

References

  1. Mina Tahmasbi Arashloo, Yaron Koral, Michael Greenberg, Jennifer Rexford, and David Walker. SNAP: Stateful Network-Wide Abstractions for Packet Processing. In Proceedings of the 2016 ACM SIGCOMM Conference, SIGCOMM '16, pages 29-43, New York, NY, USA, 2016. ACM. URL: http://dx.doi.org/10.1145/2934872.2934892.
  2. Jiasong Bai, Jun Bi, Menghao Zhang, and Guanyu Li. Filtering Spoofed IP Traffic Using Switching ASICs. In Proceedings of the ACM SIGCOMM 2018 Conference on Posters and Demos, pages 51-53. ACM, 2018. Google Scholar
  3. Andrew Begel, Steven McCanne, and Susan L. Graham. BPF+: Exploiting Global Data-flow Optimization in a Generalized Packet Filter Architecture. In Proceedings of the Conference on Applications, Technologies, Architectures, and Protocols for Computer Communication, SIGCOMM '99, pages 123-134, New York, NY, USA, 1999. ACM. URL: http://dx.doi.org/10.1145/316188.316214.
  4. Pat Bosshart, Dan Daly, Glen Gibb, Martin Izzard, Nick McKeown, Jennifer Rexford, Cole Schlesinger, Dan Talayco, Amin Vahdat, George Varghese, and David Walker. P4: Programming Protocol-independent Packet Processors. SIGCOMM Comput. Commun. Rev., 44(3):87-95, July 2014. URL: http://dx.doi.org/10.1145/2656877.2656890.
  5. John Peter Campora, Sheng Chen, Martin Erwig, and Eric Walkingshaw. Migrating gradual types. Proceedings of the ACM on Programming Languages, 2(POPL):15, 2017. Google Scholar
  6. Martin Casado, Michael J Freedman, Justin Pettit, Jianying Luo, Nick McKeown, and Scott Shenker. Ethane: Taking control of the enterprise. In ACM SIGCOMM Computer Communication Review, volume 37 (4), pages 1-12. ACM, 2007. Google Scholar
  7. P4 Language Consortium. P4 Language Specification, Version 1.0.4. Technical report, Available at https://p4.org/specs/, 2017. Google Scholar
  8. Jonathan Corbet. BPF: the universal in-kernel virtual machine, May 2014. Available at https://lwn.net/Articles/599755/,.
  9. Robert Ennals, Richard Sharp, and Alan Mycroft. Linear Types for Packet Processing. In David Schmidt, editor, Programming Languages and Systems, pages 204-218, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg. Google Scholar
  10. William G. J. Halfond, Alessandro Orso, and Panagiotis Manolios. Using Positive Tainting and Syntax-aware Evaluation to Counter SQL Injection Attacks. In Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering, SIGSOFT '06/FSE-14, pages 175-185, New York, NY, USA, 2006. ACM. URL: http://dx.doi.org/10.1145/1181775.1181797.
  11. Wei Huang, Yao Dong, and Ana Milanova. Type-Based Taint Analysis for Java Web Applications. In Proceedings of the 17th International Conference on Fundamental Approaches to Software Engineering - Volume 8411, pages 140-154, New York, NY, USA, 2014. Springer-Verlag New York, Inc. URL: http://dx.doi.org/10.1007/978-3-642-54804-8_10.
  12. Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler. Featherweight Java: A Minimal Core Calculus for Java and GJ. ACM Trans. Program. Lang. Syst., 23(3):396-450, May 2001. URL: http://dx.doi.org/10.1145/503502.503505.
  13. Xin Jin. netcache-p4, March 2018. URL: https://github.com/netx-repo/netcache-p4.
  14. Xin Jin, Xiaozhou Li, Haoyu Zhang, Nate Foster, Jeongkeun Lee, Robert Soulé, Changhoon Kim, and Ion Stoica. NetChain: Scale-free sub-rtt coordination. In USENIX Symposium on Networked Systems Design and Implementation (NSDI), April 2018. Best paper award. Google Scholar
  15. 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, pages 121-136. ACM, 2017. Google Scholar
  16. Ali Kheradmand and Grigore Roşu. P4K: A formal semantics of P4 and applications. Technical Report https://arxiv.org/abs/1804.01468, University of Illinois at Urbana-Champaign, April 2018. Google Scholar
  17. George T. Klees, Andrew Ruef, Benjamin Cooper, Shiyi Wei, and Michael Hicks. Evaluating Fuzz Testing. In Proceedings of the ACM Conference on Computer and Communications Security (CCS), October 2018. Google Scholar
  18. Chaitanya Kodeboyina. An open-source P4 switch with SAI support, June 2015. URL: https://p4.org/p4/an-open-source-p4-switch-with-sai-support.html.
  19. Rahul Kumar and BB Gupta. Stepping stone detection techniques: Classification and state-of-the-art. In Proceedings of the international conference on recent cognizance in wireless communication & image processing, pages 523-533. Springer, 2016. Google Scholar
  20. Jed Liu, William Hallahan, Cole Schlesinger, Milad Sharif, Jeongkeun Lee, Robert Soulé, Han Wang, Călin Caşcaval, Nick McKeown, and Nate Foster. P4V: Practical Verification for Programmable Data Planes. In Proceedings of the 2018 Conference of the ACM Special Interest Group on Data Communication, SIGCOMM '18, pages 490-503, New York, NY, USA, 2018. ACM. URL: http://dx.doi.org/10.1145/3230543.3230582.
  21. Nick McKeown, Tom Anderson, Hari Balakrishnan, Guru Parulkar, Larry Peterson, Jennifer Rexford, Scott Shenker, and Jonathan Turner. OpenFlow: Enabling Innovation in Campus Networks. SIGCOMM Comput. Commun. Rev., 38(2):69-74, March 2008. URL: http://dx.doi.org/10.1145/1355734.1355746.
  22. Nick McKeown, Dan Talayco, George Varghese, Nuno Lopes, Nikolaj Bjorner, and Andrey Rybalchenko. Automatically verifying reachability and well-formedness in P4 Networks, September 2016. URL: https://www.microsoft.com/en-us/research/publication/automatically-verifying-reachability-well-formedness-p4-networks/.
  23. Robin Milner. A Theory of Type Polymorphism in Programming. Journal of Computer and System Sciences, 17(3):348-375, December 1978. Google Scholar
  24. Barefoot Networks. Tofino 2. URL: https://www.barefootnetworks.com/products/brief-tofino-2/.
  25. Barefoot Networks. Behavioral Model, December 2018. URL: https://github.com/p4lang/behavioral-model.
  26. TJ OConnor, William Enck, W Michael Petullo, and Akash Verma. Pivotwall: SDN-based information flow control. In Proceedings of the Symposium on SDN Research, page 3. ACM, 2018. Google Scholar
  27. Grigore Roşu and Traian Florin Şerbănuţă. An Overview of the K Semantic Framework. Journal of Logic and Algebraic Programming, 79(6):397-434, 2010. URL: http://dx.doi.org/10.1016/j.jlap.2010.03.012.
  28. Anirudh Sivaraman, Alvin Cheung, Mihai Budiu, Changhoon Kim, Mohammad Alizadeh, Hari Balakrishnan, George Varghese, Nick McKeown, and Steve Licking. Packet Transactions: High-Level Programming for Line-Rate Switches. In Proceedings of the 2016 ACM SIGCOMM Conference, SIGCOMM '16, pages 15-28, New York, NY, USA, 2016. ACM. URL: http://dx.doi.org/10.1145/2934872.2934900.
  29. Manu Sridharan. Engineering NullAway, Uber’s Open Source Tool for Detecting NullPointerExceptions on Android, December 2018. URL: https://eng.uber.com/nullaway/.
  30. Radu Stoenescu, Dragos Dumitrescu, Matei Popovici, Lorina Negreanu, and Costin Raiciu. Debugging P4 Programs with Vera. In ACM SIGCOMM, pages 518-532, New York, NY, USA, 2018. ACM. URL: http://dx.doi.org/10.1145/3230543.3230548.
  31. Radu Stoenescu, Matei Popovici, Lorina Negreanu, and Costin Raiciu. SymNet: Scalable symbolic execution for modern networks. In ACM SIGCOMM, pages 314-327, New York, NY, USA, 2016. ACM. URL: http://dx.doi.org/10.1145/2934872.2934881.
  32. Sam Tobin-Hochstadt and Matthias Felleisen. Logical Types for Untyped Languages. In Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming, ICFP '10, pages 117-128, New York, NY, USA, 2010. ACM. URL: http://dx.doi.org/10.1145/1863543.1863561.
  33. Dennis Volpano, Cynthia Irvine, and Geoffrey Smith. A Sound Type System for Secure Flow Analysis. J. Comput. Secur., 4(2-3):167-187, January 1996. URL: http://dl.acm.org/citation.cfm?id=353629.353648.
  34. Menghao Zhang. Anti-spoof, November 2018. URL: https://github.com/zhangmenghao/Anti-spoof.
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 Imprint Privacy Contact