A Formal Approach to Cyber-Physical Attacks

Cyber-Physical Systems (CPSs) are integrations of networking and distributed computing systems with physical processes that monitor and control entities in a physical environment, with feedback loops where physical processes affect computations and vice versa. In this paper, we apply formal methods to lay and streamline theoretical foundations to reason about CPSs and cyber-physical attacks. We focus on a formal treatment of both integrity and DoS attacks to sensors and actuators of CPSs, paying particular attention to the timing aspects of these attacks. Our contributions are threefold: (1) we define a hybrid process calculus to model both CPSs and cyber-physical attacks; (2) we define a threat model of cyber-physical attacks and provide the means to assess attack tolerance/vulnerability with respect to a given attack; (3)~we formalise how to estimate the impact of a successful attack on a CPS and investigate possible quantifications of the success chances of an attack. We illustrate definitions and results by means of a non-trivial engineering application.