Elahe Fazeldehkordi successfully completed her PhD trial lecture and thesis defense at the Department of Technology Systems, University of Oslo on Tuesday, the 16th of March 2021 and will be awarded the degree of Doctor of Philosophy.
The title of her thesis is “Security and Privacy Solutions in IoT and Distributed Systems Design” and the given topic for her trial lecture was “Executable UML models: formal modelling and verification of functional correctness and safety properties”.
New distributed systems in computing technology are appearing on the market day by day. Consequently, new security and privacy challenges arise when designing these systems. These challenges demand a need to look for comprehensive and more precise approaches that can provide higher levels of security, privacy, and trust from the design phase in these systems.
In order to develop systems including open distributed systems, we need techniques and tools for specification, design, and code generation. For the initial ideas of such systems, it is desirable to use graphical notations, so that ideas can easily be understood. This is relevant for the early design phase. Once the ideas are agreed upon, it is then desirable to have a formal basis for the specifications of the desired system, in order to support rigorous reasoning about specifications and designs. This can be done in the late design phase.
Existing documents for security and privacy requirements and functionalities in IoT systems lack some of the security functionalities, and in particular, they do not focus on privacy issues or are presented only in textual form, without defining a framework. Structures of these documents are also complicated. Systems are often made without the help of security and privacy experts. So a comprehensive graphical representation framework is needed and should be easy to follow, even for non-experts.
Formal methods have come into wide use in the design and verification of safety, security, and privacy of systems in the industry, because they are very effective in verifying safety, security, and privacy requirements of systems, requirements for which testing is mostly ineffective. Formal verification techniques can guarantee that a design is free of specific flaws.
Provability of IoT and distributed systems depends on the language used to model the system, its semantics, and the kind of system properties to prove and the techniques used to verify them. One may take a bottom-up approach, starting with low level languages in use, or one may take a top-down approach, starting with a more abstract language with an expressiveness suitable for IoT and distributed systems. Such a language can be used to model IoT and distributed systems, and if the language is executable, it can be used for simulation and prototyping of IoT and distributed systems, and if the language is imperative with standard mechanisms such as object orientation, IoT and distributed models made in the language can easily be translated to more low level languages. The latter approach also has the advantage that one can define the language and its semantics so that it is amenable to semantical analysis and verification. Additionally, this approach makes program reasoning simple and powerful.
The active object paradigm provides a natural way of modeling distributed systems in general, and IoT systems in particular, because it covers the fundamental aspects of IoT systems such as distribution of concurrent, autonomous units communicating by message passing, where each unit can run on a device with limited processing power and limited storage.
In this thesis, we focus on two aspects of the design phase to develop methodologies to improve security, privacy, and trust levels of IoT and distributed systems. Firstly, we consider the early design phase, where the architecture of a system is being developed, focusing on the setting of IoT systems. Secondly, we consider the late design phase, where models, in particular executable models and prototypes are designed, focusing on IoT systems and also the more general setting of distributed systems. For the modeling related to the late design phase, we limit our work to the active object paradigm. In particular, we find techniques for increasing the security level of the overall IoT systems using a security and privacy functionality framework, and a technique for detecting potential vulnerabilities that can cause distributed denial of service (DDoS) attacks using static analysis technique. In addition, we developed a language-based approach to provide trust, safety, security, and privacy for smart contracts.
The following committee has been appointed to evaluate her thesis, trial lecture and defense:
- First external opponent: Jüri Vain, Tallinn University of Technology, Department of Software Science, Estonia.
- Second external opponent: Svetlana Boudko, Norwegian Computing Center, Norway.
- Internal member: Professor Paal Engelstad, Department of Technology Systems, UiO.
- Chair of defence: Head of Department Stian Løvold, Department of Technology Systems, UiO
Elahe Fazeldehkordi carried out her PhD work at the Department of Technology Systems, University of Oslo.
Her main supervisor was Professor Olaf Owe, Department of Informatics, University of Oslo and co-supervisors Professor Josef Noll, Department of Technology Systems, University of Oslo, Postdoctoral Fellow Toktam Ramezanifarkhani, Department of Informatics, University of Oslo and Associate Professor Christian Johansen NTNU, Norway.
Congratulations!
