SDNRacer: concurrency analysis for software-defined networks

Abstract

Concurrency violations are an important source of bugs in Software-Defined Networks (SDN), often leading to policy or invariant violations. Unfortunately, concurrency violations are also notoriously difficult to avoid, detect and debug. This paper presents a novel approach and a tool, SDNRacer, for detecting concurrency violations of SDNs. Our approach is enabled by three key ingredients: (i) a precise happens- before model for SDNs that captures when events can happen concurrently; (ii) a set of sound, domain-specific filters that reduce reported violations by orders of magnitude, and; (iii) a sound and complete dynamic analyzer, based on the above, that can ensure the network is free of harmful errors such as data races and per-packet incoherence. We evaluated SDNRacer on several real-world OpenFlow controllers, running both reactive and proactive applications in large networks. We show that SDNRacer is practically effective: it quickly pinpoints harmful concurrency violations without overwhelming the user with false positives.

References

1. OpenFlow Switch Specification. Version 1.0.0. https://www.opennetworking.org/images/ stories/downloads/sdn-resources/ onf-specifications/openflow/ openflow-spec-v1.0.0.pdf.
2. Open vSwitch. Production Quality, Multilayer Open Virtual Switch. http://openvswitch.org/.
3. Anduo, W. Zhou, B. Godfrey, and M. Caesar. Software-Defined Networks as Databases. In Presented as part of the Open Networking Summit 2014 (ONS 2014), Santa Clara, CA, 2014. USENIX. URL https: //www.usenix.org/conference/ons2014/ technical-sessions/presentation/wang.
4. T. Ball, N. Bjørner, A. Gember, S. Itzhaky, A. Karbyshev, M. Sagiv, M. Schapira, and A. Valadarsky. VeriCon: Towards Verifying Controller Programs in Software-defined Networks. In ACM PLDI ’14. doi: 10.1145/2594291.2594317.
5. R. Beckett, X. K. Zou, S. Zhang, S. Malik, J. Rexford, and D. Walker. An Assertion Language for Debugging SDN Applications. In Proceedings of the Third Workshop on Hot Topics in Software Defined Networking, HotSDN ’14. ACM. doi: 10.1145/2620728.2620743.
6. P. Berde, M. Gerola, J. Hart, Y. Higuchi, M. Kobayashi, T. Koide, B. Lantz, B. O’Connor, P. Radoslavov, W. Snow, and G. Parulkar. ONOS: Towards an Open, Distributed SDN OS. In Proceedings of the Third Workshop on Hot Topics in Software Defined Networking, HotSDN ’14. ACM. doi: 10.1145/2620728.2620744.
7. Big Switch Networks, Inc. Floodlight Circuit Pusher Application. https://github.com/floodlight/ floodlight/tree/v0.91/apps/circuitpusher, 2013.
8. Big Switch Networks, Inc. Floodlight Firewall. https://github.com/floodlight/ floodlight/tree/v0.91/src/main/java/net/ floodlightcontroller/firewall, 2013.
9. Big Switch Networks, Inc. Floodlight Forwarding Application. https://github.com/floodlight/ floodlight/blob/v0.91/src/main/java/ net/floodlightcontroller/forwarding/ Forwarding.java, 2013.
10. Big Switch Networks, Inc. Floodlight Learning Switch. https://github.com/floodlight/ floodlight/tree/v0.91/src/main/java/net/ floodlightcontroller/learningswitch, 2013.
11. Big Switch Networks, Inc. Floodlight Load-Balancer Application. https://github.com/floodlight/ floodlight/tree/v0.91/src/main/java/net/ floodlightcontroller/loadbalancer, 2013.
12. M. Canini, D. Venzano, P. Pereˇs´ıni, D. Kosti´c, and J. Rexford. A NICE Way to Test OpenFlow Applications. In USENIX NSDI ’12.
13. A. T. Clements, M. F. Kaashoek, N. Zeldovich, R. T. Morris, and E. Kohler. The Scalable Commutativity Rule: Designing Scalable Software for Multicore Processors. In ACM SOSP ’13. doi: 10.1145/2517349.2522712.
14. D. Dimitrov, V. Raychev, M. Vechev, and E. Koskinen. Commutativity Race Detection. In ACM PLDI ’14. doi: 10. 1145/2594291.2594322.
15. C. Flanagan and S. N. Freund. FastTrack: Efficient and Precise Dynamic Race Detection. In ACM PLDI ’09. doi: 10. 1145/1542476.1542490.
16. Floodlight. Floodlight Open SDN Controller. http:// projectfloodlight.org/floodlight.
17. N. Foster, R. Harrison, M. J. Freedman, C. Monsanto, J. Rexford, A. Story, and D. Walker. Frenetic: A Network Programming Language. In ACM ICFP ’11. doi: 10.1145/ 2034773.2034812.
18. A. Guha, M. Reitblatt, and N. Foster. Machine-verified Network Controllers. In ACM PLDI ’13. doi: 10.1145/ 2491956.2462178.
19. S. Jain, A. Kumar, S. Mandal, J. Ong, L. Poutievski, A. Singh, S. Venkata, J. Wanderer, J. Zhou, M. Zhu, J. Zolla, U. Hölzle, S. Stuart, and A. Vahdat. B4: Experience with a Globallydeployed Software Defined WAN. In ACM SIGCOMM ’13. doi: 10.1145/2486001.2486019.
20. P. Kazemian, M. Chang, H. Zeng, G. Varghese, N. McKeown, and S. Whyte. Real Time Network Policy Checking Using Header Space Analysis. In USENIX NSDI ’13,.
21. P. Kazemian, G. Varghese, and N. McKeown. Header Space Analysis: Static Checking for Networks. In USENIX NSDI ’12,.
22. A. Khurshid, W. Zhou, M. Caesar, and P. B. Godfrey. Veriflow: Verifying Network-wide Invariants in Real Time. SIGCOMM Comput. Commun. Rev., 42(4), Sept. 2012. doi: 10. 1145/2377677.2377766.
23. M. Ku´zniar, P. Pereˇs´ıni, and D. Kosti´c. What You Need to Know About SDN Flow Tables. In International Conference on Passive and Active Measurement, PAM ’15. Springer International Publishing. doi: 10.1007/ 978-3-319-15509-8_26.
24. L. Lamport. Time, clocks, and the ordering of events in a distributed system. Communications of the ACM, 21(7), 1978.
25. doi: 10.1145/359545.359563.
26. R. Mahajan and R. Wattenhofer. On Consistent Updates in Software Defined Networks. In Proceedings of the Twelfth ACM Workshop on Hot Topics in Networks, HotNets-XII, 2013. doi: 10.1145/2535771.2535791.
27. H. Mai, A. Khurshid, R. Agarwal, M. Caesar, P. B. Godfrey, and S. T. King. Debugging the Data Plane with Anteater. In ACM SIGCOMM ’11. doi: 10.1145/ 2018436.2018470.
28. R. Majumdar, S. D. Tetali, and Z. Wang. Kuai: A Model Checker for Software-defined Networks. In Proceedings of the 14th Conference on Formal Methods in Computer-Aided Design, FMCAD ’14.
29. J. Mccauley. POX: A Python-based OpenFlow Controller. https://github.com/noxrepo/pox.
30. J. McCauley. POX Angler Forwarding Application. https://github.com/noxrepo/pox/blob/ angler/pox/forwarding/l2_multi.py, 2012.
31. J. McCauley. POX EEL Forwarding Application. https://github.com/noxrepo/pox/blob/eel/ pox/forwarding/l2_multi.py, 2015.
32. J. McCauley. POX EEL L2 Learning Switch. https://github.com/noxrepo/pox/blob/eel/ pox/forwarding/l2_learning.py, 2015.
33. J. Miserez, P. Bielik, A. El-Hassany, L. Vanbever, and M. Vechev. SDNRacer: Detecting Concurrency Violations in Software-defined Networks. In Proceedings of the 1st ACM SIGCOMM Symposium on Software Defined Networking Research, in ACM SOSR ’15. doi: 10.1145/2774993.
34. 2775004.
35. C. Monsanto, N. Foster, R. Harrison, and D. Walker. A Compiler and Run-time System for Network Programming Languages. In ACM POPL ’12. doi: 10.1145/2103656.
36. 2103685.
37. T. Nelson, A. D. Ferguson, M. J. G. Scheer, and S. Krishnamurthi. Tierless Programming and Reasoning for Softwaredefined Networks. In USENIX NSDI ’14.
38. Open Networking Laboratory. ONOS (Open Network Operating System): Forwarding Application. https://github.com/opennetworkinglab/ onos/tree/onos-1.2/apps/fwd, 2015.
39. V. Raychev, M. Vechev, and M. Sridharan. Effective Race Detection for Event-driven Programs. In ACM OOPSLA ’13. doi: 10.1145/2509136.2509538.
40. M. Reitblatt, N. Foster, J. Rexford, C. Schlesinger, and D. Walker. Abstractions for Network Update. In ACM SIGCOMM ’12. doi: 10.1145/2342356.2342427.
41. C. Rotsos, N. Sarrar, S. Uhlig, R. Sherwood, and A. W. Moore. OFLOPS: An Open Framework for Openflow Switch Evaluation. In International Conference on Passive and Active Measurement, PAM’12. Springer-Verlag. doi: 10.1007/ 978-3-642-28537-0_9.
42. C. Scott, A. Wundsam, B. Raghavan, A. Panda, A. Or, J. Lai, E. Huang, Z. Liu, A. El-Hassany, S. Whitlock, H. Acharya, K. Zarifis, and S. Shenker. Troubleshooting Blackbox SDN Control Software with Minimal Causal Sequences. In ACM SIGCOMM ’14. doi: 10.1145/2619239.2626304.

Index Terms

• General and reference

  • Cross-computing tools and techniques

    • Verification

• Networks

  • Network services

• Software and its engineering

  • Software creation and management

    • Software development process management

    • Software verification and validation

      • Formal software verification

      • Software defect analysis

        • Software testing and debugging

  • Software organization and properties

    • Software functional properties

      • Formal methods

        • Software verification

• Theory of computation

  • Semantics and reasoning

    • Program reasoning

      • Program verification