This page lists the research topics that are currently available in the Secure Systems group or with our industry partners. Each topic can be structured either as a special assignment or as an MSc thesis depending on the interests, background and experience of the students. If you are interested in a particular topic, send e-mail to the contact person (as well as the responsible ssupervisorsupervisor: (N. Asokan), Tuomas Aura, Lachlan Gunn or Janne Lindqvist) listed explaining your background and interests.
- Formally-verified executable simulation. So far we have used F* to prove the security of our model, but cannot test the accuracy of the model since it is not directly executable. The goal of this project would be to take our generic description of the ISA does in F* code, and add the extra functionality needed to make it executable.
- Unsafe registers/memory. The model verifies that, by applying taint tracking throughout the system, sensitive data cannot leak outside the system. However, we cannot use taint-tracking everywhere. Currently we only model this for the program counter, which is treated as a special case, and everything else is can potentially blindable. But hold sensitive data. But a real system has other non-blindable private state, such as memory mapped to peripherals, and the effects of variable-length instructions. The goal of this project would be to extend the model to incorporate non-blindable this kind of state, and show that an appropriately-chosen taint-tracking rule still preserves the privacy of client data.
- Microarchitectural side channels. We currently consider only an unpipelined in-order CPU model, where instructions complete one after another in the order in which they appear in memory. Real processors are more complex than this. To get high performance, instructions must take more than one cycle, with one instruction beginning to execute before previous instructions have finished. In many processors, instructions are not executed in order, with a later instruction able to be executed before an earlier one if the data it needs is already available. The goal of this project would be to model this kind of processor in order to verify the security of a speculative processor.
BliMe so far has been implemented only for CPUs. But many real-world applications, such as machine learning, also use a GPU for computation. In this project you will investigate how to extend BliMe to GPUs by taking advantage of the fact that GPU code tends to be simpler and more predictable than code written for CPUs, in order to achieve maximum performance. You will use static analysis to verify that such a piece of code does not leak sensitive data, and therefore allow BliMe to be extended to GPUs supporting confidential computing, like Nvidia's new H100 GPU.