Security design against stealthy attacks on power system state estimation: A formal approach

State estimation is very important for securely, reliably, and efficiently maintaining a power grid. If state estimation is not protected, an attacker can compromise meters or communication systems and introduce false measurements, which can evade existing Bad Data Detection (BDD) algorithms and lead to incorrect state estimation. This kind of attack is stealthy and widely known as an Undetected False Data Injection (UFDI) attack. Attackers are limited by different attributes, in terms of knowledge, capabilities, resources, and attack targets, that are important to consider for realizing the potential attack vectors and, thereby, the security measures. In this paper, we present a formal framework for automatic synthesis of security architectures that will guard the grid against potential UFDI attacks on state estimation. In this approach, we first formalize UFDI attacks with respect to the grid topology, electrical properties, and different attack attributes. The solution to the model derives the attack vectors that exist in the formalized scenario. These attack vectors are considered by a second formal model, the security architecture synthesis model, to design the security measures (i.e., a set of measurements to be protected against false data injection). We enhance the performance of the security architecture synthesis mechanism by performing parallel and stepped execution of the formal models. We demonstrate the proposed mechanism through case studies and evaluate the performance of the proposed model by running experiments on different IEEE test systems.