Design Verification: Treating Networks Like Programs or Chips

Опубликовано 27 июня 2016, 22:05

Surveys reveal that network outages are prevalent, and that many outages take hours to resolve, resulting in significant lost revenue. Many bugs are caused by errors in configuration files, which are programmed using arcane, low-level languages, akin to machine code. Further, mistakes are often hunted down using rudimentary tools such as Ping and Traceroute. Taking our cue from other fields such as hardware design, we would like to explore fresh approaches and contrast them to standard approaches to verification using model checking, SAT solvers, and so forth. While network verification is similar to finite state machine verification, there is domain-specific structure that can be exploited and a different set of properties to verify. Early results suggest that concepts from EDA and program verification can be leveraged to create what might be termed Network Design Automation. What might the equivalent of Layout Versus Schematic tools or Specification Mining be? Could there be a theory of types for networks? Our panelists will explore this vision, touching upon modular network semantics, language design, performance invariants, and interactive network debuggers. We will also explore with the help of SDN experts the connections between this vision and the vision of Software Designed Networks.