Impact Analysis of Coordinated Cyber-physical Attacks via Statistical Model Checking: A Case Study

We use Uppaal SMC to analyze a non-trivial coordinated multi-engine system equipped with both a tamperproof distributed intrusion detection system (IDS) and a tamperproof supervisor component to mitigate eventual loss of performance. We rely on statistical model checking to evaluate the impact of three coordinated cyber-physical attacks targeting all controllers of the multi-engine system, and aiming at compromising the performance of the whole system. Here, the coordination of the attackers via a covert channel is a necessary requirement to achieve the desired malicious goals. Our security analysis provide an estimate of both the physical impact of the attacks on the system and the effectiveness of the IDS.