Using Formal Methods for Modelling Cyber-Physical Systems Security

Abstract

The recent years have witnessed an increasing integration of physical systems with information and communication technology (ICT). This emerging field is usually referred to as cyber-physical systems (CPS) and has generated a lot of attention. These systems are sometimes called real-time systems because they have stringent quality of service (QoS) requirements. Also, the coupling of the physical and the cyber components entails that any malicious activity in the cyber components would have a devastating effect on the physical components which in turn may endanger the lives of the humans and the environment. For this reason, some CPS are also known as safety-critical systems. The application of CPS spans through several domains including power stations, large interconnected infrastructure, traffic systems, etc. Thus, this thesis explored how these physical systems can be incorporated and formally modelled to be able to capture the behaviour of CPS, specifically under attack. First, this research focused on the communication channel while treating the internal state of CPS as a black box. The communication channel has been shown to be vulnerable to cyber attacks and for a number of these types of attacks, the timing behaviour and particularly the buffering capacity of the communication channel is critical. To address this problem, we employed queueing networks because they are appropriate models for capturing this sort of error conditions that leads to breaching of real-time constraints. We extended the existing models to include ways of representing the interaction of the different types of traffic and to understand how that can breach the QoS requirements. This is because the probability density function for the adversarial flow need not be the same as that of the regular traffic. We then applied one of the proposed models to study the effect of adversarial flow in software-defined industrial control networks. Moreover, there are scenarios where it is necessary to study the internal state for the internal behaviour of the CPS, which means this cannot be captured using a queueing network type of model. Our interest in this regard was to describe the internal behaviour of CPS in such a way that the asynchronous communication takes a prominent role. Hence, instead of having a model that relies on state machine, where we have global knowledge of the state; we employed process calculus model which effectively allowed us to look at the distributed state and how one state can influence another process including the uncertainty of the distributed state. We first developed an adversary model based on the process calculus model which allows reasoning over process states, placement of adversarial entities and communication behaviour. Then we extended the process calculus model by embedding an algebraic representation of Attack-Defence Trees (ADT) 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. Lastly, we expanded on the process calculus model to provide a finer grain model of the actual interactions inside the physical systems of CPS.