Ryan Beckett
Jennifer Rexford
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.
- Pox. http://www.noxrepo.org/pox/about-pox/.Google Scholar
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
Index Terms
- An assertion language for debugging SDN applications
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 engineeringWe 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