Formal Modelling of the Impact of Cyberattacks on Safety of Networked Control Systems
Tid: To 2025-05-08 kl 14.00
Plats: F3 (Flodis), Lindstedtsvägen 26 & 28, Campus
Språk: Engelska
Ämnesområde: Datalogi
Respondent: Ehsan Poorhadi , Teoretisk datalogi, TCS
Opponent: Professor Yamine Aït Ameur, IRIT/INPT-ENSEEIHT, University of Tolouse, France
Handledare: Professor Elena Troubitsyna, Teoretisk datalogi, TCS
QC 20250417
Abstract
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.