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
CASE STUDIES ON MODELING SECURITY IMPLICATIONS ON SAFETY
Mälardalen University, School of Innovation, Design and Engineering.
2019 (English)Independent thesis Advanced level (degree of Master (One Year)), 15 credits / 22,5 HE creditsStudent thesis
Abstract [en]

Security is widely recognized as an important property that is tightly interdependentwith safety in safety-critical systems. The goal of this thesis is to conduct case studies on the implications that security attacks may have on the safety of these systems.In these case studies, we formally model the design of a robot arm system, verify itssecurity against some potential attack scenarios, propose mitigation techniques andanalyze their effectiveness. In order to achieve a thorough knowledge about the current formal verification approaches and select a proper modeling language/tool, weconducted an extensive literature review. We performed this review following a wellknown approach proposed by Barbara Kitchenham. The procedure and outcomes ofthis review are detailed in this thesis. Based on the literature review, we chose TRebeca, (a timed extension of Rebeca), as the formal language to model the robot armsystem, attack scenarios and mitigation techniques. Rebeca is an actor-based modeling language with a Java-like syntax that is effectively used to model concurrent anddistributed systems. This language is supported by a full-featured IDE called Afra,which facilitates the development of (T)Rebeca models and verification of correctnessproperties (such as safety and security) on them. Among several functions providedby a robot arm system, we chose two important functions i.e., Stand Still Supervisionand Control Error Supervision, which we believe would be interesting for attackerstrying to get control over robot movements. In particular, attackers may maliciouslymanipulate the parameter values of these functions, which may lead to safety issues.In order to find suitable attack scenarios on these functions, we studied the mostimportant security protocols used in safety-critical industrial control systems. Weobserved that these systems are vulnerable to several attacks, and man-in-the-middleattack is among the most successful attacks on these systems. Based on this study,we devised two attack scenarios for each function and modeled them with TRebeca.To mitigate these attacks, we proposed a redundancy technique, whose effectivenesswas also assured by Afra.

Place, publisher, year, edition, pages
2019. , p. 49
Keywords [en]
model-checking, security, safety-critical, rebeca, modeling security implications
National Category
Electrical Engineering, Electronic Engineering, Information Engineering
Identifiers
URN: urn:nbn:se:mdh:diva-45320OAI: oai:DiVA.org:mdh-45320DiVA, id: diva2:1355252
Subject / course
Computer Science
Presentation
2019-09-19, R2-141, Västerås, 11:26 (English)
Supervisors
Examiners
Available from: 2019-10-23 Created: 2019-09-27 Last updated: 2019-10-23Bibliographically approved

Open Access in DiVA

fulltext(1117 kB)66 downloads
File information
File name FULLTEXT01.pdfFile size 1117 kBChecksum SHA-512
6d4e43fbec7bbf1c1f02b4b25705d2507259be63dbfe785bb40a46773e88d0e4cdda3b140932a970199393ef26b99785f6749c57ace60cae3f92fa1e86093ce9
Type fulltextMimetype application/pdf

Search in DiVA

By author/editor
Matović, Aleksandar
By organisation
School of Innovation, Design and Engineering
Electrical Engineering, Electronic Engineering, Information Engineering

Search outside of DiVA

GoogleGoogle Scholar
Total: 66 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

urn-nbn

Altmetric score

urn-nbn
Total: 776 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