A formal model for verifying the impact of stealthy attacks on optimal power flow in power grids

In modern energy control centers, the Optimal Power Flow (OPF) routine is used to determine individual generator outputs that minimize the overall cost of generation while meeting transmission, generation, and system level operating constraints. OPF relies on the output of another module, namely the state estimator, which computes all the system variables, principally the voltage magnitudes with phase angles, transmission line flows, and the bus (and total system) loads. However, recent works have shown that the widely used weighted least square based state estimation is vulnerable to stealthy attacks wherein an adversary can alter certain measurements to corrupt the estimator's solution, yet remain undetected by the estimator's bad data detection algorithm. Here, we show that an attack on state estimation can compromise the integrity of OPF and undermine the economic and secure system operation. We present a formal verification based framework to systematically investigate the feasibility of such stealthy attacks and their influence on OPF. The proposed approach is described with an illustrative example. We also develop a mechanism to increase the efficiency of executing our model, which is evaluated by running experiments on different IEEE test cases.