research-article

Free access

p4v: practical verification for programmable data planes

Authors:

William Hallahan,

Cole Schlesinger,

Călin Caşcaval,

Nate FosterAuthors Info & Claims

SIGCOMM '18: Proceedings of the 2018 Conference of the ACM Special Interest Group on Data Communication

Pages 490 - 503

https://doi.org/10.1145/3230543.3230582

Published: 07 August 2018 Publication History

Abstract

We present the design and implementation of p4v, a practical tool for verifying data planes described using the P4 programming language. The design of p4v is based on classic verification techniques but adds several key innovations including a novel mechanism for incorporating assumptions about the control plane and domain-specific optimizations which are needed to scale to large programs. We present case studies showing that p4v verifies important properties and finds bugs in real-world programs. We conduct experiments to quantify the scalability of p4v on a wide range of additional examples. We show that with just a few hundred lines of control-plane annotations, p4v is able to verify critical safety properties for switch.p4, a program that implements the functionality of on a modern data center switch, in under three minutes.

References

[1]

Carolyn Jane Anderson, Nate Foster, Arjun Guha, Jean-Baptiste Jean-nin, Dexter Kozen, Cole Schlesinger, and David Walker. 2014. NetKAT: Semantic Foundations for Networks. In POPL. 113--126.

Digital Library

[2]

Mike Barnett, Bor-Yuh Evan Chang, Robert Deline, Bart Jacobs, and K. Rustan M. Leino. 2005. Boogie: A modular Reusable Program Verifier for Object-Oriented Programs. In Formal Methods for Components and Objects. 364--387.

Digital Library

[3]

Ryan Becket, Aarti Gupta, Ratul Mahajan, and David Walker. 2017. A General Approach to Network Configuration Verification. In SIGCOMM. 155--168.

Digital Library

[4]

Nikolaj Bjørner, Garvit Juniwal, Ratul Mahajan, Sanjit A. Seshia, and George Varghese. 2016. ddNF: An Efficient Data Structure for Header Spaces. In Haifa Verification Conference. 49--64.

[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.

Digital Library

[6]

Pat Bosshart, Glen Gibb, Hun-Seok Kim, George Varghese, Nick McKeown, Martin Izzard, Fernando Mujica, and Mark Horowitz. 2013. Forwarding Metamorphosis: Fast Programmable Match-Action Processing in Hardware for SDN. In SIGCOMM. 99--110.

Digital Library

[7]

Cristian Cadar, Daniel Dunbar, and Dawson Engler. 2008. KLEE: Unassisted and Automatic Generation of High-coverage Tests for Complex Systems Programs. In OSDI. 209--224.

Digital Library

[8]

Huynh Tu Dang, Marco Canini, Fernando Pedone, and Robert Soulé. 2016. Paxos Made Switch-y. SIGCOMM CCR 46, 2 (May 2016), 18--24.

Digital Library

[9]

Leonardo de Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems. 337--340.

Digital Library

[10]

Leonardo de Moura and Nikolaj Bjørner. 2011. Satisfiability modulo theories: Introduction and applications. CACM 54, 9 (2011), 69--77.

Digital Library

[11]

Edsger W. Dijkstra. 1975. Guarded Commands, Nondeterminacy, and Formal Derivation of Programs. CACM 18, 8 (1975), 453--457.

Digital Library

[12]

Isil Dillig, Thomas Dillig, and Alex Aiken. 2010. Reasoning About the Unknown in Static Analysis. CACM 53, 8 (2010), 115--123.

Digital Library

[13]

Mihai Dobrescu and Katerina Argyraki. 2015. Software Dataplane Verification. CACM 58, 11 (2015), 113--121.

Digital Library

[14]

Nick Feamster and Hari Balakrishnan. 2005. Detecting BGP configuration faults with static analysis. In NSDI. 43--56.

Digital Library

[15]

Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, and Raymie Stata. 2002. Extended Static Checking for Java. In PLDI. 234--245.

Digital Library

[16]

Cormac Flanagan and James B. Saxe. 2001. Avoiding Exponential Explosion: Generating Compact Verification Conditions. In POPL. 193--205.

Digital Library

[17]

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.

Digital Library

[18]

Nate Foster, Dexter Kozen, Matthew Milano, Alexandra Silva, and Laure Thompson. 2015. A Coalgebraic Decision Procedure for NetKAT. In POPL. 343--355.

Digital Library

[19]

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 SOSR. 4:1--4:7.

Digital Library

[20]

Aaron Gember-Jacobson, Raajay Viswanathan, Aditya Akella, and Ratul Mahajan. 2016. Fast Control Plane Analysis Using an Abstract Representation. In SIGCOMM. 300--313.

Digital Library

[21]

Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sjöberg, and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In OSDI. 653--669.

Digital Library

[22]

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

Digital Library

[23]

Arjun Guha, Claudiu Saftoiu, and Shriram Krishnamurthi. 2010. The essence of JavaScript. In ECOOP. 126--150.

Digital Library

[24]

David Hancock and Jacobus Van der Merwe. 2016. HyPer4: Using P4 to Virtualize the Programmable Data Plane. In CoNEXT. 507--508.

Digital Library

[25]

Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R Lorch, Bryan Parno, Michael L Roberts, Srinath Setty, and Brian Zill. 2015. IronFleet: Proving practical distributed systems correct. In SOSP. 1--17.

Digital Library

[26]

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/.

[27]

C. A. R. Hoare. 1969. An Axiomatic Basis for Computer Programming. CACM 12, 10 (1969), 576--580.

Digital Library

[28]

Xin Jin, Xiaozhou Li, Haoyu Zhang, Nate Foster, Jeongkeun Lee, Robert Soule, Changhoon Kim, and Ion Stoica. 2018. NetChain: Scale-Free Sub-RTT Coordination. In NSDI. 35--49.

[29]

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.

Digital Library

[30]

Ioannis T. Kassios, Peter Müller, and Malte Schwerhoff. 2012. Comparing Verification Condition Generation with Symbolic Execution: An Experience Report. In VSTTE. 196--208.

Digital Library

[31]

Peyman Kazemian. 2017. Network path not found? Forward Networks Blog. Available at https://bit.ly/2FzpEEZ.

[32]

Peyman Kazemian, George Varghese, and Nick McKeown. 2012. Header Space Analysis: Static Checking for Networks. In NSDI. 113--126.

Digital Library

[33]

Ali Kheradmand and Grigore Rosu. 2018. P4K: A Formal Semantics of P4 and Applications. https://arxiv.org/abs/1804.01468.

[34]

Ahmed Khurshid, Xuan Zou, Wenxuan Zhou, Matthew Caesar, and P. Brighten Godfrey. 2013. VeriFlow: Verifying Network-Wide Invariants in Real Time. In NSDI. 15--29.

Digital Library

[35]

Leslie Lamport. 1998. The Part-time Parliament. TOCS 16, 2 (1998), 133--169.

Digital Library

[36]

K. Rustan M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. In Logic for Programming, Artifical Intelligence, and Reasoning. 348--370.

Digital Library

[37]

K Rustan M Leino, Todd Millstein, and James B Saxe. 2005. Generating error traces from verification-condition counterexamples. Science of Computer Programming 55, 1--3 (2005), 209--226.

Digital Library

[38]

Xavier Leroy. 2009. A formally verified compiler back-end. Journal of Automated Reasoning 43, 4 (2009), 363--446.

Digital Library

[39]

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.

Digital Library

[40]

Gregory Malecha, Greg Morrisett, Avraham Shinnar, and Ryan Wisnesky. 2010. Toward a verified relational database management system. In POPL. 237--248.

Digital Library

[41]

Nick McKeown, Timon Sloane, and Jim Wanderer. 2017. P4 Runtime-Putting the Control Plane in Charge of the Forwarding Plane. Available at http://bit.ly/2It6Ecn.

[42]

Nick McKeown, Dan Talayco, George Varghese, Nuno Lopes, Nikolaj Bjorner, and Andrey Rybalchenko. 2016. Automatically verifying reachability and well-formedness in P4 Networks. Technical Report. Microsoft Research. http://bit.ly/2lxFVSW

[43]

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

Digital Library

[44]

P4 Language Consortium. 2017. P4 Language Specification, Version 1.0.4. Available at https://p4.org/specs/.

[45]

P4 Language Consortium. 2017. P4<sub>16</sub> Language Specification. https://p4.org/p4-spec/docs/P4-16-v1.0.0--spec.html.

[46]

Aurojit Panda, Ori Lahav, Katerina J Argyraki, Mooly Sagiv, and Scott Shenker. 2017. Verifying Reachability in Networks with Mutable Datapaths. In NSDI. 699--718.

Digital Library

[47]

Gordon D. Plotkin, Nikolaj Bjørner, Nuno P. Lopes, Andrey Rybalchenko, and George Varghese. 2016. Scaling network verification using symmetry and surgery. In POPL. 69--83.

Digital Library

[48]

François Pottier and Didier Rémy. 2005. Advaned Topis in Types and Programming Languages. MIT Press, Chapter The Essence of ML Type Inference, 389--489.

[49]

Radu Stoenescu, Dragos Dumitrescu, Matei Popovici, Lorina Negreanu, and Costin Raiciu. 2018. Debugging P4 programs with Vera. In SIGCOMM.

Digital Library

[50]

Radu Stonescu, Matei Popovici, Lirina Negranu, and Costin Raiciu. 2016. SymNet: Scalable Symbolic Execution for Modern Networks. In SIGCOMM. 314--327.

Digital Library

[51]

tofino 2015. Barefoot Tofino. https://www.barefootnetworks.com/products/brief-tofino/.

[52]

Yaron Velner, Kalev Alpernas, Aurojit Panda, Alexander Rabinovich, Mooly Sagiv, Scott Shenker, and Sharon Shoham. 2016. Some Complexity Results for Stateful Network Verification. In Tools and Algorithms for the Construction and Analysis of Systems. 811--830.

Digital Library

[53]

Konstanin Weitz, Doug Woos, Emina Torlak, Michael D. Ernst, Arvind Krishnamurthy, and Zachary Tatlock. 2016. Scalable Verification of Border Gateway Protocol Configurations With an SMT Solver. In OOPSLA. 765--780.

Digital Library

[54]

Geoffrey G. Xie, Jibin Zhan, David A. Maltz, Hui Zhang, Albert G. Greenberg, Gísli Hjálmtýsson, and Jennifer Rexford. 2005. On static reachability analysis of IP networks. In IEEE INFOCOM. 2170--2183.

[55]

Hongkun Yang and Simon S. Lam. 2013. Real-time Verification of Network Properties Using Atomic Predicates. In IEEE ICNP.

[56]

Arseniy Zaostrovnykh, Solal Pirelli, Luis David Pedrosa, Katerina Argyraki, and George Candea. 2017. A Formally Verified NAT. SIGCOMM (2017), 141--154.

Digital Library

Cited By

Pathak DS A HChinta SReddy DTammana P(2024)Anomaly Detection in In-Network Fast ReRoute Systems2024 IFIP Networking Conference (IFIP Networking)10.23919/IFIPNetworking62109.2024.10619865(122-130)Online publication date: 3-Jun-2024
https://doi.org/10.23919/IFIPNetworking62109.2024.10619865
Lu DTang BPaper MKogias M(2024)Towards Functional Verification of eBPF ProgramsProceedings of the ACM SIGCOMM 2024 Workshop on eBPF and Kernel Extensions10.1145/3672197.3673435(37-43)Online publication date: 4-Aug-2024
https://dl.acm.org/doi/10.1145/3672197.3673435
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
Show More Cited By

Index Terms

p4v: practical verification for programmable data planes
1. Networks
  1. Network architectures
    1. Programming interfaces
2. Software and its engineering
  1. Software organization and properties
    1. Software functional properties
      1. Formal methods
        Software verification

Recommendations

Verification of P4 programs in feasible time using assertions
CoNEXT '18: Proceedings of the 14th International Conference on emerging Networking EXperiments and Technologies

Recent trends in software-defined networking have extended network programmability to the data plane. Unfortunately, the chance of introducing bugs increases significantly. Verification can help prevent bugs by assuring that the program does not violate ...
Uncovering Bugs in P4 Programs with Assertion-based Verification
SOSR '18: Proceedings of the Symposium on SDN Research

Recent trends in software-defined networking have extended network programmability to the data plane through programming languages such as P4. Unfortunately, the chance of introducing bugs in the network also increases significantly in this new context. ...
POSTER: Finding Vulnerabilities in P4 Programs with Assertion-based Verification
CCS '17: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security

Current trends in SDN extend network programmability to the data plane through the use of programming languages such as P4. In this context, the chance of introducing errors and consequently software vulnerabilities in the network increases ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

SIGCOMM '18: Proceedings of the 2018 Conference of the ACM Special Interest Group on Data Communication

August 2018

604 pages

ISBN:9781450355674

DOI:10.1145/3230543

General Chairs:
Sergey Gorinsky
IMDEA, Spain
,
János Tapolcai
BME, Hungary

Copyright © 2018 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGCOMM: ACM Special Interest Group on Data Communication

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 07 August 2018

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

SIGCOMM '18

Sponsor:

SIGCOMM

SIGCOMM '18: ACM SIGCOMM 2018 Conference

August 20 - 25, 2018

Budapest, Hungary

Acceptance Rates

Overall Acceptance Rate 462 of 3,389 submissions, 14%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

86
Total Citations
View Citations
3,117
Total Downloads

Downloads (Last 12 months)350
Downloads (Last 6 weeks)53

Reflects downloads up to 12 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Pathak DS A HChinta SReddy DTammana P(2024)Anomaly Detection in In-Network Fast ReRoute Systems2024 IFIP Networking Conference (IFIP Networking)10.23919/IFIPNetworking62109.2024.10619865(122-130)Online publication date: 3-Jun-2024
https://doi.org/10.23919/IFIPNetworking62109.2024.10619865
Lu DTang BPaper MKogias M(2024)Towards Functional Verification of eBPF ProgramsProceedings of the ACM SIGCOMM 2024 Workshop on eBPF and Kernel Extensions10.1145/3672197.3673435(37-43)Online publication date: 4-Aug-2024
https://dl.acm.org/doi/10.1145/3672197.3673435
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
Kim JOkhravi HTian DUjcich B(2024)Security Challenges of Intent-Based NetworkingCommunications of the ACM10.1145/3639702Online publication date: 21-Jun-2024
https://doi.org/10.1145/3639702
Chen XLiu HXiao QHuang QZhang DZhou HZhou BWu CLiu XYang Q(2024)Hermes: Low-Overhead Inter-Switch Coordination in Network-Wide Data Plane Program DeploymentIEEE/ACM Transactions on Networking10.1109/TNET.2024.336132432:4(2842-2857)Online publication date: Aug-2024
https://doi.org/10.1109/TNET.2024.3361324
Black CScott-Hayward S(2024)Defeating Data Plane Attacks With Program ObfuscationIEEE Transactions on Dependable and Secure Computing10.1109/TDSC.2023.327793921:3(1317-1330)Online publication date: May-2024
https://doi.org/10.1109/TDSC.2023.3277939
Zhang DYe CHe F(2024)P4Inv: Inferring Packet Invariants for Verification of Stateful P4 ProgramsIEEE INFOCOM 2024 - IEEE Conference on Computer Communications10.1109/INFOCOM52122.2024.10621366(2129-2138)Online publication date: 20-May-2024
https://doi.org/10.1109/INFOCOM52122.2024.10621366
Dumitru MBădoiu VGherghescu ARaiciu C(2024)Generating P4 Dataplanes Using LLMs2024 IEEE 25th International Conference on High Performance Switching and Routing (HPSR)10.1109/HPSR62440.2024.10635926(31-36)Online publication date: 22-Jul-2024
https://doi.org/10.1109/HPSR62440.2024.10635926
Bordis TLeino K(2024)Free Facts: An Alternative to Inefficient Axioms in DafnyFormal Methods10.1007/978-3-031-71162-6_8(151-169)Online publication date: 11-Sep-2024
https://doi.org/10.1007/978-3-031-71162-6_8
Liu HXing JHuang YZhuo DDevadas SChen ACalandrino JTroncoso C(2023)Remote direct memory introspectionProceedings of the 32nd USENIX Conference on Security Symposium10.5555/3620237.3620575(6043-6060)Online publication date: 9-Aug-2023
https://dl.acm.org/doi/10.5555/3620237.3620575
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

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 Publication

Media

Figures

Other

Tables

View Table of Contents