Detection of false data injection attacks on power grids
| datacite.contributor.RelatedPerson | Κωνσταντόπουλος, Γεώργιος | |
| datacite.contributor.RelatedPerson | Αλεξανδρίδης, Αντώνης | |
| datacite.contributor.Supervisor | Σερπάνος, Δημήτριος | |
| dc.contributor.author | Μαρόπουλος, Παρασκευάς | |
| dc.contributor.other | Maropoulos, Paraskevas | |
| dc.date.accessioned | 2026-07-09T11:33:56Z | |
| dc.date.available | 2026-07-09T11:33:56Z | |
| dc.date.issued | 2026-07-01 | |
| dc.degree | masterThesis | |
| dc.description.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 | |
| dc.description.translatedabstract | Τα σύγχρονα δίκτυα ηλεκτρικής ενέργειας αποτελούν κρίσιμη εθνική υποδομή, η αξιόπιστη λειτουργία της οποίας είναι απαραίτητη για τη λειτουργία νοσοκομείων, χρηματοπιστωτικών αγορών, συστημάτων επεξεργασίας νερού και της εθνικής άμυνας. Η αυξανόμενη ενσωμάτωση των συστημάτων εποπτικού ελέγχου και συλλογής δεδομένων (SCADA) με δίκτυα επικοινωνίας βασισμένα στο πρωτόκολλο IP έχει διευρύνει σημαντικά την επιφάνεια επίθεσης των δικτύων αυτών, ενώ τα παλαιότερα βιομηχανικά πρωτόκολλα ελέγχου παρέχουν ελάχιστη αυθεντικοποίηση ή κρυπτογράφηση. Οι επιθέσεις έγχυσης ψευδών δεδομένων (False Data Injection — FDI) αποτελούν την πλέον εξελιγμένη κατηγορία κυβερνοαπειλών κατά της εκτίμησης κατάστασης των δικτύων ηλεκτρικής ενέργειας. Σε αντίθεση με τις συμβατικές επιθέσεις εγκυρότητας δεδομένων, οι επιθέσεις FDI κατασκευάζονται μαθηματικά ώστε να βρίσκονται στον χώρο στηλών του Ιακωβιανού πίνακα μετρήσεων H, με αποτέλεσμα να παραμένουν αόρατες στον τυπικό έλεγχο υπολοίπων χ² της ανίχνευσης εσφαλμένων δεδομένων (BDD). Ένας επιτιθέμενος που γνωρίζει την τοπολογία του δικτύου μπορεί να μεταβάλει αθόρυβα την αντίληψη του χειριστή για την κατάσταση του συστήματος, οδηγώντας σε εσφαλμένες αποφάσεις κατανομής, οικονομική ζημία ή μη ασφαλείς συνθήκες λειτουργίας — χωρίς την ενεργοποίηση κανενός συναγερμού. Η παρούσα διπλωματική εργασία παρουσιάζει μια τυπική (formal), αυτοματοποιημένη μεθοδολογία για την επαλήθευση του κατά πόσον ένα δεδομένο σύστημα ηλεκτρικής ενέργειας είναι ευάλωτο σε επιθέσεις FDI. Η προσέγγιση εκφράζει το πρόβλημα ύπαρξης επίθεσης FDI ως ερώτημα ικανοποιησιμότητας επί της μη γραμμικής πραγματικής αριθμητικής χωρίς ποσοδείκτες (Quantifier-Free Nonlinear Real Arithmetic — QFNRA) και το επιλύει με τον dReal — έναν δ-πλήρη (delta-complete) επιλυτή SMT για μη γραμμικές θεωρίες επί των πραγματικών αριθμών. Οι πλήρεις εξισώσεις ροής ισχύος εναλλασσόμενου ρεύματος (AC), συμπεριλαμβανομένων τόσο των ενεργών όσο και των αέργων ροών κλάδων, κωδικοποιούνται ως περιορισμοί QFNRA. Μια αποσύνθεση ελεύθερων/καθηλωμένων ζυγών (free/pinned) μειώνει τη διάσταση του προβλήματος, δηλώνοντας ως μεταβλητές SMT μόνο τους ζυγούς εντός ακτίνας BFS r από τον ζυγό-στόχο, ενώ όλοι οι υπόλοιποι ζυγοί καθηλώνονται ως αριθμητικές σταθερές που προκύπτουν από λύση ροής ισχύος Newton-Raphson. Με τον τρόπο αυτό διατηρείται η πλήρης ακρίβεια της φυσικής AC, ενώ ταυτόχρονα το πρόβλημα καθίσταται υπολογιστικά διαχειρίσιμο. Η δομή της εργασίας συνοψίζεται ως εξής: Το Κεφάλαιο 1 εισάγει το κίνητρο της εργασίας, αναδεικνύοντας το δίκτυο ηλεκτρικής ενέργειας ως κρίσιμη υποδομή, επισκοπεί το τοπίο των κυβερνοαπειλών και διατυπώνει το ερευνητικό πρόβλημα, τους στόχους και τις συνεισφορές της εργασίας. Το Κεφάλαιο 2 επισκοπεί τη βιβλιογραφία σχετικά με την εκτίμηση κατάστασης συστημάτων ηλεκτρικής ενέργειας, την ανίχνευση εσφαλμένων δεδομένων, την αρχική διατύπωση των επιθέσεων FDI των Liu et al., τις επεκτάσεις AC και τον ρόλο των τυπικών μεθόδων, καθώς και τους επιλυτές SMT και τον dReal. Το Κεφάλαιο 3 παρουσιάζει το μοντέλο του συστήματος και την τυπική διατύπωση του προβλήματος, συμπεριλαμβανομένων των εξισώσεων ροής ισχύος AC, της εκτίμησης κατάστασης υπό επίθεση και της τυπικής διατύπωσης του προβλήματος FDI με τις τρεις κατηγορίες περιορισμών: μη ανιχνευσιμότητα, φυσική εφικτότητα και λειτουργικός αντίκτυπος. Το Κεφάλαιο 4 περιγράφει αναλυτικά την κωδικοποίηση SMT: την αποσύνθεση ελεύθερων/καθηλωμένων ζυγών, τις δηλώσεις μεταβλητών και τα όριά τους, τους περιορισμούς κλάδων AC και εγχύσεων ζυγών (νόμος του Kirchhoff), τους περιορισμούς μη ανιχνευσιμότητας και αντικτύπου, τη δημιουργία αρχείων SMT2 και τη διαμόρφωση του επιλυτή. Το Κεφάλαιο 5 παρουσιάζει τα πειραματικά αποτελέσματα στα τρία πρότυπα συστήματα δοκιμών IEEE (14, 57 και 68 ζυγών), τις πειραματικές παραμέτρους, την επιλογή ζυγών-στόχων, την υπολογιστική υποδομή και τη συγκριτική ανάλυση μεταξύ των συστημάτων. Το Κεφάλαιο 6 συζητά τις επιπτώσεις των αποτελεσμάτων: την τοπολογία ως προγνωστικό παράγοντα ευπάθειας, την αποτελεσματικότητα και την πληρότητα της αποσύνθεσης ελεύθερων/καθηλωμένων ζυγών, το όριο κλιμακωσιμότητας, τη σύγκριση με προσεγγίσεις βασισμένες στο μοντέλο DC και τους περιορισμούς της μεθόδου. Το Κεφάλαιο 7 ολοκληρώνει την εργασία με σύνοψη των συνεισφορών και κατευθύνσεις για μελλοντική έρευνα, όπως η αυξητική επίλυση SMT, το σπάσιμο συμμετριών, η θερμή εκκίνηση από χαλαρώσεις DC, η επέκταση σε μεγαλύτερα πρότυπα συστήματα, η μοντελοποίηση αμυντικών αντιμέτρων και η δυναμική μοντελοποίηση επιθέσεων. Η μέθοδος επικυρώνεται στα τρία πρότυπα συστήματα αναφοράς IEEE: τα δίκτυα των 14, 57 και 68 ζυγών. Σε 27 συνδυασμούς (ζυγός-στόχος, ακτίνα), ο dReal επιστρέφει δ-sat — θετική απόδειξη ύπαρξης επίθεσης — στο 60% των περιπτώσεων για τα συστήματα των 14 και 57 ζυγών και στο 100% των περιπτώσεων για r=0 στο σύστημα των 68 ζυγών. Το πιο ενδεικτικό αποτέλεσμα, ο Ζυγός 9 του δικτύου των 68 ζυγών, παραμένει ευάλωτος σε επίθεση για r=3, με 12 ελεύθερες μεταβλητές και χρόνο επίλυσης περίπου 18,4 δευτερολέπτων. Τα πειραματικά αποτελέσματα επιβεβαιώνουν ότι ο βαθμός συνδεσιμότητας των ζυγών και η πυκνότητα πλέγματος του δικτύου αποτελούν τους βασικούς καθοριστικούς παράγοντες ευπάθειας: περιφερειακοί ζυγοί χαμηλού βαθμού είναι ευάλωτοι με μόνο δύο ελεύθερες μεταβλητές, ενώ η πυκνότερη τοπολογία πλέγματος του δικτύου των 68 ζυγών καθιστά εφικτές επιθέσεις σε κάθε δοκιμασμένο ζυγό. Οι συνεισφορές της παρούσας εργασίας είναι: – Μια πλήρης κωδικοποίηση SMT AC με αποσύνθεση ελεύθερων/καθηλωμένων ζυγών – Πειραματικός χαρακτηρισμός ευπάθειας σε τρία πρότυπα συστήματα αναφοράς – Μια τυπική περιγραφή της σχέσης μεταξύ τοπολογίας, ακτίνας BFS και επιλυσιμότητας από τον επιλυτή | |
| dc.identifier.uri | https://hdl.handle.net/10889/32441 | |
| dc.language.iso | en | |
| dc.rights | Attribution-NoDerivs 3.0 Greece | en |
| dc.rights.uri | http://creativecommons.org/licenses/by-nd/3.0/gr/ | |
| dc.subject | False data injection (FDI) attacks | |
| dc.subject | SMT solving (dReal) | |
| dc.subject | Power system state estimation | |
| dc.subject.alternative | Επιθέσεις έγχυσης ψευδών δεδομένων | |
| dc.subject.alternative | Επίλυση ικανοποιησιμότητας με δ-πλήρη επιλυτή για μη γραμμική πραγματική αριθμητική | |
| dc.subject.alternative | Εκτίμηση κατάστασης δικτύων ηλεκτρικής ενέργειας | |
| dc.title | Detection of false data injection attacks on power grids | |
| dc.title.alternative | Ανίχνευση επιθέσεων ψευδών δεδομένων σε ηλεκτρικά δίκτυα |