https://www.mdu.se/

The combination of physical assets with cyber computational entities, known as Cyber-Physical Systems (CPS), is becoming more common. These systems are used in various sectors such as manufacturing, energy production, and transportation. However, they may contain vulnerabilities that can be exploited and compromise the proper functioning of the systems. Formal methods can provide confidence in the correctness of the system. These methods can help system designers to discover vulnerabilities and ensure the system meets its intended behavior and properties.

This thesis presents a framework called CRYSTAL for analyzing the security of CPS both at the design and runtime with the following contributions: 1) We build a Timed Rebeca model augmented with attack scenarios to identify potential vulnerabilities during the design phase. We identify CPS-related attacks reported in the literature and use STRIDE threat modeling as a guideline to put them into two categories: attacks on communication and attacks on components. We augment our model with actors representing attackers that jeopardize the communication and compromised components with possible malfunctions. Subsequently, we analyze the security of the CPS design (i.e., a model augmented with attacks) using model checking and identifying the trace of events leading to a security failure (i.e., counterexamples). 2) We propose a model-based methodology for detecting attacks at runtime. We develop a monitor and an algorithm that checks whether the behavior of the system at runtime is consistent with a reference model. We call the reference model as Tiny Digital Twin and it is employed within the monitor. We create Tiny Digital Twin by automatically reducing the state space of the Timed Rebeca model while preserving the trace equivalence. 3) We provide a formal foundation for our abstraction method and present a theory to map the state space of a Timed Rebeca model into a Labeled Transition System (LTS). This is achieved by defining a Concise Rebeca Timed Transition System (CRTTS) and implementing a function to convert CRTTS into an LTS. We use mCRL2 ltsconvert tool to abstract away non-observable actions from LTS while preserving trace equivalence between the original model and its abstracted version. 4) To validate the effectiveness of our attack detection method we simulate various attacks. Subsequently, we systematically model and check complex coordinated attacks. The applicability of CRYSTAL is demonstrated in revealing malicious behavior within different case studies including Pneumatic Control System (PCS), Temperature Control System (TCS), and Secure Water Treatment System (SWaT).

Kombinationen av fysiska tillgångar med cyberberäkningsentiteter, kända som cyber-fysiska system (CPS), blir allt vanligare. Dessa system används inom olika sektorer som tillverkning, energiproduktion och transport. Dock kan de innehålla sårbarheter som kan utnyttjas och negativt påverka systemens korrekta funktion. Formella metoder kan ge förtroende för korrektheten hos system. Dessa metoder kan hjälpa systemdesigners att upptäcka sårbarheter och säkerställa att systemet uppfyller sina avsedda beteenden och egenskaper. Denna avhandling presenterar ett ramverk kallat CRYSTAL för att analysera säkerheten hos CPS både vid design och drift med följande bidrag: 1) Vi bygger en Tidsberoende Rebeca-modell med attackerade scenarier för att identifiera potentiella sårbarheter under designfasen. Vi identifierar CPS-relaterade attacker rapporterade i litteraturen och använder STRIDE-hotmodellering som riktlinje för att placera dem i två kategorier: attacker på kommunikation och attacker på komponenter. Vi utökar vår modell med aktörer, en angripare som hotar kommunikationen och systemets komprometterade komponenter med möjliga fel. Därefter analyserar vi säkerheten hos CPS-designen (dvs en modell utökad med attacker) genom att använda model-checking och identifierar händelseförlopp som leder till säkerhetsfel (d.v.s. kontraexempel). 2) Vi föreslår en modellbaserad metod för att upptäcka attacker vid drifttid. Vi utvecklar en övervakare och en algoritm som kontrollerar om systemets beteende vid drifttid är förenligt med en referensmodell. Vi kallar en referensmodell för Tiny Digital Twin och den används inom övervakaren. Vi skapar en Tiny Digital Twin genom att automatiskt minska tillståndsutrymmet för den tidsberoende Rebeca-modellen medan vi bevarar exekveringslikhet. 3) Vi tillhandahåller en formell grund för vår abstraktionsmetod och presenterar en teori för att kartlägga tillståndsutrymmet för en Tidsberoende Rebeca-modell till ett Labeled Transition System (LTS). Detta uppnås genom att definiera ett Concise Rebeca Timed Transition System (CRTTS) och genomföra en funktion för att konvertera CRTTS till ett LTS. Vi använder mCRL2 ltsconvert-verktyget för att abstrahera bort icke-observerbara åtgärder från LTS medan vi bevarar exekveringslikhet mellan den ursprungliga modellen och dess abstrakta version. 4) För att validera effektiviteten hos vår attackdetektionsmetod simulerar vi olika attacker. Därefter modellerar och kontrollerar vi systematiskt komplexa samordnade attacker. CRYSTAL:s användbarhet demonstreras genom att avslöja skadligt beteende inom olika fallstudier inklusive ett Pneumatiskt Kontrollsystem (PCS), Temperaturkontrollsystem (TCS) och Säker Vattenbehandlingsanläggning (SWaT).