research-article

Open access

SwitchV: automated SDN switch validation with P4 models

Authors:

Kinan Dak Albab,

Jonathan DiLorenzo,

Ali Kheradmand,

Steffen Smolka,

Konstantin Weitz,

Muhammad Timarzi,

Minlan YuAuthors Info & Claims

SIGCOMM '22: Proceedings of the ACM SIGCOMM 2022 Conference

Pages 365 - 379

https://doi.org/10.1145/3544216.3544220

Published: 22 August 2022 Publication History

Abstract

Increasing demand on computer networks continuously pushes manufacturers to incorporate novel features and capabilities into their switches at an ever-accelerating pace. However, the traditional approach to switch development relies on informal specifications and handcrafted tests to ensure reliability, which are tedious and slow to maintain and update, effectively putting feature velocity at odds with reliability.

This work describes our experiences following a new approach during the development of switch software stacks that extend fixed-function ASICs with SDN capabilities. Specifically, we focus on SwitchV, our system for automated end-to-end switch validation using fuzzing and symbolic analysis, that evolves effortlessly with the switch specification. Our approach is centered around using the P4 language to model the data plane behavior of the switch as well as its control plane API. Such P4 models are then used as a formal specification by SwitchV, as well as a switch-agnostic contract by SDN controllers, and a living documentation by engineers.

SwitchV found a total of 154 bugs spanning all switch layers. The majority of bugs were highly relevant and fixed within 14 days.

Supplementary Material

PDF File (p365-albab-supp.pdf)

Supplemental material.

Download
74.40 KB

References

[1]

Saswat Anand, Edmund K. Burke, Tsong Yueh Chen, John Clark, Myra B. Cohen, Wolfgang Grieskamp, Mark Harman, Mary Jean Harrold, and Phil Mcminn. 2013. An Orchestrated Survey of Methodologies for Automated Software Test Case Generation. J. Syst. Softw. 86, 8 (Aug. 2013), 1978--2001.

Digital Library

[2]

John Backes, Pauline Bolignano, Byron Cook, Andrew Gacek, Kasper Soe Luckow, Neha Rungta, Martin Schaef, Cole Schlesinger, Rima Tanash, Carsten Varming, et al. 2019. One-click formal methods. IEEE Software 36, 6 (2019), 61--65.

Digital Library

[3]

A. Biere, T. van Dijk, and K. Heljanko. 2017. Hardware model checking competition 2017. In 2017 Formal Methods in Computer Aided Design (FMCAD). 9--9.

[4]

Nikolaj Bjørner and Karthick Jayaraman. 2015. Checking cloud contracts in Microsoft Azure. In International Conference on Distributed Computing and Internet Technology. Springer, 21--32.

Digital Library

[5]

Pat Bosshart, Dan Daly, Glen Gibb, Martin Izzard, Nick McKeown, Jennifer Rexford, Cole Schlesinger, Dan Talayco, Amin Vahdat, George Varghese, et al. 2014. P4: Programming protocol-independent packet processors. ACM SIGCOMM Computer Communication Review 44, 3 (2014), 87--95.

Digital Library

[6]

Thomas Braibant, Jonathan Protzenko, and Gabriel Scherer. 2014. ArtiCheck: well-typed generic fuzzing for module interfaces. http://gallium.inria.fr/scherer/doc/articheck-long.pdf. (2014). Accessed September 5, 2021.

[7]

Pietro Bressana, Noa Zilberman, and Robert Soulé. 2020. Finding Hard-to-Find Data Plane Bugs with a PTA. In Proceedings of the 16th International Conference on Emerging Networking EXperiments and Technologies (CoNEXT '20). Association for Computing Machinery, New York, NY, USA, 218--231.

Digital Library

[8]

Cristian Cadar, Daniel Dunbar, and Dawson Engler. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI'08). USENIX Association, USA, 209--224.

Digital Library

[9]

Marco Canini, Daniele Venzano, Peter Perešíni, Dejan Kostić, and Jennifer Rexford. 2012. A NICE Way to Test Openflow Applications. In Proceedings of the 9th USENIX Conference on Networked Systems Design and Implementation (NSDI'12). USENIX Association, USA, 10.

Digital Library

[10]

Sang Kil Cha, Maverick Woo, and David Brumley. 2015. Program-Adaptive Mutational Fuzzing. In Proceedings of the 2015 IEEE Symposium on Security and Privacy (SP '15). IEEE Computer Society, USA, 725--741.

Digital Library

[11]

W.-T. Cheng and T.J. Chakraborty. 1989. Gentest: an automatic test-generation system for sequential circuits. Computer 22, 4 (1989), 43--49.

Digital Library

[12]

Joonwon Choi, Muralidaran Vijayaraghavan, Benjamin Sherman, Adam Chlipala, and Arvind. 2017. Kami: A Platform for High-Level Parametric Hardware Specification and Its Modular Verification. Proc. ACM Program. Lang. 1, ICFP, Article 24 (Aug. 2017), 30 pages.

Digital Library

[13]

Sean Choi, Boris Burkov, Alex Eckert, Tian Fang, Saman Kazemkhani, Rob Sherwood, Ying Zhang, and Hongyi Zeng. 2018. FBOSS: Building Switch Software at Scale. In Proceedings of the 2018 Conference of the ACM Special Interest Group on Data Communication (SIGCOMM '18). Association for Computing Machinery, New York, NY, USA, 342--356.

Digital Library

[14]

P4 community. 2020. P4 Constraints. https://github.com/p4lang/p4-constraints. (2020). Accessed December 20, 2020.

[15]

P4 community. 2020. P4 Runtime specification. https://p4.org/p4runtime/spec/v1.2.0/P4Runtime-Spec.html. (2020). Accessed January 13, 2021.

[16]

The P4 Language Consortium. 2017. P4₁₆ Language Specification. https://p4.org/p4-spec/docs/P4-16-v1.0.0-spec.html. (2017). Accessed January 19, 2022.

[17]

Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'08/ETAPS'08). Springer-Verlag, Berlin, Heidelberg, 337--340.

Digital Library

[18]

Edsger W Dijkstra. 1975. Guarded commands, non-determinacy and a calculus for the derivation of programs. ACM SIGPLAN Notices 10, 6 (1975), 2--2.

Digital Library

[19]

Andrew D Ferguson, Steve Gribble, Chi-Yao Hong, Charles Edwin Killian, Waqar Mohsin, Henrik Muehe, Joon Ong, Leon Poutievski, Arjun Singh, Lorenzo Vicisano, et al. 2021. Orion: Google's Software-Defined Networking Control Plane. In NSDI. 83--98.

[20]

Open Networking Foundation. 2021. P4 Integrated Network Stack (PINS). https://opennetworking.org/pins/. (2021). Accessed September 5, 2021.

[21]

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). Association for Computing Machinery, New York, NY, USA, Article 4, 7 pages.

Digital Library

[22]

Timon Gehr, Sasa Misailovic, Petar Tsankov, Laurent Vanbever, Pascal Wiesmann, and Martin Vechev. 2018. Bayonet: Probabilistic Inference for Networks. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2018). Association for Computing Machinery, New York, NY, USA, 586--602.

Digital Library

[23]

Patrice Godefroid, Hila Peleg, and Rishabh Singh. 2017. Learn amp;Fuzz: Machine learning for input fuzzing. In 2017 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE). 50--59.

[24]

Google. 2020. P4 PDPI: Program Dependent Intermediate Representation. https://github.com/google/p4-pdpi. (2020). Accessed January 27, 2021.

[25]

Alex Horn, Ali Kheradmand, and Mukul R. Prasad. 2017. Delta-net: Real-time Network Verification Using Atoms. In 14th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2017, Boston, MA, USA, March 27--29, 2017. USENIX Association, 735--749. https://www.usenix.org/conference/nsdi17/technical-sessions/presentation/horn-alex

Digital Library

[26]

Alex Horn, Ali Kheradmand, and Mukul R. Prasad. 2019. A Precise and Expressive Lattice-theoretical Framework for Efficient Network Verification. In 27th IEEE International Conference on Network Protocols, ICNP 2019, Chicago, IL, USA, October 8--10, 2019. IEEE, 1--12.

[27]

Intel. 2022. Intel® Tofino™ Series Programmable Ethernet Switch ASIC. https://www.intel.com/content/www/us/en/products/network-io/programmable-ethernet-switch/tofino-series.html. (2022). accessed Jun, 19 2022.

[28]

Sushant Jain, Alok Kumar, Subhasree Mandal, Joon Ong, Leon Poutievski, Arjun Singh, Subbaiah Venkata, Jim Wanderer, Junlan Zhou, Min Zhu, et al. 2013. B4: Experience with a globally-deployed software defined WAN. ACM SIGCOMM Computer Communication Review 43, 4 (2013), 3--14.

Digital Library

[29]

Qiao Kang, Jiarong Xing, Yiming Qiu, and Ang Chen. 2021. Probabilistic Profiling of Stateful Data Planes for Adversarial Testing. In Proceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS 2021). Association for Computing Machinery, New York, NY, USA, 286--301.

Digital Library

[30]

Peyman Kazemian, George Varghese, and Nick McKeown. 2012. Header Space Analysis: Static Checking for Networks. In Proceedings of the 9th USENIX Conference on Networked Systems Design and Implementation (NSDI'12). USENIX Association, USA, 9.

Digital Library

[31]

Ali Kheradmand. 2020. Automatic Inference of High-Level Network Intents by Mining Forwarding Patterns. In SOSR '20: Symposium on SDN Research, San Jose, CA, USA, March 3, 2020. ACM, 27--33.

Digital Library

[32]

Ali Kheradmand and Grigore Rosu. 2018. P4K: A Formal Semantics of P4 and Applications. CoRR abs/1804.01468 (2018). arXiv:1804.01468 http://arxiv.org/abs/1804.01468

[33]

Ahmed Khurshid, Xuan Zou, Wenxuan Zhou, Matthew Caesar, and Philip Brighten Godfrey. 2013. VeriFlow: Verifying Network-Wide Invariants in Real Time. In Proceedings of the 10th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2013, Lombard, IL, USA, April 2--5, 2013. USENIX Association, 15--27. https://www.usenix.org/conference/nsdi13/technical-sessions/presentation/khurshid

[34]

Dexter Kozen. 2014. NetKAT --- A Formal System for the Verification of Networks. In Programming Languages and Systems, Jacques Garrigue (Ed.). Springer International Publishing, Cham, 1--18.

[35]

Caroline Lemieux and Koushik Sen. 2018. Fairfuzz: A targeted mutation strategy for increasing greybox fuzz testing coverage. In Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering. 475--485.

Digital Library

[36]

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). Association for Computing Machinery, New York, NY, USA, 490--503.

Digital Library

[37]

Yuan Lu and Mike Jorda. 2004. Verifying a Gigabit Ethernet Switch Using SMV. In Proceedings of the 41st Annual Design Automation Conference (DAC '04). Association for Computing Machinery, New York, NY, USA, 230--233.

Digital Library

[38]

Haohui Mai, Ahmed Khurshid, Rachit Agarwal, Matthew Caesar, P. Brighten Godfrey, and Samuel Talmadge King. 2011. Debugging the Data Plane with Anteater. SIGCOMM Comput. Commun. Rev. 41, 4 (Aug. 2011), 290--301.

Digital Library

[39]

Nick McKeown, Tom Anderson, Hari Balakrishnan, Guru Parulkar, Larry Peterson, Jennifer Rexford, Scott Shenker, and Jonathan Turner. 2008. OpenFlow: Enabling Innovation in Campus Networks. SIGCOMM Comput. Commun. Rev. 38, 2 (March 2008), 69--74.

Digital Library

[40]

Justin Meza, Tianyin Xu, Kaushik Veeraraghavan, and Onur Mutlu. 2018. A large scale study of data center network reliability. In Proceedings of the Internet Measurement Conference 2018. 393--407.

[41]

Mehdi Mirzaaghaei, Fabrizio Pastore, and Mauro Pezzè. 2010. Automatically repairing test cases for evolving method declarations. In 2010 IEEE International Conference on Software Maintenance. 1--5.

Digital Library

[42]

Bao N. Nguyen, Bryan Robbins, Ishan Banerjee, and Atif Memon. 2014. GUITAR: An Innovative Tool for Automated Testing of GUI-Driven Software. Automated Software Engg. 21, 1 (March 2014), 65--105.

Digital Library

[43]

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). Association for Computing Machinery, New York, NY, USA, Article 5, 7 pages.

Digital Library

[44]

Mohammad A. Noureddine, Amanda Hsu, Matthew Caesar, Fadi A. Zaraket, and William H. Sanders. 2019. P4AIG: Circuit-Level Verification of P4 Programs. In 2019 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks - Supplemental Volume (DSN-S). 21--22.

[45]

P4lang. 2022. The BMv2 Simple Switch target. https://github.com/p4lang/behavioral-model/blob/d52ac6257bb3a58606383d03b31ed89671504791/docs/simple_switch.md. (2022). accessed Jun, 19 2022.

[46]

Rohan Padhye, Caroline Lemieux, Koushik Sen, Mike Papadakis, and Yves Le Traon. 2019. Semantic Fuzzing with Zest. In Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2019). Association for Computing Machinery, New York, NY, USA, 329--340.

Digital Library

[47]

Rohan Padhye, Caroline Lemieux, Koushik Sen, Laurent Simon, and Hayawardh Vijayakumar. 2019. Fuzzfactory: domain-specific fuzzing with waypoints. Proceedings of the ACM on Programming Languages 3, OOPSLA (2019), 1--29.

Digital Library

[48]

Santhosh Prabhu, Kuan-Yen Chou, Ali Kheradmand, Brighten Godfrey, and Matthew Caesar. 2020. Plankton: Scalable network configuration verification through model checking. In 17th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2020, Santa Clara, CA, USA, February 25--27, 2020. USENIX Association, 953--967. https://www.usenix.org/conference/nsdi20/presentation/prabhu

[49]

Open Compute Project. 2015. Switch Abstraction Interface (SAI): A Reference Switch Abstraction Interface for OCP. Technical Report.

[50]

Open Compute Project. 2017. SAI Object Model. https://github.com/opencomputeproject/SAI/blob/master/doc/object-model/pipeline_object_model.pdf. (2017). Accessed January 12, 2022.

[51]

Talia Ringer. 2021. Proof Repair. Ph.D. Dissertation. University of Washington.

[52]

Kostya Serebryany. 2016. Libfuzzer: A library for coverage-guided fuzz testing (within llvm). URL https://releases.llvm.org/7.0 (2016).

[53]

Haruto Tanno, Xiaojing Zhang, Takashi Hoshino, and Koushik Sen. 2015. TesMa and CATG: Automated Test Generation Tools for Models of Enterprise Applications. In 2015 IEEE/ACM 37th IEEE International Conference on Software Engineering, Vol. 2. 717--720.

[54]

Junjie Wang, Bihuan Chen, Lei Wei, and Yang Liu. 2017. Skyfire: Data-Driven Seed Generation for Fuzzing. In 2017 IEEE Symposium on Security and Privacy (SP). 579--594.

[55]

Xin Wu, Daniel Turner, Chao-Chih Chen, David A Maltz, Xiaowei Yang, Lihua Yuan, and Ming Zhang. 2012. NetPilot: Automating datacenter network failure mitigation. In Proceedings of the ACM SIGCOMM 2012 conference on Applications, technologies, architectures, and protocols for computer communication. 419--430.

Digital Library

[56]

Lihua Yuan and Microsoft Azure Network Team. 2018. SONiC: Software for Open Networking in the Cloud. (Aug. 2018). Retrieved July 1, 2022 from https://conferences.sigcomm.org/events/apnet2018/slides/lihua.pdf

[57]

Michał Zalewski. 2019. American Fuzzy Lop. http://lcamtuf.coredump.cx/af. (2019). Accessed September 5, 2021.

[58]

Hongyi Zeng, Peyman Kazemian, George Varghese, and Nick McKeown. 2012. Automatic Test Packet Generation. In Proceedings of the 8th International Conference on Emerging Networking Experiments and Technologies (CoNEXT '12). Association for Computing Machinery, New York, NY, USA, 241--252.

Digital Library

[59]

Junlan Zhou, Malveeka Tewari, Min Zhu, Abdul Kabbani, Leon Poutievski, Arjun Singh, and Amin Vahdat. 2014. WCMP: Weighted Cost Multipathing for Improved Fairness in Data Centers. In Proceedings of the Ninth European Conference on Computer Systems (EuroSys '14). Association for Computing Machinery, New York, NY, USA, Article 5, 14 pages.

Digital Library

Cited By

Wang CScazzariello MFarshin AFerlin SKostić DChiesa M(2024)NetConfEval: Can LLMs Facilitate Network Configuration?Proceedings of the ACM on Networking10.1145/36562962:CoNEXT2(1-25)Online publication date: 13-Jun-2024
https://dl.acm.org/doi/10.1145/3656296
Ollando RShin SBriand L(2024)Learning Failure-Inducing Models for Testing Software-Defined NetworksACM Transactions on Software Engineering and Methodology10.1145/364154133:5(1-25)Online publication date: 3-Jun-2024
https://dl.acm.org/doi/10.1145/3641541

Index Terms

SwitchV: automated SDN switch validation with P4 models
1. Networks
  1. Network architectures
    1. Programming interfaces
  2. Network properties
    1. Network reliability
2. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
  2. Software notations and tools
    1. System description languages

Recommendations

Precise Time-synchronization in the Data-Plane using Programmable Switching ASICs
SOSR '19: Proceedings of the 2019 ACM Symposium on SDN Research

Current implementations of time synchronization protocols (e.g. PTP) in standard industry-grade switches handle the protocol stack in the slow-path (control-plane). With new use cases of in-network computing using programmable switching ASICs, global ...
Improving function coverage with munch: a hybrid fuzzing and directed symbolic execution approach
SAC '18: Proceedings of the 33rd Annual ACM Symposium on Applied Computing

Fuzzing and symbolic execution are popular techniques for finding vulnerabilities and generating test-cases for programs. Fuzzing, a blackbox method that mutates seed input values, is generally incapable of generating diverse inputs that exercise all ...
Delay Analysis in Programmable Data Plane Using Jitter Calculations
IC3-2023: Proceedings of the 2023 Fifteenth International Conference on Contemporary Computing

The second generation of Software Defined Networks (SDN) made the network more flexible and automated with the introduction of programmable forwarding devices. This programmability has reduced the delay and processing time taken by a traditional router ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

SIGCOMM '22: Proceedings of the ACM SIGCOMM 2022 Conference

August 2022

858 pages

ISBN:9781450394208

DOI:10.1145/3544216

General Chairs:
Fernando Kuipers
Delft University of Technology
,
Ariel Orda
Technion Israel Institute of Technology

Copyright © 2022 Owner/Author.

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

Sponsors

SIGCOMM: ACM Special Interest Group on Data Communication

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 22 August 2022

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

NSF

Conference

SIGCOMM '22

Sponsor:

SIGCOMM

SIGCOMM '22: ACM SIGCOMM 2022 Conference

August 22 - 26, 2022

Amsterdam, Netherlands

Acceptance Rates

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

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
1,678
Total Downloads

Downloads (Last 12 months)460
Downloads (Last 6 weeks)35

Reflects downloads up to 04 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Wang CScazzariello MFarshin AFerlin SKostić DChiesa M(2024)NetConfEval: Can LLMs Facilitate Network Configuration?Proceedings of the ACM on Networking10.1145/36562962:CoNEXT2(1-25)Online publication date: 13-Jun-2024
https://dl.acm.org/doi/10.1145/3656296
Ollando RShin SBriand L(2024)Learning Failure-Inducing Models for Testing Software-Defined NetworksACM Transactions on Software Engineering and Methodology10.1145/364154133:5(1-25)Online publication date: 3-Jun-2024
https://dl.acm.org/doi/10.1145/3641541

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