Team for Research in
Ubiquitous Secure Technology

Citation
Nate Foster. "Machine-Verified Network Controllers". Talk or presentation, 9, October, 2013.

Abstract
In many areas of computing, techniques ranging from testing to formal modeling to full-blown verification have been successfully used to help programmers build reliable systems. But although networks are critical infrastructure, they have largely resisted analysis using formal techniques. Software-defined networking (SDN) is a new network architecture that has the potential to provide a foundation for network reasoning, by standardizing the interfaces used to express network programs and giving them a precise semantics. This paper describes the design and implementation of the first machine-verified SDN controller. Starting from the foundations, we develop a detailed operational model for OpenFlow (the most popular SDN platform) and formalize it in the Coq proof assistant. We then use this model to develop a verified compiler and run-time system for a high-level network programming language. We identify bugs in existing languages and tools built without formal foundations, and prove that these bugs are absent from our system. Finally, we describe our prototype implementation and our experiences using it to build practical applications.

Electronic downloads

• Foster_2013-10-trust.pdf · application/pdf · 10973 kbytes

• HTML

  Nate Foster. <a
  href="http://www.truststc.org/pubs/920.html"
  ><i>Machine-Verified Network
  Controllers</i></a>, Talk or presentation,  9,
  October, 2013.

• Plain text

  Nate Foster. "Machine-Verified Network
  Controllers". Talk or presentation,  9, October, 2013.

• BibTeX

  @presentation{Foster13_MachineVerifiedNetworkControllers,
      author = {Nate Foster},
      title = {Machine-Verified Network Controllers},
      day = {9},
      month = {October},
      year = {2013},
      abstract = {In many areas of computing, techniques ranging
                from testing to formal modeling to full-blown
                verification have been successfully used to help
                programmers build reliable systems. But although
                networks are critical infrastructure, they have
                largely resisted analysis using formal techniques.
                Software-defined networking (SDN) is a new network
                architecture that has the potential to provide a
                foundation for network reasoning, by standardizing
                the interfaces used to express network programs
                and giving them a precise semantics. This paper
                describes the design and implementation of the
                first machine-verified SDN controller. Starting
                from the foundations, we develop a detailed
                operational model for OpenFlow (the most popular
                SDN platform) and formalize it in the Coq proof
                assistant. We then use this model to develop a
                verified compiler and run-time system for a
                high-level network programming language. We
                identify bugs in existing languages and tools
                built without formal foundations, and prove that
                these bugs are absent from our system. Finally, we
                describe our prototype implementation and our
                experiences using it to build practical
                applications.},
      URL = {http://www.truststc.org/pubs/920.html}
  }
  

Posted by Carolyn Winter on 18 Nov 2013.
For additional information, see the Publications FAQ or contact webmaster at www truststc org.