Model checking for real-time attack detection in water distribution systems

Water distribution systems represents critical infrastructures. These architectures are really critical and an irregular behaviour can be reflected in human safety. As a matter of fact, an attacker obtaining the control of such of an architecture is able to perpetrate a plethora of damages, both to the infrastructure but also to people. In this paper, we propose an approach to identify irregular behaviours focused on water distribution systems. The designed approach considers formal verification environment. The logs retrieved from water distribution systems are parsed into a formal model and, by exploiting timed temporal logic, we characterize the behaviour of a water distribution system while an attack is happening. The evaluation, referred to a water distribution system, confirmed the effectiveness of the designed approach in the identification of three different irregular behaviours.