short-paper

p4pktgen: Automated Test Case Generation for P4 Programs

Authors:

Andres Nötzli,

Andy Fingerhut,

Peter AthanasAuthors Info & Claims

SOSR '18: Proceedings of the Symposium on SDN Research

Article No.: 5, Pages 1 - 7

https://doi.org/10.1145/3185467.3185497

Published: 28 March 2018 Publication History

Abstract

With the rise of programmable network switches, network infrastructure is becoming more flexible and more capable than ever before. Programming languages such as P4 lower the barrier for changing the inner workings of network switches and offer a uniform experience across different devices. However, this programmability also brings the risk of introducing hard-to-catch bugs at a level that was previously covered by well-tested devices with a fixed set of capabilities. Subtle discrepancies between different implementations pose a risk of introducing bugs at a layer that is opaque to the user.

To reap the benefit of programmable hardware and keep---or improve upon---the reliability of traditional approaches, new tools are needed. In this work, we present p4pktgen, a tool for automatically generating test cases for P4 programs using symbolic execution. These test cases can be used to validate that P4 programs act as intended on a device.

References

[1]

2017. BMv2 JSON input format. Technical Report. https://github.com/p4lang/behavioral-model/blob/master/docs/JSON_format.md.

[2]

Clark Barrett, Christopher L Conway, Morgan Deters, Liana Hadarean, Dejan Jovanović, Tim King, Andrew Reynolds, and Cesare Tinelli. 2011. CVC4. In CAV.

Digital Library

[3]

Clark Barrett, Pascal Fontaine, and Cesare Tinelli. 2016. The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org. (2016).

[4]

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. SIGCOMM (2014).

Digital Library

[5]

Cristian Cadar, Daniel Dunbar, Dawson R Engler, et al. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In OSDI.

Digital Library

[6]

Marco Canini, Daniele Venzano, Peter Peresini, Dejan Kostic, and Jennifer Rexford. 2012. A NICE way to test OpenFlow applications. In NSDI.

Digital Library

[7]

P4 community. 2017. BMv2. https://github.com/p4lang/behavioral-model. (2017).

[8]

P4 community. 2017. p4c. https://github.com/p4lang/p4c. (2017).

[9]

P4 community. 2017. Switch. https://github.com/p4lang/switch. (2017).

[10]

Huynh Tu Dang, Han Wang, Theo Jepsen, Gordon Brebner, Changhoon Kim, Jennifer Rexford, Robert Soulé, and Hakim Weatherspoon. 2017. Whippersnapper: A P4 Language Benchmark Suite. In SOSR.

Digital Library

[11]

Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An efficient SMT solver. TACAS (2008).

[12]

Mihai Dobrescu and Katerina Argyraki. 2015. Software dataplane verification. Commun. ACM (2015).

Digital Library

[13]

Nate Foster, Cole Schlesinger, Robert Soulé, and Han Wang. 2017. A Program Logic for Automated P4 Verification. (2017). http://p4.org/wp-content/uploads/2017/06/p4-ws-2017-hoare.pdf.

[14]

Patrice Godefroid, Nils Klarlund, and Koushik Sen. 2005. DART: directed automated random testing. In ACM Sigplan Notices.

Digital Library

[15]

Patrice Godefroid, Michael Y Levin, and David Molnar. 2012. SAGE: whitebox fuzzing for security testing. Commun. ACM (2012).

Digital Library

[16]

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

Digital Library

[17]

Ali Kheradmand and Grigore Rosu. 2017. Executable Formal Semantic of P4 and Applications. (2017). http://p4.org/wp-content/uploads/2017/06/p4-ws-2017-p4k-executable-formal-semantic.pdf.

[18]

Eddie Kohler, Robert Morris, Benjie Chen, John Jannotti, and M Frans Kaashoek. 2000. The Click modular router. TOCS (2000).

Digital Library

[19]

Maciej Kuzniar, Peter Peresini, Marco Canini, Daniele Venzano, and Dejan Kostic. 2012. A SOFT way for openflow switch interoperability testing. In Proceedings of the 8th international conference on Emerging networking experiments and technologies.

Digital Library

[20]

Nuno P. Lopes, Nick Mckeown, 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/

[21]

Grigore Rosu and Traian Florin Şerbănută. 2010. An overview of the K semantic framework. The Journal of Logic and Algebraic Programming (2010).

[22]

Koushik Sen, Darko Marinov, and Gul Agha. 2005. CUTE: a concolic unit testing engine for C. In ACM SIGSOFT Software Engineering Notes.

Digital Library

[23]

Nick Stephens, John Grosen, Christopher Salls, Andrew Dutcher, Ruoyu Wang, Jacopo Corbetta, Yan Shoshitaishvili, Christopher Kruegel, and Giovanni Vigna. 2016. Driller: Augmenting Fuzzing Through Selective Symbolic Execution. In NDSS.

[24]

David E Taylor and Jonathan S Turner. 2007. Classbench: A packet classification benchmark. TON (2007).

Digital Library

[25]

Xuejun Yang, Yang Chen, Eric Eide, and John Regehr. 2011. Finding and understanding bugs in C compilers. In ACM SIGPLAN Notices.

Digital Library

[26]

Hongyi Zeng, Peyman Kazemian, George Varghese, and Nick McKeown. 2012. Automatic test packet generation. In CoNEXT.

Digital Library

[27]

Qirun Zhang, Chengnian Sun, and Zhendong Su. 2017. Skeletal program enumeration for rigorous compiler testing. In PLDI.

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
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
Chen XZhang WSun XLiu HZhang JHuang QZhang DZhou HLiu XWu C(2024)Resource-Efficient and Timely Packet Header Vector (PHV) Encoding on Programmable SwitchesIEEE/ACM Transactions on Networking10.1109/TNET.2024.341353032:5(4191-4206)Online publication date: Oct-2024
https://doi.org/10.1109/TNET.2024.3413530
Show More Cited By

p4pktgen: Automated Test Case Generation for P4 Programs
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Software defect analysis

Recommendations

Synthesizable Standard Cell FPGA Fabrics Targetable by the Verilog-to-Routing CAD Flow
Special Section on Field Programmable Logic and Applications 2015 and Regular Papers

In this article, we consider implementing field-programmable gate arrays (FPGAs) using a standard cell design methodology and present a framework for the automated generation of synthesizable FPGA fabrics. The open-source Verilog-to-Routing (VTR) FPGA ...
Clock Power Analysis of Low Power Clock Gated Arithmetic Logic Unit on Different FPGA
CICN '14: Proceedings of the 2014 International Conference on Computational Intelligence and Communication Networks

This paper, deals with Latch Free Clock Gating technique for reduction of clock power and total power consumption in Low Power Arithmetic and Logic Unit and we have analysed power reduction on different FPGA devices. Without latch free clock gating ...
Embedded SoPC Design with Nios II Processor and Verilog Examples

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

SOSR '18: Proceedings of the Symposium on SDN Research

March 2018

195 pages

ISBN:9781450356640

DOI:10.1145/3185467

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
ONS: Open Networking Summit

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 28 March 2018

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Best Short Paper

Qualifiers

Short-paper
Research
Refereed limited

Conference

SOSR '18

Sponsor:

SIGCOMM
ONS

SOSR '18: Symposium on SDN Research

March 28 - 29, 2018

CA, Los Angeles, USA

Acceptance Rates

Overall Acceptance Rate 7 of 43 submissions, 16%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

51
Total Citations
View Citations
885
Total Downloads

Downloads (Last 12 months)36
Downloads (Last 6 weeks)4

Reflects downloads up to 01 Nov 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
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
Chen XZhang WSun XLiu HZhang JHuang QZhang DZhou HLiu XWu C(2024)Resource-Efficient and Timely Packet Header Vector (PHV) Encoding on Programmable SwitchesIEEE/ACM Transactions on Networking10.1109/TNET.2024.341353032:5(4191-4206)Online publication date: Oct-2024
https://doi.org/10.1109/TNET.2024.3413530
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
Robin DKhan J(2024)An open-source P416 compiler backend for reconfigurable match-action table switches: Making networking innovation accessibleComputer Networks10.1016/j.comnet.2024.110246242(110246)Online publication date: Apr-2024
https://doi.org/10.1016/j.comnet.2024.110246
Larsen JGuanciale RHaller PScalas A(2023)P4R-Type: A Verified API for P4 Control Plane ProgramsProceedings of the ACM on Programming Languages10.1145/36228667:OOPSLA2(1935-1963)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622866
Ruffy FLiu JKotikalapudi PHavel VTavante HSherwood RDubina VPeschanenko VSivaraman AFoster NSchulzrinne HKohler EMaltz DMisra V(2023)P4Testgen: An Extensible Test Oracle For P4-16Proceedings of the ACM SIGCOMM 2023 Conference10.1145/3603269.3604834(136-151)Online publication date: 10-Sep-2023
https://dl.acm.org/doi/10.1145/3603269.3604834
Liatifis ASarigiannidis PArgyriou VLagkas T(2023)Advancing SDN from OpenFlow to P4: A SurveyACM Computing Surveys10.1145/355697355:9(1-37)Online publication date: 16-Jan-2023
https://dl.acm.org/doi/10.1145/3556973
Ajayi OAkinyemi TSaadawi T(2023)P4Chain: A Multichain Approach for Real-Time Anomaly Traffic Detection in P4 Network2023 IEEE 14th Annual Ubiquitous Computing, Electronics & Mobile Communication Conference (UEMCON)10.1109/UEMCON59035.2023.10316086(0163-0170)Online publication date: 12-Oct-2023
https://doi.org/10.1109/UEMCON59035.2023.10316086
Shukla AHudemann KVági ZHügerich LSmaragdakis GHecker ASchmid SFeldmann A(2023)Runtime Verification for Programmable SwitchesIEEE/ACM Transactions on Networking10.1109/TNET.2023.323493131:4(1822-1837)Online publication date: Aug-2023
https://doi.org/10.1109/TNET.2023.3234931
Show More Cited By

View Options

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

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents