Abstractions for model checking SDN controllers

Divjyot Sethi, Srinivas Narayana, Sharad Malik

Research output: Chapter in Book/Report/Conference proceedingConference contribution

29 Scopus citations

Abstract

Software defined networks (SDNs) are receiving significant attention in the computer networking community, with increasing adoption by the industry. The key feature of SDNs is a centralized controller which programs the packet forwarding behavior of a distributed underlying network. This centralized view of control - which is absent in traditional networks - opens up opportunities for full formal verification. While there is recent research in formal verification of these networks, model checking the controller behavior as it updates the underlying network has only seen limited application. Existing approaches are limited to verifying the controller for a small number of exchanged packets in the network. In this case study, we extend the state of the art by presenting abstractions for model checking controllers for an arbitrarily large number of packets exchanged in the network. We validate the utility of these abstractions through two applications: a learning switch and a stateful firewall.

Original languageEnglish (US)
Title of host publication2013 Formal Methods in Computer-Aided Design, FMCAD 2013
PublisherIEEE Computer Society
Pages145-148
Number of pages4
ISBN (Print)9780983567837
DOIs
StatePublished - 2013
Event13th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2013 - Portland, OR, United States
Duration: Oct 20 2013Oct 23 2013

Publication series

Name2013 Formal Methods in Computer-Aided Design, FMCAD 2013

Other

Other13th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2013
CountryUnited States
CityPortland, OR
Period10/20/1310/23/13

All Science Journal Classification (ASJC) codes

  • Computer Graphics and Computer-Aided Design
  • Logic

Fingerprint Dive into the research topics of 'Abstractions for model checking SDN controllers'. Together they form a unique fingerprint.

  • Cite this

    Sethi, D., Narayana, S., & Malik, S. (2013). Abstractions for model checking SDN controllers. In 2013 Formal Methods in Computer-Aided Design, FMCAD 2013 (pp. 145-148). [6679403] (2013 Formal Methods in Computer-Aided Design, FMCAD 2013). IEEE Computer Society. https://doi.org/10.1109/fmcad.2013.6679403