Visible to the public A Formal Model for Resiliency-Aware Deployment of SDN: A SCADA-Based Case Study

TitleA Formal Model for Resiliency-Aware Deployment of SDN: A SCADA-Based Case Study
Publication TypeConference Paper
Year of Publication2019
AuthorsJakaria, A H M, Rahman, Mohammad Ashiqur, Gokhale, Aniruddha
Conference Name2019 15th International Conference on Network and Service Management (CNSM)
Keywordsbudget constraints, computability, Control Theory and Resiliency, deployment plan, encoding, formal model, formal modeling, hybrid network, incremental deployment, legacy forwarding devices, network synthesis, Network topology, novel grid control operations, power engineering computing, programmable SDN-enabled switches, pubcrawl, real-time data, resilience, Resiliency, resiliency requirements, resiliency-aware deployment, resilient operation, satisfiability modulo theories, SCADA, SCADA network, SCADA systems, SCADA-based case study, SDN architecture, SDNSynth, SDNSynth framework, Smart grid, Smart grids, smart power grids, software defined networking, supervisory control and data acquisition network, Switches, synthesis model, synthetic SCADA systems, systematic deployment methodology

The supervisory control and data acquisition (SCADA) network in a smart grid requires to be reliable and efficient to transmit real-time data to the controller. Introducing SDN into a SCADA network helps in deploying novel grid control operations, as well as, their management. As the overall network cannot be transformed to have only SDN-enabled devices overnight because of budget constraints, a systematic deployment methodology is needed. In this work, we present a framework, named SDNSynth, that can design a hybrid network consisting of both legacy forwarding devices and programmable SDN-enabled switches. The design satisfies the resiliency requirements of the SCADA network, which are specified with respect to a set of identified threat vectors. The deployment plan primarily includes the best placements of the SDN-enabled switches. The plan may include one or more links to be installed newly. We model and implement the SDNSynth framework that includes the satisfaction of several requirements and constraints involved in resilient operation of the SCADA. It uses satisfiability modulo theories (SMT) for encoding the synthesis model and solving it. We demonstrate SDNSynth on a case study and evaluate its performance on different synthetic SCADA systems.

Citation Keyjakaria_formal_2019