Themen für Abschlussarbeiten
Inhaltsverzeichnis
Alle vorgeschlagenen Themen können grundsätzlich als Bachelor-, Beleg-, Diplom-, oder Masterarbeitsthema vergeben werden. Wir werden den Umfang dann in Absprache anpassen. Auch eigene Themenvorschläge sind willkommen!
High-performance Architectures
Systems in high-performance computing (HPC) need to cater to the demanding nature of applications in this field. Traditional requirements include low latency networking, cache-optimal memory placement, and timely coordination between compute nodes in the system. More recently, energy considerations have also become a concern. We study the implications these requirements and the specialised HPC hardware have for system-level software.
In recent years, several new main memory technologies have emerged, such as non-volatile memory or high-bandwidth memory.
Unfortunately, these new technologies are often space-constrained or even unavailable in some computer systems.
We therefore plan to develop mechanisms to compensate for the lack of high-bandwidth memory, ECC memory or non-volatile memory. These mechanisms should enhance the corresponding non-functional properties (high data throughput, error correction, persistence) when used on conventional DDR DRAM. A user land interface should allow applications to benefit from these strategies with minimal code changes.
Supervisor: André Berthold
Scheduling
The scheduling of processes or threads in different environments (e.g. realtime, distributed, or high-performance systems) is governed by a diverse set of optimisation goals: throughput, timeliness, energy conservation, quality-of-service guarantees, to name but a few. Our work in this area tries to incorporate new approaches like machine learning or explores new areas like disaggregated systems.
System Architecture
Modern computers have a complex interaction between processing units, devices, and pieces of firmware. This complexity is hard to understand and manage. Therefore, Fiedler et al. have developed the Sockeye3 language. Sockeye3 specifications allow to capture the possible interactions of the different contexts on a modern computer at the level of accessible memory.
The M³ system has a lot of such interacting hardware components. This microkernel-based system for heterogeneous manycores is a tiled architecture with each CPU core isolated using a special hardware component.
The idea of this student project should be to describe the architecture of M³ using the Sockeye3 language. This should help to understand the hardware-based isolation in the M³ system better. To this end, it should be attempted to use Sockeye3 to verify some isolation properties of the different contexts in M³.
Contact: Viktor Reusch
Trusted Computing
The Transport Layer Security (TLS) protocol solves the problem of securing communication channels between two computer systems. Remote attestation is a technology from the field of Trusted Computing that allows to identify what software is running on a remote computer system. Additionally, remote attestation provides secure identification of the remote system. By combining the two protocols, one can ensure that the communication channel really terminates in a specifc remote system and that the right software is running there.
In earlier work, remote attestation has already been integrated into the TLS protocol. The corresponding implementation is based on OpenSSL, which is quite complex and written in C. However, smaller TLS libraries exist, including ones written in safe programming languages. In this work, possible candidates shall be investigated and the concept of remote attestation shall then be intregated into such a suitable TLS library.
Supervisor: Carsten Weinhold
Remote attestation is a technology from the field of Trusted Computing that allows to identify what software is running on a remote computer system. Additionally, remote attestation provides secure identification of the remote system. Some low-power Internet-of-Things (IoT) devices based on RIOT can support attestation, but potentially not using the same protocols as more capable systems, including M3. The goal of this work is to enable cross-platform attestation between M3 and RIOT systems. A possible way to do this is by integrating attestation with the communication protocol DTLS, which is less resource hungry than TCP/IP-based TLS and therefore more suitable for RIOT-based devices.
Supervisor: Carsten Weinhold
Hardware support for efficient encryption of DRAM contents is readily available on many platforms. There are also solutions that allow for integrity checking, but they typically do not guarantee that data in memory is up to date, because the costs for such freshness checks are too high. This may allow attackers to roll back all or a part of the memory contents to an older version that can still be decrypted and also pass signature-based integrity checks, but that is not the latest version. Such a roll-back attack may cause correctness or security issues in the program that uses the data in this memory region.
In this thesis and/or a research project module preceding the thesis, software-based methods for ensuring freshness of encrypted memory shall be reviewed. At least one approach shall be implemented. Suitability of the approach for various use cases, impact of hardware support, whether all memory or just parts of it are up-to-date, and the performance impact shall be evaluated.
Supervisor: Carsten Weinhold
Virtualization
Fault Tolerance and Fault Injection
Computers are usually assumed to always work correctly and predictably, as defined in the program code. While this is generally correct, there may be internal and external influences that effect this assumption. Internal influences can be undetected production errors, which become more likely as the structure size of the chips becomes increasingly smaller. While external influences can be radiation particles, which pass through the chips and lead for example to ionization in the transistors. Especially if these errors occur only very rarely and the system architecture is based on the assumption that exactly what is defined in the code will happen, severe consequences can be the result.
To counter this, we study the possibilities of software-implemented hardware fault tolerance (SIHFT), in which faults are detected with the help of software. This variant can also be integrated after the hardware is developed and produced and is therefore also applicable for commercial off-the-shelf hardware. Since redundant hardware is expensive to develop, SIHFT has many possible areas to be applied, for example in cubesats or cars.
In particular, we evaluate SIHFT methods with the fault-injection framework FAIL*, which can imitate hardware faults caused by radiation effects and systematically examine a program regarding its fault tolerance.
Miscellaneous
This category comprises topics that don't fit any of the other categories.
The Rust Miri tool is an interpreter for Rust's Mid-level Intermediate Representation (MIR), used primarily for detecting undefined behavior.
It helps identify issues such as use-after-free, buffer overflows, and invalid memory accesses, ensuring memory safety and correctness in Rust programs.
M³ is a microkernel-based operating system, which is primarily written in Rust.
Due to the use of platform-specific code and performance considerations, M³ contains portions of unsafe code.
Consequently, testing (a subset of) M³ using Miri would further assure the safety and security of the M³ system.
Get in touch to discuss a possible thesis topic.
Supervisor: Viktor Reusch
M³ is a microkernel-based operating system designed for heterogeneous manycore systems.
The M³ kernel is written in Rust, a systems programming language known for its safety features and performance. Verus is a verification tool for Rust code that allows developers to specify the expected behavior of their code and statically checks that the code will always satisfy those specifications. By using Verus, we hope to gain more confidence in the correctness of the M³ kernel and its ability to handle complex scenarios.
The task of this thesis topic is to try out Verus for verifying parts of the M³ kernel. The focus is on areas of the kernel that are critical to its correctness and would benefit from formal verification. The primary goal of this project is to test out Verus as a tool for verifying the M³ kernel and to increase confidence in the correctness of the kernel, particularly in its unsafe portions.
Supervisor: Viktor Reusch