Verifiably-safe software-defined networks for CPS
Date
2012-12-10
DOI
Authors
Skowyra, Rick
Lapets, Andrei
Bestavros, Azer
Kfoury, Assaf
Version
OA Version
Citation
Skowyra, Rick; Lapets, Andrei; Bestavros, Azer; Kfoury, Assaf. "Verifiably-Safe Software-Defined Networks for CPS", Technical Report BUCS-TR-2012-020, Computer Science Department, Boston University, December 10, 2012. [Available from: http://hdl.handle.net/2144/11408]
Abstract
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. We posit that a design strategy based on the complementary pairing of software-defined networking and formal verification would enable the CPS community to build next-generation systems without sacrificing the safety and reliability that these systems must deliver.