The PhD defence will be fully digital and streamed directly using Zoom. The host of the session will moderate the technicalities while the chair of the defence will moderate the disputation.
Ex auditorio questions: the chair of the defence will invite the audience to ask ex auditorio questions either written or oral. This can be requested by clicking 'Participants -> Raise hand'.
Trial lecture
Executable UML models: formal modelling and verification of functional correctness and safety properties
Main research findings
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.
For more information
Ida Elisabeth Rydning, i.e.rydning@its.uio.no
Technician, Arild Hemstad, arild.hemstad@its.uio.no