research-article

Free access

SymNet: Scalable symbolic execution for modern networks

Authors:

Radu Stoenescu,

Matei Popovici,

Lorina Negreanu,

Costin RaiciuAuthors Info & Claims

SIGCOMM '16: Proceedings of the 2016 ACM SIGCOMM Conference

Pages 314 - 327

https://doi.org/10.1145/2934872.2934881

Published: 22 August 2016 Publication History

Abstract

We present SymNet, a network static analysis tool based on symbolic execution. SymNet injects symbolic packets and tracks their evolution through the network. Our key novelty is SEFL, a language we designed for expressing data plane processing in a symbolic-execution friendly manner. SymNet statically analyzes an abstract data plane model that consists of the SEFL code for every node and the links between nodes. SymNet can check networks containing routers with hundreds of thousands of prefixes and NATs in seconds, while verifying packet header memory-safety and covering network functionality such as dynamic tunneling, stateful processing and encryption. We used SymNet to debug mid- dlebox interactions from the literature, to check properties of our department’s network and the Stanford backbone. Modeling network functionality is not easy. To aid users we have developed parsers that automatically generate SEFL models from router and switch tables, firewall configura- tions and arbitrary Click modular router configurations. The parsers rely on prebuilt models that are exact and fast to an- alyze. Finally, we have built an automated testing tool that combines symbolic execution and testing to check whether the model is an accurate representation of the real code.

Supplementary Material

MP4 File (p314.mp4)

Download
433.51 MB

References

[1]

C. J. Anderson, N. Foster, A. Guha, J.-B. Jeannin, D. Kozen, C. Schlesinger, and D. Walker. Netkat: Semantic foundations for networks. In POPL'14.

Digital Library

[2]

K. Bhargavan, D. Obradovic, and C. A. Gunter. Formal verification of standards for distance vector routing protocols. J. ACM, 49(4):538–576, July 2002.

Digital Library

[3]

C. Cadar, D. Dunbar, and D. Engler. Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs. In Proc. OSDI'08.

Digital Library

[4]

M. Canini, D. Venzano, P. Perešíni, D. Kostić, and J. Rexford. A nice way to test openflow applications. In Proc. NSDI'12.

Digital Library

[5]

L. De Moura and N. Bjørner. Z3: An efficient smt solver. In Proc. TACAS'08.

Digital Library

[6]

M. Dobrescu and K. Argyraki. Software dataplane verification. In Proc. NSDI'14, NSDI'14.

Digital Library

[7]

S. K. Fayaz, T. Yu, Y. Tobioka, S. Chaki, and V. Sekar. Buzz: Testing context-dependent policies in stateful networks. In Proc. NSDI 2016.

Digital Library

[8]

N. Feamster and H. Balakrishnan. Detecting bgp configuration faults with static analysis. In NSDI, 2005.

Digital Library

[9]

A. Fogel, S. Fung, L. Pedrosa, M. Walraed-Sullivan, R. Govindan, R. Mahajan, and T. Millstein. A general approach to network configuration analysis. In NSDI, 2015.

Digital Library

[10]

N. Foster, R. Harrison, M. J. Freedman, C. Monsanto, J. Rexford, A. Story, and D. Walker. Frenetic: A network programming language. In Proc. ICFP '11.

Digital Library

[11]

T. G. Griffin and J. L. Sobrinho. Metarouting. In Proc. SIGCOMM'05.

Digital Library

[12]

P. Kazemian. Hassel tool and public datasets. https://bitbucket.org/peymank/hassel-public/wiki/Home.

[13]

P. Kazemian, M. Chang, H. Zeng, G. Varghese, N. McKeown, and S. Whyte. Real time network policy checking using header space analysis. In Proc. NSDI'13.

Digital Library

[14]

P. Kazemian, G. Varghese, and N. McKeown. Header space analysis: Static checking for networks. In Proc. NSDI'12.

Digital Library

[15]

A. Khurshid, X. Zou, W. Zhou, M. Caesar, and P. B. Godfrey. Veriflow: Verifying network-wide invariants in real time. In Proc. NSDI'13.

Digital Library

[16]

S. Khurshid, C. S. Păsăreanu, and W. Visser. Generalized symbolic execution for model checking and testing. In Proc. TACAS'03.

Digital Library

[17]

E. Kohler, R. Morris, B. Chen, J. Jannotti, and M. F. Kaashoek. The click modular router. ACM Trans. Comput. Syst., 18(3):263–297, Aug. 2000.

Digital Library

[18]

F. Le, E. Nahum, V. Pappas, M. Touma, and D. Verma. Experiences deploying a transparent split-tcp middlebox in operational networks and the implications for nfv. HotMiddlebox'15, 2015.

Digital Library

[19]

N. P. Lopes, N. Bjørner, P. Godefroid, K. Jayaraman, and G. Varghese. Checking beliefs in dynamic networks. In Proc. NSDI'15.

Digital Library

[20]

H. Mai, A. Khurshid, R. Agarwal, M. Caesar, P. B. Godfrey, and S. T. King. Debugging the data plane with anteater. In Sigcomm, 2011.

Digital Library

[21]

A. Panda, O. Lahav, K. Argyraki, M. Sagiv, and S. Shenker. Verifying Isolation Properties in the Presence of Middleboxes. Tech Report arXiv:1409.7687v1.

[22]

J. Wagner, V. Kuznetsov, and G. Candea. Overify: Optimizing programs for fast verification. In Proc. HotOS'13.

Digital Library

[23]

G. G. Xie, J. Zhan, D. A. Maltz, H. Zhang, A. Greenberg, G. Hjalmtysson, and J. Rexford. On static reachability analysis of ip networks. In Proceedings of Infocom, 2005.

[24]

H. Zeng, P. Kazemian, G. Varghese, and N. McKeown. Automatic test packet generation. In Proc. CoNEXT'12.

Digital Library

Cited By

Wang YYu KWang ZHu KDu HXiang QFang XLi GZhou RKong LShu J(2024)Rethinking DNS Configuration Verification with a Distributed ArchitectureProceedings of the 8th Asia-Pacific Workshop on Networking10.1145/3663408.3663412(23-30)Online publication date: 3-Aug-2024
https://dl.acm.org/doi/10.1145/3663408.3663412
Li RYuan YYe FLiu MYang RYu YGuo TMa QZeng XXu CCai DZhai ESekar VYu MSeneviratne AVeitch D(2024)A General and Efficient Approach to Verifying Traffic Load Properties under Arbitrary k FailuresProceedings of the ACM SIGCOMM 2024 Conference10.1145/3651890.3672246(228-243)Online publication date: 4-Aug-2024
https://dl.acm.org/doi/10.1145/3651890.3672246
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

SymNet: Scalable symbolic execution for modern networks
1. Networks
  1. Network services
    1. Network management
2. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification

Recommendations

SymNet: static checking for stateful networks
HotMiddlebox '13: Proceedings of the 2013 workshop on Hot topics in middleboxes and network function virtualization

Today's networks deploy many stateful procesing boxes ranging from NATs to firewalls and application optimizers: these boxes operate on packet flows, rather than individual packets. As more and more middleboxes are deployed, understanding their ...
Verifying Network Properties in SRv6 based Service Function Chaining
AINTEC '21: Proceedings of the 16th Asian Internet Engineering Conference

Segment Routing over IPv6 (SRv6) is a simple and scalable protocol for building service function chaining (SFC) on IPv6 data plane. Despite the benefits, managing the data plane of service chains in SRv6 is an error-prone task for network operators, ...
A Survey on the Verification of Adversarial Data Planes in Software-Defined Networks
SDN-NFV Sec'21: Proceedings of the 2021 ACM International Workshop on Software Defined Networks & Network Function Virtualization Security

As network policies are becoming increasingly nuanced and complex, so too are the mechanisms required to ensure that the network is functioning as intended. In particular, since the dawn of software-defined networking and the shift towards high-level ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

SIGCOMM '16: Proceedings of the 2016 ACM SIGCOMM Conference

August 2016

645 pages

ISBN:9781450341936

DOI:10.1145/2934872

General Chairs:
Marinho Barcellos
UFRGS
,
Jon Crowcroft
University of Cambridge
,
Program Chairs:
Amin Vahdat
Google
,
Sachin Katti
Stanford University

Copyright © 2016 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]

Sponsors

SIGCOMM: ACM Special Interest Group on Data Communication

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 22 August 2016

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Conference

SIGCOMM '16

Sponsor:

SIGCOMM

SIGCOMM '16: ACM SIGCOMM 2016 Conference

August 22 - 26, 2016

Florianopolis, Brazil

Acceptance Rates

SIGCOMM '16 Paper Acceptance Rate 39 of 231 submissions, 17%;

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

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

99
Total Citations
View Citations
1,867
Total Downloads

Downloads (Last 12 months)256
Downloads (Last 6 weeks)41

Reflects downloads up to 19 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Wang YYu KWang ZHu KDu HXiang QFang XLi GZhou RKong LShu J(2024)Rethinking DNS Configuration Verification with a Distributed ArchitectureProceedings of the 8th Asia-Pacific Workshop on Networking10.1145/3663408.3663412(23-30)Online publication date: 3-Aug-2024
https://dl.acm.org/doi/10.1145/3663408.3663412
Li RYuan YYe FLiu MYang RYu YGuo TMa QZeng XXu CCai DZhai ESekar VYu MSeneviratne AVeitch D(2024)A General and Efficient Approach to Verifying Traffic Load Properties under Arbitrary k FailuresProceedings of the ACM SIGCOMM 2024 Conference10.1145/3651890.3672246(228-243)Online publication date: 4-Aug-2024
https://dl.acm.org/doi/10.1145/3651890.3672246
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
Bringhenti DBussa SSisto RValenza F(2024)A Two-Fold Traffic Flow Model for Network Security ManagementIEEE Transactions on Network and Service Management10.1109/TNSM.2024.340715921:4(3740-3758)Online publication date: Aug-2024
https://doi.org/10.1109/TNSM.2024.3407159
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: Oct-2024
https://doi.org/10.1109/TCAD.2024.3383961
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
Liao JHe BWang JWang JQi QLiao JHe BWang JWang JQi Q(2024)Intelligent Allocation Technologies for All-Scenario KDN ResourcesKey Technologies for On-Demand 6G Network Services10.1007/978-3-031-70606-6_7(163-201)Online publication date: 26-Sep-2024
https://doi.org/10.1007/978-3-031-70606-6_7
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
Li YZhang HWang JWang ZYin XShi XWu J(2023)A General Approach to Generate Test Packets with Network ConfigurationsIEEE Transactions on Parallel and Distributed Systems10.1109/TPDS.2023.3241433(1-14)Online publication date: 2023
https://doi.org/10.1109/TPDS.2023.3241433
Li YHu XJia CWang KLi J(2023)Kano: Efficient Cloud Native Network Policy VerificationIEEE Transactions on Network and Service Management10.1109/TNSM.2022.322967520:3(3747-3764)Online publication date: Sep-2023
https://doi.org/10.1109/TNSM.2022.3229675
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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