More Web Proxy on the site http://driver.im/

research-article

Free access

Software dataplane verification

Authors:

Mihai Dobrescu,

Katerina ArgyrakiAuthors Info & Claims

Communications of the ACM, Volume 58, Issue 11

Pages 113 - 121

https://doi.org/10.1145/2823400

Published: 23 October 2015 Publication History

All formats PDF

Abstract

The industry is in the mood for programmable networks, where an operator can dynamically deploy network functions on network devices, akin to how one deploys virtual machines on physical machines in a cloud environment. Such flexibility brings along the threat of unpredictable behavior and performance. What are the minimum restrictions that we need to impose on network functionality such that we are able to verify that a network device behaves and performs as expected, for example, does not crash or enter an infinite loop? We present the result of working iteratively on two tasks: designing a domain-specific verification tool for packet-processing software, while trying to identify a minimal set of restrictions that packet-processing software must satisfy in order to be verification-friendly. Our main insight is that packet-processing software is a good candidate for domain-specific verification, for example, because it typically consists of distinct pieces of code that share limited mutable state; we can leverage this and other properties to sidestep fundamental verification challenges. We apply our ideas on Click packet-processing software; we perform complete and sound verification of an IP router and two simple middleboxes within tens of minutes, whereas a state-of-the-art general-purpose tool fails to complete the same task within several hours.

References

[1]

Ball, T., Rajamani, S.K. The SLAM project: Debugging system software via static analysis. In Proceedings of the ACM Symposium on the Principles of Programming Languages (POPL) (2002).

Digital Library

[2]

Bishop, S., Fairbairn, M., Norrish, M., Sewell, P., Smith, M., Wansbrough K. Rigorous specification and conformance testing techniques for network protocols, as applied to TCP, UDP, and Sockets. In Proceedings of the ACM SIGCOMM Conference (2005).

Digital Library

[3]

Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X. A static analyzer for large safety-critical software. In Proceedings of the ACM Conference on Programming Language Design and Implementation (PLDI) (2003).

Digital Library

[4]

Cadar, C., Dunbar, D., Engler, D.R. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI) (2008).

Digital Library

[5]

Cadar, C., Engler, D.R. EXE: Automatically generating inputs of death. In Proceedings of the ACM Conference on Computer Communication Security (CCS) (2006).

Digital Library

[6]

Canini, M., Venzano, D., Peresini, P., Kostic, D., Rexford J. A NICE way to test OpenFlow applications. In Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI) (2012).

Digital Library

[7]

Chipounov, V., Kuznetsov, V., Candea, G. The S2E platform: Design, implementation, and applications. ACM Transactions on Computer Systems 30, 1 (February 2012), 2:1--2:49.

Digital Library

[8]

Cook, B., Podelski, A., Rybalchenko, A. Termination proofs for systems code. In Proceedings of the ACM Conference on Programming Language Design and Implementation (PLDI) (2006).

Digital Library

[9]

Dobrescu, M., Egi, N., Argyraki, K., Chun, B.-G., Fall, K., Iannaccone, G., Knies, A., Manesh, M., Ratnasamy, S. RouteBricks: Exploiting parallelism to scale software routers. In Proceedings of the ACM Symposium on Operating Systems Principles (SOSP) (2009).

Digital Library

[10]

I.S.G. European Telecommunications Standards Institute (ETSI). Network Functions Virtualisation (NFV); Use Cases. Technical Report ETSI GS NFV 001 V1.1.1, ETSI, 650 Route des Lucioles, F-06921 Sophia Antipolis Cedex, FRANCE, 2013. Reference DGS/NFV-009.

[11]

Feamster, N., Rexford, J., Zegura, E. The road to SDN: An intellectual history of programmable networks. ACM Comput. Commun. Rev. 44, 2 (April 2014), 87--98.

Digital Library

[12]

Godefroid, P. Model checking for programming languages using Verisoft. In Proceedings of the ACM Symposium on the Principles of Programming Languages (POPL) (1997).

Digital Library

[13]

Godefroid, P. Compositional dynamic test generation. In Proceedings of the ACM Symposium on the Principles of Programming Languages (POPL) (2007).

Digital Library

[14]

Godefroid, P., Klarlund, N., Sen, K. DART: Directed automated random testing. In Proceedings of the ACM Conference on Programming Language Design and Implementation (PLDI) (2005).

Digital Library

[15]

Guha, A., Reitblatt, M., Foster, N. Machine-verified network controllers. In Proceedings of the ACM Conference on Programming Language Design and Implementation (PLDI) (2013).

Digital Library

[16]

Killian, C., Anderson, J.W., Jhala, R., Vahdat, A. Life, death, and the critical transition: Finding liveness bugs in systems code. In Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI) (2007).

Digital Library

[17]

Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Norrish, M., Kolanski, R., Sewell, T., Tuch, H., Winwood, S. seL4: Formal verification of an OS kernel. In Proceedings of the ACM Symposium on Operating Systems Principles (SOSP) (2009).

Digital Library

[18]

Kohler, E., Morris, R., Chen, B., Jannoti, J., Kaashoek, M.F. The click modular router. ACM Trans. Comput. Syst. 18, 3 (August 2000), 263--297.

Digital Library

[19]

Kroening, D., Clarke, E., Yorav, K. Behavioral consistency of C and Verilog programs using bounded model checking. In Proceedings of the Design Automation Conference (DAC) (2003).

Digital Library

[20]

Kuznetsov, V., Kinder, J., Bucur, S., Candea, G. Efficient state merging in symbolic execution. In Proceedings of the ACM Conference on Programming Language Design and Implementation (PLDI) (2012).

Digital Library

[21]

Kuzniar, M., Peresini, P., Canini, M., Venzano, D., Kostic, D. A SOFT way for OpenFlow switch interoperability testing. In Proceedings of the ACM Conference on emerging Networking EXperiments and Technologies (CoNEXT) (2012).

Digital Library

[22]

Musuvathi, M., Engler, D.R. Model checking large network protocol implementations. In Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI) (2004).

Digital Library

[23]

Musuvathi, M., Park, D., Chou, A., Engler, D.R., Dill, D.L. CMC: A pragmatic approach to model checking. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI) (2002).

Digital Library

[24]

Sekar, V., Egi, N., Ratnasamy, S., Reiter, M.K., Shi, G. Design and implementation of a consolidated middlebox architecture. In Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI) (2012).

Digital Library

[25]

Sherry, J., Hasan, S., Scott, C., Krishnamurthy, A., Ratnasamy, S., Sekar, V. Making middleboxes someone else's problem: network processing as a cloud service. In Proceedings of the ACM SIGCOMM Conference (2012).

Digital Library

Cited By

Singha RIyer RLiu CTerrill CMillstein TShenker SVarghese G(2024)If Layering is useful, why not Sublayering?Proceedings of the 23rd ACM Workshop on Hot Topics in Networks10.1145/3696348.3696892(142-149)Online publication date: 18-Nov-2024
https://dl.acm.org/doi/10.1145/3696348.3696892
Jayasena AMishra P(2024)HIVE: Scalable Hardware-Firmware Co-Verification Using Scenario-Based Decomposition and Automated Hint ExtractionIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2024.338396143:10(3278-3291)Online publication date: 1-Oct-2024
https://dl.acm.org/doi/10.1109/TCAD.2024.3383961
He XDong EYang JZhang SWang ZWang ZYang YZhou JSun XSong ELu JLyu BZhu S(2024)CloudPlanner: Minimizing Upgrade Risk of Virtual Network Devices for Large-Scale Cloud NetworksIEEE INFOCOM 2024 - IEEE Conference on Computer Communications10.1109/INFOCOM52122.2024.10621109(741-750)Online publication date: 20-May-2024
https://doi.org/10.1109/INFOCOM52122.2024.10621109
Show More Cited By

Recommendations

Software dataplane verification
NSDI'14: Proceedings of the 11th USENIX Conference on Networked Systems Design and Implementation

Software dataplanes are emerging as an alternative to traditional hardware switches and routers, promising programmability and short time to market. These advantages are set against the risk of disrupting the network with bugs, unpredictable performance,...
UPPAAL-Based Software-Defined Network Verification
TMPA '13: Proceedings of the 2013 Tools & Methods of Program Analysis

A lot of efforts were made in the last few years in the area of software-defined networks (SDN) - a special kind of computer networks in which the switching device control is fully centralized. This paper investigates the problems of formal description ...
Specification and automated verification of concurrent software systems

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Communications of the ACM

Communications of the ACM Volume 58, Issue 11

November 2015

112 pages

ISSN:0001-0782

EISSN:1557-7317

DOI:10.1145/2838899

Editor:
Moshe Y. Vardi
Association for Computing Machinery, New York, NY

Issue’s Table of Contents

Copyright © 2015 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 ACM 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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 23 October 2015

Published in CACM Volume 58, Issue 11

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Research-article
Research
Refereed

Funding Sources

Swiss National Science Foundation

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

13
Total Citations
View Citations
5,453
Total Downloads

Downloads (Last 12 months)381
Downloads (Last 6 weeks)137

Reflects downloads up to 07 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Singha RIyer RLiu CTerrill CMillstein TShenker SVarghese G(2024)If Layering is useful, why not Sublayering?Proceedings of the 23rd ACM Workshop on Hot Topics in Networks10.1145/3696348.3696892(142-149)Online publication date: 18-Nov-2024
https://dl.acm.org/doi/10.1145/3696348.3696892
Jayasena AMishra P(2024)HIVE: Scalable Hardware-Firmware Co-Verification Using Scenario-Based Decomposition and Automated Hint ExtractionIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2024.338396143:10(3278-3291)Online publication date: 1-Oct-2024
https://dl.acm.org/doi/10.1109/TCAD.2024.3383961
He XDong EYang JZhang SWang ZWang ZYang YZhou JSun XSong ELu JLyu BZhu S(2024)CloudPlanner: Minimizing Upgrade Risk of Virtual Network Devices for Large-Scale Cloud NetworksIEEE INFOCOM 2024 - IEEE Conference on Computer Communications10.1109/INFOCOM52122.2024.10621109(741-750)Online publication date: 20-May-2024
https://doi.org/10.1109/INFOCOM52122.2024.10621109
Lepers BGouicem RCarver DLozi JPalix NAponte MZwaenepoel WSopena JLawall JMuller GBilas AMagoutis KMarkatos EKostic DSeltzer M(2020)Provable multicore schedulers with IpanemaProceedings of the Fifteenth European Conference on Computer Systems10.1145/3342195.3387544(1-16)Online publication date: 15-Apr-2020
https://dl.acm.org/doi/10.1145/3342195.3387544
Klimis VParisis GReus B(2020)Towards Model Checking Real-World Software-Defined NetworksComputer Aided Verification10.1007/978-3-030-53291-8_8(126-148)Online publication date: 14-Jul-2020
https://doi.org/10.1007/978-3-030-53291-8_8
Reyes JLopez JZeghlache D(2019)Identifying Running Data-paths in Software Defined Networking Driven Data-planes2019 IEEE 18th International Symposium on Network Computing and Applications (NCA)10.1109/NCA.2019.8935031(1-8)Online publication date: Sep-2019
https://doi.org/10.1109/NCA.2019.8935031
Lopes NRybalchenko A(2019)Fast BGP Simulation of Large DatacentersVerification, Model Checking, and Abstract Interpretation10.1007/978-3-030-11245-5_18(386-408)Online publication date: 11-Jan-2019
https://doi.org/10.1007/978-3-030-11245-5_18
Liu JHallahan WSchlesinger CSharif MLee JSoulé RWang HCaşcaval CMcKeown NFoster NGorinsky STapolcai J(2018)p4vProceedings of the 2018 Conference of the ACM Special Interest Group on Data Communication10.1145/3230543.3230582(490-503)Online publication date: 7-Aug-2018
https://dl.acm.org/doi/10.1145/3230543.3230582
Nötzli AKhan JFingerhut ABarrett CAthanas P(2018)p4pktgenProceedings of the Symposium on SDN Research10.1145/3185467.3185497(1-7)Online publication date: 28-Mar-2018
https://dl.acm.org/doi/10.1145/3185467.3185497
Schmid SSrba J(2018)Polynomial-Time What-If Analysis for Prefix-Manipulating MPLS NetworksIEEE INFOCOM 2018 - IEEE Conference on Computer Communications10.1109/INFOCOM.2018.8486261(1799-1807)Online publication date: 16-Apr-2018
https://dl.acm.org/doi/10.1109/INFOCOM.2018.8486261
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Digital Edition

View this article in digital edition.

Digital Edition

Magazine Site

View this article on the magazine site (external)

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 Article

Media

Figures

Other

Tables

View Issue’s Table of Contents