If a Tree Falls in the Forest: Risk Logics for Safety-Security Analysis

New technology comes with new risks: self-driving cars or train automation systems may get hacked, people depend on medical implants not malfunctioning for their continued health. This is true both in the domain of safety – i.e., the absence of risk connected with unintentional malfunctions/faults – and security – i.e., the absence of risk linked with intentional attacks.

Safety and security can be heavily intertwined. Measures that increase safety may decrease security and vice versa: smart IoT sensors offer ample opportunities to monitor the safety of power plants and wind turbines, but their many access points are notorious for enabling hackers to enter the system. When considering the intertwined nature of safety-security risk management, one overarching challenge stands out: decision making. How to effectively evaluate which risks are most threatening, and which countermeasures are most (cost-)effective? These decisions are notoriously hard to take: it is well-understood – e.g., from research by Nobel prize winner Daniel Kahneman – that people have very poor intuitions for risks and probability, especially when taking decisions in a hurry.

In this thesis, we foster transparent, systematic and objective decision making by developing a compositional framework to reason about safety-, security- and joint safety-security risks. We empower practitioners with the ability to 1. model systems with sufficient expressiveness; 2. query their models with flexible yet powerful languages; and 3. check whether their models exhibit (un)desirable characteristics. To do so, we leverage already established formal models for risk assessment – such as fault trees and attack trees – and develop powerful yet understandable logics that can reason about qualitative and quantitative aspects of risk, such as failure probabilities, success, cost and time of (cyber)attacks. In addition, we develop intermediate query languages to propel usability, and state-of-the-art model checking algorithms to verify safety-security properties of these models. Finally, we explore cross-fertilization between this framework and conceptual analyses from the field of risk ontology and offer prototypical tool support to promote usage of our methods.