How to find a good thesis topic?

The two most important things for finding a good thesis topic is to find a topic that excites you and your supervisor, and that you have the competencies to succeed in.

To help you find a good thesis topic you can read a list of concrete thesis topics that I would be excited to supervise, and a list of past theses from which you can take inspiration. You can pick a topic from my list or propose a topic of your own.

Project ideas

Training safe robot controllers

Controller safety is an important problem where the controller of a robot should not damage itself or the environment in which it operates. To this purpose, some simulators have been developed like Safety Gym from OpenAI, BRAX by Google, or Mujoco by Deepmind.

Differentiable logics allow to have a logical specification of the safety property, and to translate such logic formula into a loss function that can be used in training a neural network. Vehicle is a tool that implements these differentiable logics, and integrates into standard toolkits for training neural networks. The project aim to explore how differentiable logics can help in producing safe controllers.

Formalizing applications of probability theory in the Coq Proof Assistant

Probability theory has many application in computer science: machine learning, statistical algorithms, post-quantum and modern cryptography to name a few. We have been developing two libraries for probability theory with many interesting applications: MathComp-analysis, which is a library for real analysis that includes our work on probability, and Infotheo, which was originally developed to study information theory, but contains now more applications of probabilities.

I have many interesting projects in the intersection of machine learning, statistics and probability theory using these libraries. Get in touch if you want to work on such topics.

Analyze a security protocol

Security protocols are used in all aspects of our lives. TLS for example empowers secure communication over the internet, but is not the only protocol. Many protocols include flaws that go undetected even after years that they have been in use. Many of these flaws are logical errors, that is security problems that designers did not think were possible when designing the protocol. These can be detected using tools (like ProVerif) that allow you to model protocols and automatically check that certain security properties hold, or show an attack otherwise.

A successful thesis in this area would consider an interesting security protocol, and then conduct a formal analysis using these automated tools. Very often these theses lead to finding mistakes in the specifications or implementation. For example we have helped improve the EDHOC standard for secure IoT communication proposed by Ericsson, and showed some flaws in CAN-bus, a network for controlling electronic components in automobiles. Options for the analysis could be: the Apple keychain/Firefox password storage; a messaging protocol (WhatsApp/Telegram etc.); an Internet protocol; an IoT protocol.

Work on analysis/compilation of secure protocols

Often tools for analyzing security protocols come with limitations: certain properties cannot automatically be checked and require manual abstractions to complete the proofs, and there are certain equations that require special care. One particular problem is when analyzing stateful protocols: protocols that maintain state depending upon which certain actions are enabled or not.

Another problem is how to construct secure software once a protocol model has been proven correct: one option is to derive working code from the protocol model that is secure by construction.

If you like to work with programming languages, software analysis, logics, compilers, and think that security problems are very relevant in the software landscape, we can find a thesis for you!

Hacking projects

I do sometimes supervise bachelor and master projects related to hacking, however I reserve these projects for exceptionally motivated students with novel ideas of targets and techniques that they want to explore. If you want to just test your waters on hacking techniques, you can join my class on ethical hacking instead.

Past theses

Here is a list of past thesis titles, I hope this gives you some insight in the kinds of theses that I supervise. Feel free to ask about some topics.

  • Exploring PAC-Learnability of decision stumps in Coq (SWU, 2024)
  • Machine learning robustness using Vehicle (BDS, 2024)
  • Building training material and challenges on fuzzing and symbolic execution (SWU, 2024)
  • Building a linter for finding security vulnerabilities in Dockerfiles (SWU, 2024)
  • Visualizing security protocols as choreographies (SWU, 2023)
  • Human detection of AI generated images (KCS, 2023)
  • EMV payment attacks (KCS, 2023)
  • Building a platform for running CTF competitions (SWU, 2023)
  • Implementing Apachi, a conference management system (SWU, 2022, 2024)
  • Implementing LoRaRatchet, a security protocol for IoT devices (KCS, 2022)
  • Compiling security choreographies to executable code and ProVerif models (KCS, 2022)
  • Hacking CAN bus vehicle health monitors (SWU, 2022)
  • Finding zero day vulnerabilities in the Linux kernel using the CodeQL code scanning tool (SWU, 2022)
  • Creating cybersecurity training material for highschool students (KSD, 2022)
  • LoRaRatchet, a security protocol for IoT devices with post-compromise security (KSD, 2021)
  • Threat assessment for LoRaWAN devices in offshore wind energy (KSD, 2021)
  • Using the angr.io framework to find information flow vulnerabilities in Unix binaries (KCS, 2021)
  • Security analysis of the OSCORE secure transport protocol for IoT (BSc, 2021)
  • Extending session types to model security properties (KCS, 2021)
  • Mitigating timing attacks on network traffic (MSC, 2021)
  • Apachi - an Accountable, Secure and Fair Approach to Conference Paper Submission (KCS, 2020)
  • Scanning the Danish internet to determine the state of Danish cybersecurity (SWU, 2020)
  • Detection of botnets through the use of Honeypots (SWU, 2020)
  • Formal Verification of the Firefox Sync Protocol, Spring 2019
  • Security Analysis of a Smart Heat Meter, Spring 2019
  • CityRun: A combined running- and sightseeing app, Spring 2019
  • Decentralized certificate authority as a blockchain application, Spring 2019
  • Extending Session Types to Model Security Properties, Spring 2019
  • Formal Verification of Object Security for Constrained RESTful Environments (OSCORE), Spring 2019
  • Formal verification of Certificate Transparency, Spring 2019
  • Verification of privacy in Bingo Voting, Spring 2019
  • Zero-knowledge proofs on the GPU for voting, Spring 2019
  • From Applied Pi Calculus to Linear Logic, Fall 2018
  • Formal analysis of EDHOC, a protocol for IoT secure communication, Theis Grønbech Petersen and Thorvald Sahl Jørgensen, Spring 2018
  • Security analysis for smart door lock, Steffen Mogensen, Spring 2018
  • Deduplicated Storage Systems: Trade-offs between security and efficiency, Emma Arfelt Kock, Fall 2017
  • Verifying Selene in Tamarin, Eva Drewsen, Spring 2017
  • Voting Protocol in Ethereum, Adrian Brink, Spring 2017
  • Transparent authentication with wearable devices, Jacob Cholewa and Rasmus Wismann, Spring 2017
  • Hacking WinVote machines, Florin Vasile and Andreas Nielsen, Fall 2016