https://www.mdu.se/

mdu.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Automated Vulnerability Discovery and Attack Detection Framework for Cyber-Physical Systems
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems. (Cyber-Physical Systems Analysis)
2024 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

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).

Abstract [sv]

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). 

Place, publisher, year, edition, pages
Västerås: Mälardalens universitet, 2024.
Series
Mälardalen University Press Dissertations, ISSN 1651-4238 ; 407
National Category
Computer Systems
Research subject
Computer Science
Identifiers
URN: urn:nbn:se:mdh:diva-66422ISBN: 978-91-7485-646-0 (print)OAI: oai:DiVA.org:mdh-66422DiVA, id: diva2:1851381
Public defence
2024-06-07, Omega, Mälardalens universitet, Västerås, 13:15 (English)
Opponent
Supervisors
Funder
Swedish Foundation for Strategic ResearchAvailable from: 2024-04-15 Created: 2024-04-14 Last updated: 2024-05-17Bibliographically approved
List of papers
1. On-Off Attack on a Blockchain-based IoT System
Open this publication in new window or tab >>On-Off Attack on a Blockchain-based IoT System
Show others...
2019 (English)In: IEEE International Conference on Emerging Technologies and Factory Automation, ETFA, Institute of Electrical and Electronics Engineers Inc. , 2019, p. 1768-1773Conference paper, Published paper (Refereed)
Abstract [en]

There is a growing interest in using the Blockchain for resolving IoT security and trustworthiness issues existing in today's complex systems. Blockchain concerns trust in peer to peer networks by providing a distributed tamper-resistant ledger. However, the combination of these two emerging technologies might create new problems and vulnerabilities that attackers might abuse.In this paper, we aim to investigate the trust mechanism of Lightweight Scalable BlockChain (LSB), that is a Blockchain specifically designed for Internet of Things networks, to show that a malicious participant in a Blockchain architecture have possibility to pursue an On-Off attack and downgrade the integrity of the distributed ledger. We choose a remote software update process as an instance to represent this violation. Finally, using the actor-based language Rebeca, we provide a model of a system under attack and verify the described attack scenario.

Place, publisher, year, edition, pages
Institute of Electrical and Electronics Engineers Inc., 2019
Keywords
Blockchain, Distributed Trust, IoT, On-Off Attack, Security, Factory automation, Network security, Peer to peer networks, Attack scenarios, Emerging technologies, Malicious participant, Software updates, Tamper resistant, Internet of things
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:mdh:diva-46532 (URN)10.1109/ETFA.2019.8868238 (DOI)000556596600280 ()2-s2.0-85074214755 (Scopus ID)9781728103037 (ISBN)
Conference
24th IEEE International Conference on Emerging Technologies and Factory Automation, ETFA 2019, 10 September 2019 through 13 September 2019
Available from: 2019-12-17 Created: 2019-12-17 Last updated: 2024-04-14Bibliographically approved
2. An Actor-based Approach for Security Analysis of Cyber-Physical Systems
Open this publication in new window or tab >>An Actor-based Approach for Security Analysis of Cyber-Physical Systems
Show others...
2020 (English)In: Formal Methods for Industrial Critical Systems, FMICS 2020, Lecture Notes in Computer Science, vol 12327, Springer, 2020, p. 130-147, article id 12327Conference paper, Published paper (Refereed)
Place, publisher, year, edition, pages
Springer, 2020
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 12327
National Category
Engineering and Technology Computer Systems
Identifiers
urn:nbn:se:mdh:diva-49979 (URN)10.1007/978-3-030-58298-2_5 (DOI)000884747200005 ()2-s2.0-85091308994 (Scopus ID)978-3-030-58297-5 (ISBN)978-3-030-58298-2 (ISBN)
Conference
25th International Conference on Formal Methods for Industrial Critical Systems FMICS20, 02 Sep 2020, Vienna, Austria
Projects
Serendipity - Secure and dependable platforms for autonomy
Available from: 2020-09-29 Created: 2020-09-29 Last updated: 2024-04-14Bibliographically approved
3. Monitoring Cyber-Physical Systems Using a Tiny Twin to Prevent Cyber-Attacks
Open this publication in new window or tab >>Monitoring Cyber-Physical Systems Using a Tiny Twin to Prevent Cyber-Attacks
Show others...
2022 (English)In: Lecture Notes in Computer Science, vol. 13255, Springer Science and Business Media Deutschland GmbH , 2022, p. 24-43Conference paper, Published paper (Refereed)
Abstract [en]

We propose a method to detect attacks on sensors and controllers in cyber-physical systems. We develop a monitor that uses an abstract digital twin, Tiny Twin, to detect false sensor data and faulty control commands. The Tiny Twin is a state transition system that represents the observable behavior of the system from the monitor point of view. At runtime, the monitor observes the sensor data and the control commands, and checks whether the observed data and commands are consistent with the state transitions in the Tiny Twin. The monitor produces an alarm when an inconsistency is detected. We model the components of the system and the physical processes in the Rebeca modeling language and use its model checker to generate the state space. The Tiny Twin is built automatically by reducing the state space, keeping the observable behavior of the system, and preserving the trace equivalence. We demonstrate the method and evaluate it in detecting attacks using a temperature control system. 

Place, publisher, year, edition, pages
Springer Science and Business Media Deutschland GmbH, 2022
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 13255 LNCS
Keywords
Abstraction, Attack detection and prevention, Cyber-physical systems, Cyber-security, Model checking, Monitoring, Cyber Physical System, Cybersecurity, Embedded systems, Modeling languages, Network security, Attack detection, Attack prevention, Control command, Cybe-physical systems, Cyber security, Models checking, Observable behavior, Sensors data
National Category
Robotics
Identifiers
urn:nbn:se:mdh:diva-59941 (URN)10.1007/978-3-031-15077-7_2 (DOI)000874749700002 ()2-s2.0-85137039734 (Scopus ID)9783031150760 (ISBN)
Conference
28th International Symposium on Model Checking Software, SPIN 2022, Virtual, Online, 21 May, 2022
Available from: 2022-09-14 Created: 2022-09-14 Last updated: 2024-04-14Bibliographically approved
4. Tiny Twins for detecting cyber-attacks at runtime using concise Rebeca time transition system
Open this publication in new window or tab >>Tiny Twins for detecting cyber-attacks at runtime using concise Rebeca time transition system
2024 (English)In: Journal of Parallel and Distributed Computing, ISSN 0743-7315, E-ISSN 1096-0848, Vol. 184, article id 104780Article in journal (Refereed) Published
Abstract [en]

This paper presents a method for detecting cyber-attacks in cyber-physical systems using a monitor. The method employs an abstract model called Tiny Twin, which is built at design time and is used at runtime to detect inconsistencies. Tiny Twin is a state transition system that represents the observable behavior of the system from the monitor point of view. We model the behavior of the system in the Rebeca modeling language and use Afra model checker to generate the state space. The Tiny Twin is built automatically, by abstracting the state space while keeping the observable actions and preserving the trace equivalence. For doing that we had to solve the complexities in the state space introduced by time-shifts, nondeterministic assignments and abstraction of internal actions. We formally define the state space as Concise Rebeca Timed Transition System (CRTTS), and then map CRTTS to an LTS. The LTS is then fed to a tool to abstract away the non-observable actions.

Place, publisher, year, edition, pages
Academic Press Inc., 2024
Keywords
Cyber-security, Intrusion detection systems, Model abstraction, Model checking, Runtime monitoring, Abstracting, Computer crime, Crime, Cyber attacks, Cyber Physical System, Embedded systems, Intrusion detection, Modeling languages, Network security, Cyber security, Cyber-attacks, Models checking, Runtimes, State-space, Time transition, Timed transition systems
National Category
Computer Systems
Identifiers
urn:nbn:se:mdh:diva-64590 (URN)10.1016/j.jpdc.2023.104780 (DOI)001099111600001 ()2-s2.0-85173631477 (Scopus ID)
Available from: 2023-10-30 Created: 2023-10-30 Last updated: 2024-04-14Bibliographically approved
5. CRYSTAL framework: Cybersecurity assurance for cyber-physical systems
Open this publication in new window or tab >>CRYSTAL framework: Cybersecurity assurance for cyber-physical systems
Show others...
2024 (English)In: The Journal of logical and algebraic methods in programming, ISSN 2352-2208, E-ISSN 2352-2216, ISSN 2352-2208, Vol. 139Article in journal (Refereed) Published
Abstract [en]

We propose CRYSTAL framework for automated cybersecurity assurance of cyber-physical systems (CPS) at design-time and runtime. We build attack models and apply formal verification to recognize potential attacks that may lead to security violations. We focus on both communication and computation in designing the attack models. We build a monitor to check and manage security at runtime and use a reference model, called Tiny Digital Twin, in detecting attacks. The Tiny Digital Twin is an abstract behavioral model that is automatically derived from the state space generated by model checking during design-time. Using CRYSTAL, we are able to systematically model and check complex coordinated attacks. In this paper we discuss the applicability of CRYSTAL in security analysis and attack detection for different case studies, Temperature Control System (TCS), Pneumatic Control System (PCS), and Secure Water Treatment System (SWaT). We provide a detailed description of the framework and explain how it works in different cases.

Place, publisher, year, edition, pages
Elsevier, 2024
Keywords
Cyber-Physical Systems (CPS), Formal verification, Model abstraction, Attack detection system, Runtime monitoring, Tiny Digital Twin
National Category
Computer Systems
Identifiers
urn:nbn:se:mdh:diva-66419 (URN)10.1016/j.jlamp.2024.100965 (DOI)001224282500001 ()2-s2.0-85189706631 (Scopus ID)
Available from: 2024-04-14 Created: 2024-04-14 Last updated: 2024-05-29Bibliographically approved

Open Access in DiVA

fulltext(2809 kB)31 downloads
File information
File name FULLTEXT02.pdfFile size 2809 kBChecksum SHA-512
a4c2183c1bf19ea459a75f89e5139548f9c698ea93ceb14bb38f9f6504381ca862f1a8cffd783f96a7c355f1c9d7ae70e15f854f6b33d3e80fd9314d522f1737
Type fulltextMimetype application/pdf

Authority records

Moradi, Fereidoun

Search in DiVA

By author/editor
Moradi, Fereidoun
By organisation
Embedded Systems
Computer Systems

Search outside of DiVA

GoogleGoogle Scholar
Total: 31 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

isbn
urn-nbn

Altmetric score

isbn
urn-nbn
Total: 1135 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf