Modern control systems provide services that are indispensable for society, e.g., transportation, energy production, healthcare etc. Hence, it is important to guarantee safe and reliable functioning of such systems. However, they are increasingly relying on networking technologies, which makes them susceptible to cyberattacks that could potentially jeopardise their safety. Moreover, such systems typically have a complex distributed architecture and dynamic behaviour. Hence, it is hard to ensure correctness and safety of their design. Formal methods are used to tackle system complexity and guarantee correctness of the design via abstract mathematical modelling and rigorous verification. Various formal modelling techniques have been successfully used in the design of safety-critical systems in different domains. However, they primarily focused on modelling and verification of system safety. Since modern safety-critical systems are increasingly becoming the subject of cyberattacks, formal modelling techniques should be extended to address the emerging problem of safety-security interactions. In this thesis, we propose a rigorous approach to modelling the impact of cyberattacks on safety of networked control systems. Our approach integrates graphical modelling in Systems Modelling Language – SysML and formal specification and verification in the Event-B framework. Graphical models provide support in visualising system architecture and interactions between the components as well as facilitate the analysis of safety and security interactions by the interdisciplinary teams. Modelling and proof- based verification in Event-B allows us to formally identify the cyberattacks that jeopardise system safety. To bridge the gap between the graphical and formal modelling, we developed software automatically translating graphical system models into formal specifications in Event-B. We believe that this thesis makes both theoretical and practical contributions towards an integration of safety and security engineering, which is necessary for the development of modern trustworthy networked control systems.

Moderna reglersystem tillhandahåller tjänster som är oumbärliga för samhället, t.ex. transport, energiproduktion, hälso- och sjukvård etc. Därför är det viktigt att garantera att sådana system fungerar säkert och tillförlitligt. De använder dock i allt högre grad nätverksteknik, vilket gör dem mottagliga för cyberattacker som potentiellt kan äventyra deras säkerhet. Dessutom har sådana system vanligtvis komplex distribuerad arkitektur och dynamiskt beteende. Därför är det svårt att säkerställa att deras design är korrekt och säker. Formella metoder används för att hantera systemkomplexitet och garantera att designen är korrekt via abstrakt matematisk modellering och rigorös verifiering. Olika formella modelleringstekniker har framgångsrikt använts vid design av trygghet-kritiska system inom olika domäner. För närvarande kräver användningen av nätverksteknik en utvidgning av denna teknik för att ta itu med det framväxande problemet med interaktion mellan trygghet och säkerhet. I den här avhandlingen föreslår vi ett rigoröst tillvägagångssätt för modellering av effekterna av cyberattacker på trygghet i nätverksanslutna styrsystem. Vårt tillvägagångssätt integrerar grafisk modellering i Systems Modelling Language – SysML och formell specifikation och verifiering i Event- B-ramverket. Grafiska modeller ger stöd för att visualisera systemarkitektur och interaktioner mellan komponenterna samt underlättar analysen av säkerhets- och trygghetsinteraktioner av de tvärvetenskapliga teamen. Modellering och bevisbaserad verifiering i Event-B gör det möjligt för oss att formellt identifiera de cyberattacker som äventyrar systems trygghet. För att överbrygga klyftan mellan den grafiska och formella modelleringen utvecklade vi en programvara som automatiskt översätter grafiska systemmodeller till formella specifikationer i Event-B. Vi tror att denna avhandling ger både teoretiska och praktiska bidrag till en integration av säkerhets- och trygghetsteknik, vilket är nödvändigt för utvecklingen av moderna pålitliga nätverksbaserade reglersystem.  

Nowadays safety-critical systems extensively rely on networking technologies to implement various monitoring and control functions. Therefore, system safety and security become intertwined, i.e. cyberattacks might result in a violation of safety requirements. To enable a holistic analysis of the impact of cyberattacks on safety, we propose an automated integrated approach that facilitates the analysis of safety-security interactions using SysML and Event-B. Our modelling guidelines support an explicit representation of system behaviour during a cyberattack in SysML. A translation and subsequent refinement in Event-B enable the discovery of violated safety requirements via formal proof-based verification. In this paper, we focus on discussing the developed automated tool support - EBSysMLSec that enables a holistic model-based analysis of safety-security interactions.

Over recent years, the number of cyberattacks on safety-critical systems, including railways has been rapidly increasing. To analyze the impact of cyberattacks on safety, we need to create methods supporting a systematic and rigorous analysis of system behavior in the presence of cyber threats. In this paper, we propose a methodology and automated tool support for an integrated analysis of the impact of cyberattacks on the safety of railway systems. Our approach relies on graphical modeling in SysML, HAZOP-based analysis of cyber threats and formal modeling in Event-B. The proposed approach allows the designers to identify and visualize the safety requirements that become violated as a result of various cyberattacks.

Safety-critical control systems increasingly rely on networking technologies, which makes these systems vulnerable to cyber attacks that can potentially jeopardise system safety. To achieve safe- and secure-by-construction development, the designers should analyse the impact of security attacks already at the modelling stage. Since SysML is often used for modelling safety-critical systems, in this paper, we propose to integrate modelling in SysML and Event-B to enable reasoning about safety-security interactions at system modelling stage. Our approach combines the benefits of graphical modelling in SysML with the mathematical rigor of Event-B to visualise and formalise the analysis of the impact of security attacks on system safety.

Modern railway signaling extensively relies on wireless communication technologies for efficient operation. The communication infrastructures that they rely on are increasingly based on standardized protocols and are shared with other users. As a result, it has an increased attack surface and is more likely to become the target of cyber attacks that can result in loss of availability and, in the worst case, in safety incidents. While formal modeling of safety properties has a well-established methodology in the railway domain, the consideration of security vulnerabilities and the related threats lacks a framework that would allow a formal treatment. In this paper, we develop a modeling framework for the analysis of the potential of security vulnerabilities to jeopardize safety in communications-based train control for railway signaling, focusing on the recently introduced moving block system. We propose a refinement-based approach enabling a structured and rigorous analysis of the impact of security on system safety.

Modern safety-critical systems become increasingly networked and interconnected. Often the communication between the system components utilises the protocols similar to the standard Internet Protocol (IP). In particular, such protocols are used for communication between smart sensors and controller. While offering advanced capabilities such as remote diagnostics and maintenance, this also make safety-critical systems susceptible to the attacks implementable against IP-based systems. In this paper, we propose an approach to specifying a generic IP-based networked control system and formalising its security properties. We use the Event-B framework to formally analyse the impact of security attacks on safety properties of the system.