| Title | Real-Time SCADA Attack Detection by Means of Formal Methods |
| Publication Type | Conference Paper |
| Year of Publication | 2019 |
| Authors | Mercaldo, Francesco, Martinelli, Fabio, Santone, Antonella |
| Conference Name | 2019 IEEE 28th International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises (WETICE) |
| Date Published | jun |
| Keywords | Automata, automata theory, chemical manufacturing plants, chemical substances, Chemicals, Clocks, compositionality, control smart grid, critical infrastructure, critical infrastructures, critical machines, formal methods, Human Behavior, model checking, programmable controllers, programmable logic controller, pubcrawl, real-time SCADA attack detection, Resiliency, Safety, SCADA, SCADA control systems, SCADA systems, SCADA Systems Security, SCADA water distribution system, security, security of data, Semantics, temporal logic, timed automata, timed automaton, timed temporal logic, water supply |
| Abstract | SCADA control systems use programmable logic controller to interface with critical machines. SCADA systems are used in critical infrastructures, for instance, to control smart grid, oil pipelines, water distribution and chemical manufacturing plants: an attacker taking control of a SCADA system could cause various damages, both to the infrastructure but also to people (for instance, adding chemical substances into a water distribution systems). In this paper we propose a method to detect attacks targeting SCADA systems. We exploit model checking, in detail we model logs from SCADA systems into a network of timed automata and, through timed temporal logic, we characterize the behaviour of a SCADA system under attack. Experiments performed on a SCADA water distribution system confirmed the effectiveness of the proposed method. |
| DOI | 10.1109/WETICE.2019.00057 |
| Citation Key | mercaldo_real-time_2019 |
Real-Time SCADA Attack Detection by Means of Formal Methods