Automated formal analytics for smart grid security and resiliency
Smart grid is the modernization of the legacy electric power system in which cyber computing and communications are integrated with the physical world of power systems. A smart grid provides efficient and cost-effective management of the grid by allowing real-time monitoring, coordinating, and controlling of the system using communication networks among physical components. A smart grid exhibits complex configurations due to the coexistence of legacy systems with the modern technologies and the interdependency between different cyber and physical components. This inherent complexity significantly increases the vulnerabilities and attack surface in smart grids due to misconfigurations and the lack of security hardening. In a critical infrastructure like smart grid, a security breach can cause devastating damages. Thus, there is a need for formal security analytics to automatically verify smart grid security, provably identify potential attacks and their impacts, and devise cost-effective mitigation plans in a proactive manner. In this dissertation, we focus on achieving these goals through the following three research thrusts.First, we develop a model to formally verify the compliance of the advanced metering infrastructure (AMI) configurations with the security requirements, and generate remediation plans for potential security violations. The development of this model includes formal modeling of AMI configurations and security control requirements based on NIST guidelines. We develop a similar formal model for verifying the supervisory control and data acquisition (SCADA) security. We primarily verify trusted communications between field devices and the control center along with different resiliency constraints to ensure whether SCADA operations remain reliable in contingencies.Second, we formally model a framework to automatically synthesize cost-effective, network isolation-based resiliency architecture for the cyber systems in smart grids. The framework considers isolation requirements and usability and cost constraints, and synthesizes resiliency configurations by exploring various isolation patterns for network traffic flows. We devise a hypothesis testing-based refinement mechanism that systematically finds an optimal resilient architecture by investigating alternative designs. We provide another framework to synthesize redundancy-based resilient configurations for AMI, considering operational integrity and robustness requirements. Third, we develop a formal model for analyzing attack evasions on state estimation, a core control module of SCADA. The model identifies attack vectors (e.g., a set of measurements to be altered) for compromising state estimation, considering (i) a comprehensive set of attack attributes, including access capability, attack resources, and knowledge, (ii) potential attack evasions, and (iii) the interdependency between state estimation and other control modules. The modeling of interdependency enables provable identification of novel stealthy attacks and their escalation to impact on the economic operation of smart grids. For risk mitigation, we provide two techniques: (i) we synthesize proactive security plans that recommend a minimal data integrity of measurements in order to make such attacks infeasible, and (ii) we increase the robustness of the control system against persistent attacks by frequently randomizing state estimation parameters that are critical for launching such attacks.