Formal synthesis of dependable configurations for advanced metering infrastructures

The Advanced Metering Infrastructure (AMI) in a smart grid comprises of a large number of smart meters along with heterogeneous cyber-physical components. These components communicate with each other through different communication media, protocols, and delivery modes for transmitting usage reports and control commands to and from the utility. There is potential for dependability threats especially due to misconfigurations, which can easily disrupt the operations in AMI. Therefore, an AMI must be configured correctly. In this paper, we present an automated configuration synthesis framework that mitigates potential threats by eliminating mis-configurations. We have manifold contributions in this research: (i) formal modeling of AMI configurations including AMI device configurations, topology and communication properties, and data flows among the devices; (ii) formal modeling of AMI operational integrity properties considering the interdependencies among AMI devices' configurations; and (iii) implementing the model using Satisfiability Modulo Theories (SMT), execution of which synthesizes necessary AMI configurations. We demonstrate the proposed framework on an example case study and evaluate the scalability of the framework on various synthetic AMI networks.