Verifiably-safe software-defined networks for CPS
Richard Skowyra, Andrei Lapets, Azer Bestavros, Assaf J. Kfoury · 2013
Next generation cyber-physical systems (CPS) are expected to be deployed in domains which require scalability as well as performance under dynamic conditions. This scale and dynamicity will require that CPS communication networks be programmatic (i.e., not requiring manual intervention at any stage), but still maintain iron-clad safety guarantees. Software-defined networking standards like Openflow provide a means for scalably building tailor-made network architectures, but there is no guarantee that these systems are safe, correct, or secure. In this work we propose a methodology and accompanying tools for specifying and modeling distributed systems such that existing formal verification techniques can be transparently used to analyze critical requirements and properties prior to system implementation. We demonstrate this methodology by iteratively modeling and verifying an Openflow learning switch network with respect to network correctness, network convergence, and mobility-related properties.