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

Cyber-Physical Systems are exposed to cyber-physical attacks, i.e., security breaches in cyberspace that alter the underlying physical processes. 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 injecting malicious code in all controllers of the multi-engine system to compromise the performance of the whole system. Here, the coordination of the attackers is a necessary requirement to achieve the desired malicious goals. Our security analysis provides an estimate of both the physical impact of the attacks on the physical process of the system and the effectiveness of the IDS. We believe that by assessing the impact of attacks, system engineers may understand whether they have to develop more accurate impact metrics or focus on different invariants to enhance their IDSs in order to detect such attacks.