Student Thesis Topics (2025)

Teaching

I will supervise BSc thesis projects in Spring 2025. Since I have limited supervision capacity, I typically take the first N students following more or less a first-come, first-served strategy. I like to form clusters of students working on related topics, and I organize weekly (online) meetings with these clusters. We use a collaborative note taking tool to track progress. The work itself is taking place in two phases. In the first phase, students will dive into the state of the art of their topic, resulting in a state of the art report. I will review these reports and provide feedback. In the second phase, students focus on their own contribution, and they will finally write their thesis. The thesis naturally builds on the state of the art report and extends it with the work describing the contribution. Before submitting the thesis, students have to present and defend their work in the BSc thesis seminar. The seminar grade is given for the presentation. The thesis grade is given for the thesis report, the technical accomplishments, including the work organization (regular participation in weekly meetings and steady progress).

If you are interested in systems-oriented computer science and computer security, either talk to me in person or schedule an online meeting. I expect that students have a solid understanding of operating systems and computer networks or computer security. I also expect that students are capable to handle programming tasks well and that they can work independently.

Performance and Usability of Rusty and not so Rusty Unikernels

Unikernels are operating system functions implemented as a library and linked to application code so that the resulting software image can be executed directly by a hypervisor.

Performance and Usability Assessment of the Nanos Unikernel

Nanos is a unikernel written in C. The goal of this project is to investigate the performance of applications running on the Nanos unikernel. The project involves selecting applications of varying code complexities and functionalities (e.g., web servers, machine learning inference models, or network utilities), adapt them to run on the Nanos unikernel, and evaluate their performance and the usability of Nanos compared to traditional operating system environments. Students need to understand the structure of the Nanos unikernel and develop the skills necessary to port applications to Nanos. The performance metrics should include startup time, memory footprint, and execution speed for each application. For usability analysis, emphasis should be on handling system calls, I/O, and network communication and the porting effort. Moreover, students should document any challenges encountered during this analysis along with resolution strategies.

Reading:

Performance and Usability Assessment of the Rusty Hermit Unikernel

Rusty Hermit is a unikernel written in Rust. The goal of this project is to investigate the performance of applications running on the Rusty Hermit unikernel. The project involves selecting applications of varying code complexities and functionalities (e.g., web servers, machine learning inference models, or network utilities), adapt them to run on the Rusty Hermit unikernel, and evaluate their performance and the usability of Rusty Hermit compared to traditional operating system environments. Students need to understand the structure of the Rusty Hermit unikernel and develop the skills necessary to port applications to Rusty Hermit. The performance metrics should include startup time, memory footprint, and execution speed for each application. For usability analysis, emphasis should be on handling system calls, I/O, and network communication and the porting effort. Moreover, students should document any challenges encountered during this analysis along with resolution strategies.

Reading:

Performance and Usability Assessment of the Unikraft Unikernel

Unikraft is a unikernel written in C. The goal of this project is to investigate the performance of applications running on the Unikraft unikernel. The project involves selecting applications of varying code complexities and functionalities (e.g., web servers, machine learning inference models, or network utilities), adapt them to run on the Unikraft unikernel, and evaluate their performance and the usability of Unikraft compared to traditional operating system environments. Students need to understand the structure of the Unikraft unikernel and develop the skills necessary to port applications to Unikraft. The performance metrics should include startup time, memory footprint, and execution speed for each application. For usability analysis, emphasis should be on handling system calls, I/O, and network communication and the porting effort. Moreover, students should document any challenges encountered during this analysis along with resolution strategies.

Reading:

Unikernel Network Stacks

Unikernels usually have to provide a TCP/IP network stack and they often adopt and integrate existing network stacks. The goal is to investigate how these network stacks compare and perform relative to the network stack found in say the Linux kernel.

Performance Evaluation of the smoltcp TCP/IP Stack written in Rust

The smoltcp project develops a TCP/IP stack written in Rust. The smoltcp project provides a standalone, event-driven TCP/IP stack designed for bare-metal applications and real-time embedded systems. Its design goals are simplicity and robustness.

The goal of this project is to compare the smoltcp user-space TCP/IP stack with a traditional kernel-based TCP/IP stack (e.g., the Linux TCP stack) based on performance metrics such as latency, throughput, CPU utilization, and memory usage. Students need to develop various use-case scenarios (e.g., bulk data transfer, message exchange, etc) to perform the assessment under different conditions (e.g., different packet sizes, network speeds, and packet loss/jitter). For evaluation, consider smoltcp in both real-time OS, and Linux environment context to measure its performance.

Reading:

Performance Evaluation of the lwIP TCP/IP Stack written in C

The lwIP TCP/IP stack was originally designed for embedded systems, but it has recently also been used by unikernels such as Unikraft. The goal of the project is to compare lwIP running in user space with a traditional TCP/IP stack provided by a typical Linux kernel to understand the trade-offs and performance gains. Students need to evaluate the performance of lwIP under different scenarios, such as high loads, network disruption, and error-prone environments. lwIP has different variants optimized for various tasks, such as memory usage, enhanced protocol support, and more. The assessment of these variants can also provide valuable insights into performance metrics. For evaluation, consider lwIP in both real-time OS and Linux environment contexts to measure its performance.

Reading:

Unikernel Security

Rust-based Unikernel Security Analysis

Using Rust does not automatically ensure that code is free from security issues. The goal is to analyze and improve the security properties of Rust-based unikernels. Students need to understand the security mechanisms of Rust-based unikernels and identify common vulnerabilities. Then, analyze the impact of Rust's safety features (e.g., memory safety, type safety, and concurrency model) on these vulnerabilities. Based on the findings, design and implement appropriate mitigation strategies (e.g., access controls, sandboxing, or monitoring). Finally, verify and validate the effectiveness of the proposed approach against the identified vulnerabilities. Also, evaluate the trade-offs between security and performance in Rust-based unikernels, present the impact of the proposed approach in comparison with the standard implementations.

Reading:

Investigating Unikernels and In-Memory Data Encryption

Modern CPUs support keeping data encrypted in main memory, which protects data against potential attacks and is commonly referred to as confidential computing. The goal of this project is to investigate how unikernels handle in-memory data encryption and to analyze the associated performance and software complexity in the context of confidential computing. Students need to analyze the performance costs of secure memory systems in general to understand how modern CPUs enable in-memory encryption to secure sensitive data from attacks. Then, investigate the existing unikernel frameworks (such as MirageOS, IncludeOS, or OSv) to determine if they currently support confidential computing techniques or have the potential to integrate them.

Reading:

Unikernel Code Analysis and Verification

Formal Verification of Unikernel Components

Consider a cloud service provider running multiple unikernels on a single physical server. Each unikernel is responsible for its own memory management and scheduling. When a unikernel boots, the hypervisor allocates a specific amount of memory to the unikernels. It is then the unikernel’s responsibility to allocate this memory as needed (e.g., data storage, buffers) and free the memory when it is no longer needed to avoid memory leakage.

Similarly, for scheduling, the hypervisor manages the CPU resources among the individual unikernels based on the criticality of their applications. However, within each unikernel, there may be different tasks or functions, such as processing network packets, handling input/output operations, or managing background tasks. The unikernel's scheduler ensures that these tasks are executed in the required order while prioritzing critical tasks.

The objective of this project is to formally verify the memory allocator and scheduler of each unikernel, not the hypervisor. The students need to select atleast two different variants of unikernels and formally verify the memory allocation and scheduling of each unikernel using formal verification tools. Then, compare the results to determine if different unikernel variants impact memory allocation and scheduling.

For the formal verification of unikernel memory allocation: 1) Verify that all allocated memory is freed to prevent memory leakage. 2) Verify that memory accesses are within bounds to avoid buffer overflows. 3) Verify that no memory is accessed after being freed to prevent use after free bugs.

Similiarly for the formal verification of scheduling: 1) Verify that scheduler meet all the constraints (e.g. complete task in allocated CPU time). 2) Verify the fair CPU access for all tasks based on task priorities. 3) Verify the absence of deadlocks and task starvation to ensure reliable task execution.

Reading:

Static Analysis of Unikernel Codebases to Assess Code Quality and Complexity

Perform static analysis (code quality and complexity) on at least two unikernels using tools that can assess code quality, complexity, and security. Students need to identify and categorize the common code issues and vulnerabilities within each unikernel. Analyze the effectiveness of static analysis tools and their utilization for evaluating unikernel memory safety, concurrency, and modularity. Summarize findings by highlighting the strengths and weaknesses of static analysis tools in unikernel environments, as well as their limitations for code verification. Compare the assessment results of both unikernels in terms of common vulnerabilities, challenges unique to each unikernel, and suggest your idea for improvements based on your findings.

Note: Static analysis tools are designed for traditional monolithic or microservice-based architectures, may not fully align with requirements of unikernel.

Suggestions (Not mandatory): Use Docker to containerize the unikernel environment for repeated tests. Also, automate and document the static analysis process using GitHub Actions to support accurate and reproducible comparisons.

Static Analysis Tools (Not limited to these): Clang Static Analyzer, Cppcheck, SonarQube

Reading:

Adoption of Microkernels Formal Verification Technique to Unikernels

A microkernel is a minimal OS kernel providing essential services such as process management, memory management, and communication between processes. A variety of formal verification methods have been proposed to prove the correctness and security of its design, including theorem proving, model checking, and proof assistants. The project involves the analysis of existing formal verification approaches designed for microkernels and investigate whether these approaches can be tailored or adopted for unikernels. The student needs to understand a specific microkernel (e.g., seL4) and its formal verification approaches, then apply similar verification to a unikernel (e.g., unikraft) or provide a theoretical analysis, supported by relevant justification, to argue the feasibility or infeasibility of such an approach. If feasible, then describe your idea to tailor or adopt the existing formal verification technique to a specific unikernel.

Note: Unikraft is a modular unikernel, which means that the unikernel is built from different components and libraries required for a targeted application or service. Therefore, it may be possible to apply verification techniques to smaller, isolated modules rather than the entire kernel.

Reading:

Context Sensitive Authentication

Dynamic Context Sensitive Authentication System

Context-sensitive authentication relies on multiple biometric features rather than a single one, including the surrounding conditions. Suppose a user authenticates with a system using voice recognition in a quiet environment, and the surroundings become noisy, the system would dynamically switch to face recognition to ensure seamless validation.

To implement this approach, the student needs to identify suitable devices and biometrics. For smartphones, feasible options include facial recognition, voice authentication, and swipe dynamics. Then, identify relevant sensors for contextual environmental analysis, such as the microphone (to assess noise levels) and motion sensors (for proximity detection). Finally, implement a multimodal data fusion framework that dynamically assigns weights to each biometric modality based on contextual reliability. The approach will authenticate the user based on fused biometric data, ensuring adaptive and continuous security.

Reading:

Educational Technology

Teaching Functional Programming and Proof Assistants to Beginners Using Lean

The Lean programming language and theorem prover provide a high-level programming environment for formalizing mathematics and verifying formalized proofs. Lean4 belongs to the class of functional programming languages, while the theorem prover is based on dependent type theory.

Usually first-year students are required to learn programming and how to write formal proofs. However, programming education is largely focused on imperative languages, while mathematics education often relies on handwritten proofs checked by humans.

To address this, we need to develop modular learning tutorials that supports students in learning the basics of functional programming and formal proof writing in Lean. Each module could focus on key topics such as recursion, higher-order functions, immutability, and proof by induction. Features should be implemented to detect common errors students make in Lean proofs and programming exercises, then provide real-time feedback and hints. The work may involve conducting assessment of learning materials using some first-year students (if possible) to evaluate their effectiveness.

Reading: