Threat Modelling of Cyber-Physical Systems Using an Applied Pi-Calculus

Abstract

Cyber–Physical Systems (CPS) are distributed systems in which the state of the physical system is generally not observable in non-trivial cases, and where state transitions of this physical system can also occur without resulting in immediate changes to observable variables. This poses challenges for the bidirectional synchronisation of the discrete cyber models and the partially continuous physical systems. Threats to CPS from cyber attacks are, however, often instantiable only where conditions on the CPS state during the attack meet certain conditions such that they drive the system state outside a desirable or safe space.

In this paper we propose an extension to an applied -calculus in which we can capture both the behaviour of the CPS as well as modelling possible adversary behaviour. This is achieved by embedding an algebraic representation of Attack–Defence Trees (ADT) in the applied -calculus and augmenting this by the addition of a partial ordering over the constituents of the ADT within the embedding, offering an elegant mechanism to extend ADT to ordering and time-related attacks. We illustrate the modelling approach for the case of an electrical substation fragment in which components communicate via the IEC 61850 protocol.