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.
| Identifer | oai:union.ndltd.org:UPSALLA1/oai:DiVA.org:mdh-45320 |
| Date | January 2019 |
| Creators | Matović, Aleksandar |
| Publisher | Mälardalens högskola, Akademin för innovation, design och teknik |
| Source Sets | DiVA Archive at Upsalla University |
| Language | English |
| Detected Language | English |
| Type | Student thesis, info:eu-repo/semantics/bachelorThesis, text |
| Format | application/pdf |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.0016 seconds