research-article

Free access

An assertion language for debugging SDN applications

Authors:

David WalkerAuthors Info & Claims

HotSDN '14: Proceedings of the third workshop on Hot topics in software defined networking

Pages 91 - 96

https://doi.org/10.1145/2620728.2620743

Published: 22 August 2014 Publication History

PDF eReader

Abstract

Software Defined Networking (SDN) provides opportunities for network verification and debugging by offering centralized visibility of the data plane. This has enabled both offline and online data-plane verification. However, little work has gone into the verification of time-varying properties (e.g., dynamic access control), where verification conditions change dynamically in response to application logic, network events, and external stimulus (e.g., operator requests).

This paper introduces an assertion language to support verifying and debugging SDN applications with dynamically changing verification conditions. The language allows programmers to annotate controller applications with C-style assertions about the data plane. Assertions consist of regular expressions on paths to describe path properties for classes of packets, and universal and existential quantifiers that range over programmer-defined sets of hosts, switches, or other network entities. As controller programs dynamically add and remove elements from these sets, they generate new verification conditions that the existing data plane must satisfy. This work proposes an incremental data structure together with an underlying verification engine, to avoid naively re-verifying the entire data plane as these verification conditions change. To validate our ideas, we have implemented a debugging library on top of a modified version of VeriFlow, which is easily integrated into existing controller systems with minimal changes. Using this library, we have verified correctness properties for applications on several controller platforms.

References

[1]

Pox. http://www.noxrepo.org/pox/about-pox/.

Google Scholar

[2]

Handigol, N., Heller, B., Jeyakumar, V., Lantz, B., and McKeown, N. Reproducible network experiments using container-based emulation. In Proceedings of the 8th International Conference on Emerging Networking Experiments and Technologies (2012), CoNEXT '12, ACM, pp. 253--264.

Digital Library

Google Scholar

[3]

Handigol, N., Heller, B., Jeyakumar, V., Maziéres, D., and McKeown, N. I know what your packet did last hop: Using packet histories to troubleshoot networks. In 11th USENIX Symposium on Networked Systems Design and Implementation (NSDI 14) (Apr. 2014), USENIX Association, pp. 71--85.

Digital Library

Google Scholar

[4]

Kazemian, P., Chang, M., Zeng, H., Varghese, G., McKeown, N., and Whyte, S. Real time network policy checking using header space analysis. In Proceedings of the 10th USENIX Conference on Networked Systems Design and Implementation (2013), pp. 99--112.

Digital Library

Google Scholar

[5]

Kazemian, P., Varghese, G., and McKeown, N. Header space analysis: Static checking for networks. In Presented as part of the 9th USENIX Symposium on Networked Systems Design and Implementation (NSDI (San Jose, CA, 2012), USENIX, pp. 113--126.

Digital Library

Google Scholar

[6]

Khurshid, A., Zou, X., Zhou, W., Caesar, M., and Godfrey, P. B. Veriflow: Verifying network-wide invariants in real time. In Proceedings of the 10th USENIX Conference on Networked Systems Design and Implementation (2013), pp. 15--28.

Digital Library

Google Scholar

[7]

Mai, H., Khurshid, A., Agarwal, R., Caesar, M., Godfrey, P. B., and King, S. T. Debugging the data plane with anteater. 290--301.

Google Scholar

[8]

Monsanto, C., Reich, J., Foster, N., Rexford, J., and Walker, D. Composing software-defined networks. In Proceedings of the 10th USENIX Conference on Networked Systems Design and Implementation (2013), nsdi'13, pp. 1--14.

Digital Library

Google Scholar

[9]

Reitblatt, M., Canini, M., Guha, A., and Foster, N. Fattire: Declarative fault tolerance for software-defined networks. In Proceedings of the Second ACM SIGCOMM Workshop on Hot Topics in Software Defined Networking (2013), pp. 109--114.

Digital Library

Google Scholar

[10]

Soul--e, R., Basu, S., Kleinberg, R., Sirer, E. G., and Foster, N. Managing the network with merlin. In Proceedings of the Twelfth ACM Workshop on Hot Topics in Networks (2013), pp. 24:1--24:7.

Digital Library

Google Scholar

[11]

Wundsam, A., Levin, D., Seetharaman, S., and Feldmann, A. Ofrewind: Enabling record and replay troubleshooting for networks. In Proceedings of the 2011 USENIX Conference on Annual Technical Conference (2011), pp. 29--29.

Digital Library

Google Scholar

Cited By

View all

Yao YCui ZTian LLi MPan FHu Y(2024)Scaver: A Scalable Verification System for Programmable NetworkProceedings of the 2024 SIGCOMM Workshop on Formal Methods Aided Network Operation10.1145/3672199.3673887(14-19)Online publication date: 4-Aug-2024
https://dl.acm.org/doi/10.1145/3672199.3673887
Grewal KGodfrey PHsu J(2023)Expressive Policies For Microservice NetworksProceedings of the 22nd ACM Workshop on Hot Topics in Networks10.1145/3626111.3628181(280-286)Online publication date: 28-Nov-2023
https://dl.acm.org/doi/10.1145/3626111.3628181
Hamza KKilani JBensalah FBaddi Y(2023)Evaluation and Analysis of Network Safety Mechanisms in SDN Infrastructure2023 IEEE 6th International Conference on Cloud Computing and Artificial Intelligence: Technologies and Applications (CloudTech)10.1109/CloudTech58737.2023.10366087(01-06)Online publication date: 21-Nov-2023
https://doi.org/10.1109/CloudTech58737.2023.10366087
Show More Cited By

Index Terms

An assertion language for debugging SDN applications
1. Networks
  1. Network services
    1. Network management

Recommendations

Incremental predicate analysis for regression verification

Software products are evolving during their life cycles. Ideally, every revision need be formally verified to ensure software quality. Yet repeated formal verification requires significant computing resources. Verifying each and every revision can be ...
An incremental verification framework for component-based software systems
CBSE '13: Proceedings of the 16th International ACM Sigsoft symposium on Component-based software engineering

We present a tool-supported framework for the efficient reverification of component-based software systems after changes such as additions, removals or modifications of components. The incremental verification engine at the core of our INcremental ...
Validating assertion language rewrite rules and semantics with automated theorem provers

Modern assertion languages such as property specification language (PSL) and System Verilog assertions include many language constructs. By far, the most economical way to process the full languages in automated tools is to rewrite the majority of ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

HotSDN '14: Proceedings of the third workshop on Hot topics in software defined networking

August 2014

252 pages

ISBN:9781450329897

DOI:10.1145/2620728

Program Chairs:
Aditya Akella
University of Wisconsin-Madison, USA
,
Albert Greenberg
Microsoft, USA

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

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 22 August 2014

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Conference

SIGCOMM'14

Sponsor:

SIGCOMM

SIGCOMM'14: ACM SIGCOMM 2014 Conference

August 22, 2014

Illinois, Chicago, USA

Acceptance Rates

HotSDN '14 Paper Acceptance Rate 50 of 114 submissions, 44%;

Overall Acceptance Rate 88 of 198 submissions, 44%

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

43
Total Citations
View Citations
977
Total Downloads

Downloads (Last 12 months)68
Downloads (Last 6 weeks)13

Reflects downloads up to 20 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Yao YCui ZTian LLi MPan FHu Y(2024)Scaver: A Scalable Verification System for Programmable NetworkProceedings of the 2024 SIGCOMM Workshop on Formal Methods Aided Network Operation10.1145/3672199.3673887(14-19)Online publication date: 4-Aug-2024
https://dl.acm.org/doi/10.1145/3672199.3673887
Grewal KGodfrey PHsu J(2023)Expressive Policies For Microservice NetworksProceedings of the 22nd ACM Workshop on Hot Topics in Networks10.1145/3626111.3628181(280-286)Online publication date: 28-Nov-2023
https://dl.acm.org/doi/10.1145/3626111.3628181
Hamza KKilani JBensalah FBaddi Y(2023)Evaluation and Analysis of Network Safety Mechanisms in SDN Infrastructure2023 IEEE 6th International Conference on Cloud Computing and Artificial Intelligence: Technologies and Applications (CloudTech)10.1109/CloudTech58737.2023.10366087(01-06)Online publication date: 21-Nov-2023
https://doi.org/10.1109/CloudTech58737.2023.10366087
Angi ASacco AEsposito FMarchetto GClemm A(2022)NLP4: An Architecture for Intent-Driven Data Plane Programmability2022 IEEE 8th International Conference on Network Softwarization (NetSoft)10.1109/NetSoft54395.2022.9844035(25-30)Online publication date: 27-Jun-2022
https://doi.org/10.1109/NetSoft54395.2022.9844035
Bhayo JJafaq RAhmed AHameed SShah S(2022)A Time-Efficient Approach Toward DDoS Attack Detection in IoT Network Using SDNIEEE Internet of Things Journal10.1109/JIOT.2021.30980299:5(3612-3630)Online publication date: 1-Mar-2022
https://doi.org/10.1109/JIOT.2021.3098029
Rahouti MXiong KXin YJagatheesaperumal SAyyash MShaheed M(2022)SDN Security Review: Threat Taxonomy, Implications, and Open ChallengesIEEE Access10.1109/ACCESS.2022.316897210(45820-45854)Online publication date: 2022
https://doi.org/10.1109/ACCESS.2022.3168972
Ahmed NBakar KZuhra FKehkashan TMujahid MRathore MDawood MIsyaku B(2022)Security & Privacy in Software Defined Networks, Issues, Challenges and Cost of Developed Solutions: A Systematic Literature ReviewInternational Journal of Wireless Information Networks10.1007/s10776-022-00561-y29:3(314-340)Online publication date: 23-Jun-2022
https://doi.org/10.1007/s10776-022-00561-y
Rikhotso VVelempini M(2022)The Evaluation of the Two Detection Algorithms for Distributed Denial of Service AttackAd Hoc Networks and Tools for IT10.1007/978-3-030-98005-4_5(63-71)Online publication date: 27-Mar-2022
https://doi.org/10.1007/978-3-030-98005-4_5
Sharmila SVijayarani S(2022)Machine to Machine (M2M), Radio-frequency Identification (RFID), and Software-Defined Networking (SDN): Facilitators of the Internet of ThingsArtificial Intelligence-based Internet of Things Systems10.1007/978-3-030-87059-1_8(219-242)Online publication date: 11-Jan-2022
https://doi.org/10.1007/978-3-030-87059-1_8
Kumar RAggarwal AHanda KSoni PKumar M(2022)Software‐Defined Networks and Its ApplicationsSoftware Defined Networks10.1002/9781119857921.ch3(63-96)Online publication date: 11-Aug-2022
https://doi.org/10.1002/9781119857921.ch3
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

Incremental predicate analysis for regression verification

An incremental verification framework for component-based software systems

Validating assertion language rewrite rules and semantics with automated theorem provers