Abstract
We report on the design of the first fully automatic, machine-checked tool suite for verification of high-level network programs. The tool suite targets programs written in NetCore, a new declarative network programming language. Our work builds on a recent effort by Guha, Reitblatt, and Foster to build a machine-verified compiler from NetCore to OpenFlow, a new protocol for software-defined networking.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
- Network Address Translation
- Weak Precondition
- Ternary Content Addressable Memory
- Forwarding Rule
- Atomic Predicate
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
Foster, N., Harrison, R., Freedman, M.J., Monsanto, C., Rexford, J., Story, A., Walker, D.: Frenetic: A network programming language. In: ICFP (2011)
Guha, A., Reitblatt, M., Foster, N.: Machine-verified network controllers. In: PLDI (2013)
Gutz, S., Story, A., Schlesinger, C., Foster, N.: Splendid isolation: A slice abstraction for software-defined networks. In: Hot Topics in SDNs. ACM (2012)
Kazemian, P., Varghese, G., McKeown, N.: Header space analysis: Static checking for networks. In: NSDI (2012)
Khurshid, A., Zhou, W., Caesar, M., Godfrey, P.: Veriflow: Verifying network-wide invariants in real time. In: Hot Topics in SDNs. ACM (2012)
Mai, H., Khurshid, A., Agarwal, R., Caesar, M., Godfrey, P., King, S.T.: Debugging the data plane with Anteater. ACM SIGCOMM CCR 41(4) (2011)
McCune, W., Wos, L.: Otter: The CADE-13 competition incarnations. JAR 18, 211–220 (1997)
McKeown, N., Anderson, T., Balakrishnan, H., Parulkar, G., Peterson, L., Rexford, J., Shenker, S., Turner, J.: OpenFlow: Enabling innovation in campus networks. ACM SIGCOMM CCR 38(2), 69–74 (2008)
Monsanto, C., Foster, N., Harrison, R., Walker, D.: A compiler and run-time system for network programming languages. In: POPL (2012)
Reitblatt, M., Foster, N., Rexford, J., Schlesinger, C., Walker, D.: Abstractions for network update. In: SIGCOMM (2012)
Robinson, J.A.: A Machine-Oriented Logic Based on the Resolution Principle. Journal of the ACM 12, 23–41 (1965)
Voellmy, A., Hudak, P.: Nettle: Taking the sting out of programming network routers. In: Rocha, R., Launchbury, J. (eds.) PADL 2011. LNCS, vol. 6539, pp. 235–249. Springer, Heidelberg (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer International Publishing Switzerland
About this paper
Cite this paper
Stewart, G. (2013). Computational Verification of Network Programs in Coq. In: Gonthier, G., Norrish, M. (eds) Certified Programs and Proofs. CPP 2013. Lecture Notes in Computer Science, vol 8307. Springer, Cham. https://doi.org/10.1007/978-3-319-03545-1_3
Download citation
DOI: https://doi.org/10.1007/978-3-319-03545-1_3
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-03544-4
Online ISBN: 978-3-319-03545-1
eBook Packages: Computer ScienceComputer Science (R0)