Detection of false data injection attacks on power grids
Loading...
Date
2026-07-01
Authors
Μαρόπουλος, Παρασκευάς
Journal Title
Journal ISSN
Volume Title
Publisher
Abstract
Current power grids represent critical national infrastructure whose reliable operation is required for the functioning of hospitals, financial markets, water treatment systems, and national defence. The increasing integration of Supervisory Control and Data Acquisition (SCADA) systems with IP-based communication networks has vastly expanded the attack surface of these grids while legacy industrial control protocols supply little authentication or encryption.
False Data Injection (FDI) attacks represent the most sophisticated class among cyber threats to power grid system estimation. Unlike conventional data validity attacks, FDI attacks are mathematically constructed to lie in the column space of the measurement Jacobian matrix H, rendering them invisible to the standard chi-squared (chi2) bad data detection (BDD) residual test. An adversary who knows the network topology[21] can silently shift the operator's perception of the system state, resulting in incorrect dispatch decisions, economic harm, or unsafe operating conditions — without triggering any alarms.
This thesis presents a formal, automated methodology for verifying whether a given power system is vulnerable to FDI attacks. The approach expresses the FDI attack existence problem as a satisfiability query over Quantifier-Free Nonlinear Real Arithmetic (QFNRA)[19] and solves it using dReal — a delta-complete SMT solver for nonlinear theories over the reals. The full AC power flow equations, including both active and reactive branch flows, are encoded as QFNRA constraints. A free/pinned bus decomposition reduces problem dimensionality by declaring only buses within a BFS radius r of the target as SMT variables, while pinning all remaining buses as numeric constants obtained from a Newton-Raphson power flow solution. This preserves full AC physics accuracy as making the problem tractable.
The thesis is organised as follows:
Chapter 1 introduces the motivation for protecting the power grid as critical infrastructure, surveys the cyber threat landscape, and formulates the research problem, objectives and contributions of the thesis.
Chapter 2 reviews the background literature on power system state estimation, bad data detection, the original FDI attack formulation of Liu et al., AC extensions and the role of formal methods, as well as SMT solvers and dReal.
Chapter 3 presents the system model and the formal problem statement, including the AC power flow equations, state estimation under attack, and the formal FDI problem formulation with its three constraint classes: stealth, physical feasibility, and operational impact.
Chapter 4 details the SMT-based encoding: the free/pinned bus decomposition, variable declarations and bounds, AC branch and bus injection constraints (Kirchhoff’s law), the stealth and impact constraints, SMT2 file generation, and solver configuration.
Chapter 5 presents the experimental results for the three IEEE benchmark test systems (14-bus, 57-bus and 68-bus), the experimental parameters, target bus selection, computational infrastructure, and the comparative analysis between the systems.
Chapter 6 discusses the implications of the results: topology as a vulnerability predictor, the effectiveness and completeness of the free/pinned decomposition, the scalability ceiling, the comparison with DC-based approaches, and the limitations of the method.
Chapter 7 concludes the thesis with a summary of contributions and directions for future work, including incremental SMT solving, symmetry breaking, warm-starting from DC relaxations, extension to larger benchmark systems, modelling of defender countermeasures, and dynamic attack modelling.
The method is validated on three IEEE benchmark setups: the 14-bus, 57-bus, and 68-bus networks. Across 27 (target bus, radius) combinations, dReal returns delta-sat — a positive proof of attack existence — in 60% of cases for the 14-bus and 57-bus systems, and in 100% of cases at r=0 for the 68-bus system. The most permissive result, Bus 9 of the 68-bus network, remains attackable at r=3 with 12 free variables and a solve time of approximately 18.4 seconds. The experimental results confirm that bus degree and network mesh density are the primary determinants of vulnerability: low-degree peripheral buses are attackable with only two free variables, while the denser 68-bus mesh topology enables attacks at every tested bus.
The contributions of this work are:
A complete AC SMT encoding with free/pinned bus decomposition
Experimental vulnerability characterisation across three benchmark setups
A formal account of the relationship among topology, BFS radius, and solver tractability
Description
Keywords
False data injection (FDI) attacks, SMT solving (dReal), Power system state estimation