Title: Modeling and analysis of security implications in safety-critical systems using the Rebeca tool
Subject: Software engineering
Level: Advanced
Description: For safety-critical applications safety is the highest overall goal, however nowadays systems are becoming less isolated and more interconnected, thus, the importance of deal-ing with security concerns in order to be able to assure system safety raises. There are developed security analyses on a system level, e.g., vulnerability and threat analyses, and even safety and security co-analyses, e.g., FMVEA [1], SAHARA [2]. However, the advance in the research area has to be coupled with technologies being applied in real life. The understanding of system safety being connected to system security is already presented in the research community, however there is a lack of particular examples coupled with system analyses, i.e., not just a successful attack being performed, but bounding a particular threat to a particular safety requirement. Thus, the thesis aims to investigate how injected failures caused by security breaches and corresponding adversary actions can affect safety requirements. The idea is to verify system safety requirements by using a verification tool, in which an industrial system along with injected failures can be modeled.
In this thesis we propose to model a robot arm presented by a set of safety functions with the Rebeca tool [3]. Rebeca is an actor-based language and a corresponding tool, in which one can model system behavior via its states and check whether specified system properties are holding. The security analysis outcomes will be incorporated by modeling of security breaches and possible adversary actions. The system description and its safety requirements will be provided. The work will include a survey on existing formal modeling language and their applicability for modeling and analysis of security concerns, a system security analysis of the provided system, possible extension of Rebeca to support security modeling, modeling in Rebeca of the provided system and security breaches, and analysis of modelling results.

[1] Schmittner C., Ma Z., Smith P. (2014) FMVEA for Safety and Security Analysis of Intelligent and Coop-erative Vehicles. In: Bondavalli A., Ceccarelli A., Ortmeier F. (eds) Computer Safety, Reliability, and Security. SAFECOMP 2014. Lecture Notes in Computer Science, vol 8696. Springer, Cham
[2] Georg Macher, Harald Sporer, Reinhard Berlach, Eric Armengaud, and Christian Kreiner. 2015. SAHA-RA: a security-aware hazard and risk analysis method. In Proceedings of the 2015 Design, Automation & Test in Europe Conference & Exhibition (DATE '15). EDA Consortium, San Jose, CA, USA, 621-624.
[3] http://rebeca-lang.org/
Start date:
End date:
IDT supervisors: Elena Lisova, Aida Causevic
Examiner: Marjan Sirjani
Company contact: