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, some generic project topics that I would be interested 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.
- Robust machine learning: verify the robustness of a machine learning algorithm in Coq (e.g.: the PAC algorithm)
Programming languages & verification
- Verify probabilistic Hoare logic using monadic reasoning in Coq
- Verification of security choreographies (see Security Protocols as Choreographies)
- Prepare and evaluate education material (e-learning, also serious games) for security training in highschools
- Prepare and evaluate training material on adversarial machine learning
- Create “security-by-design” training material
- Attack EMV payment systems (familiarize yourself with EMV relay attacks first)
Broadly speaking, I am interested in a wide range of topics, most of them relate to formal verification, security, and education. You can come up with your own idea, so here is a few overarching themes that I would be interested to supervise.
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!
Hack a connected device
Another option is to consider a particular hardware device whose security is important, and try to hack it. This thesis requires you to go through the process of doing forensics analysis of a real device and then responsible disclosure in case you find some bugs. It requires a diverse range of skills, including quick learning of new software and hardware analysis tools, analyzing and reconstructing encrypted communication between devices, good communication skills with the companies involved.
Examples of such a thesis are: hack a smart-lock, IoT camera or toy, a smart-meter, an industrial control system etc.
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.
- Implementing Apachi, a conference management system (SWU, 2022)
- 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