Cyber-Safety Assessment of Wind Turbines: A Reachability Analysis Approach Against Cyber-Attacks

Cyber threats to Wind Power Plants (WPPs) are progressively rising as they often rely heavily on numerous digital assets and interconnected control systems. This makes WPPs more attractive to cybercriminals, as sabotaging these facilities can disrupt grid stability and energy supply. Most risk analyses of WPPs use informal frameworks or simulations, which can miss rare but critical scenarios, especially during cyberattacks, due to their non-exhaustive nature. This can compromise both security and safety. However, formal methods like model checking and theorem proving provide us with guarantees to ensure safety and stability. This paper presents the application of formal methods, particularly reachability analysis, to highlight the risks associated with wind plants. The focus is on model-based safety analysis of a wind turbine, including its pitch control system, with an emphasis on scenarios involving cyberattacks. We model the wind turbine system as a hybrid automaton based on its different control regions. We then perform reachability analysis of the hybrid automaton to examine all system states over a finite horizon, thus addressing the verification challenges inherent in such nonlinear dynamical systems. We identify vulnerabilities present in the system that attackers may exploit to cause harm to the plant. We conclude by discussing the impact of two different cyber attacks on the safety of the system.