PhD research projects

If you are interested in one of these topics, please read the application guidance first and then contact the named supervisor to discuss.

1. Human factors of software updating. Updating software is one of the best ways to protect a computer from attack, yet many people choose to not update software. Identify the best practices for automatic updating of software so that users are happy and security patches are installed quickly. Contact: Kami Vaniea

2. Usable security API design for SSL/TLS. Understand the current usability issues with security APIs such as SSL and TLS. Then design a new API that is easier to use resulting in higher adoption of security practices and a reduction of errors. Contact: Kami Vaniea

3. Automatic analysis of electronic voting protocols. Many countries have or plan to conduct legally binding elections using electronic voting systems. Such systems need to provide security guarantees, e.g., fairness, privacy, and verifiability. These are tricky to establish and can be in conflict with one another. Several proposed electronic voting systems have been found to fail to achieve their intended security goals, demonstrating the need for formally verified electronic voting systems. Contact: Myrto Arapinis

4. Verification of Software Defined Network controller programs. Software Defined Networking is becoming an important part of data centre infrastructure; SDN controllers run programs to configure switches to achieve certain aims. The challenge is to ensure such controller programs ensure overall security objectives as they reconfigure networks dynamically and in response to security attacks. Contact: David Aspinall

5. Verification of Security of the mbed OS uVisor (with ARM). The mbed OS uVisor is a core security component for ARM's mbed IoT platform. It creates isolated security domains M7 microcontrollers with a Memory Protection Unit (MPU). On top of these the uVisor provides a flexible compartmentalisation using separate security domains ("Secure Boxes"), configured with ACLs. This project will apply theorem proving methods to help define and then verify correctness and security properties of the uVisor implementation, building on previous work on instruction set models and decompilation techniques. Contact: [Ian Stark][stark]

6. Formal Specifications and Proofs for TrustZone (with ARM). Increasing complexity and connectivity in microcontroller devices motivates new protection mechanisms to improve reliability and security. ARM's TrustZone for ARMv8-M provides a separate "secure world" execution mode to enable features such as secure firmware updates, safe integration of code from multiple suppliers and controlled access to privileged peripherals. This project will study the low-level instruction set design of TrustZone for ARMv8-M, devising formal specifications describing the security properties that hold at the instruction level and proofs that these provide the intended protection against low-level attacks. Contact: [Ian Stark][stark].

7. Quantum-enhanced Cloud. The security of the cloud could be obtained through Fully Homomorphic Encryption schemes. However these schemes are potentially breakable in a post-quantum regime and require huge overhead and hence despite intensive efforts from all the major players in the information industry, they remain mainly infeasible. The primary goal of this project is to develop quantum enhanced protocols where both efficiency and security are boosted. Implementations of plug and play solutions for these new protocols will be also pursued in realistic scenarios. Contact: Elham Kashefi

8. Nominal Logic for Verification and Security. Nominal logic extends ordinary logic with special features for reasoning about names, particularly freshly introduced names with a particular scope (similar to nonces in cryptographic protocols). Thus nominal logics and type theory may form a good foundation for verification of security properties. This topic is in the area of nominal logic for verification and security. Contact: James Cheney

9. Language-based provenance security. Provenance means metadata/trace information about a computation. Many scientific disciplines are increasingly data-driven and require support for provenance to make it possible to safely share and reuse raw data or processed results. There are many intriguing interactions between provenance and classical problems in programming languages and security. This includes language-based security (information flow), incremental or bidirectional computation, and software engineering (program slicing) for provenance-tracking. This topic is in the area of language-based provenance security. Contact: James Cheney

10. Mobile Crowdsensing with Location Privacy. Using sensor data from mobile phones for better understanding of users and fine-grained monitoring of the environment is a major current research topic. From point of view of privacy, the challenge is to infer important features from collective data, without compromising location and other sensitive information of any individual. Contact: Rik Sarkar

11. Security Applications of Planning and Decision Making in Robotics. Robots are sometimes used in security applications, for example areas such as border patrol scheduling. Robots are often used within teams of other robots and humans: this leads to issues of uncertainty and incomplete information. How can we design intelligence for these applications that cannot be easily predicted or fooled by opponents? Contact: Michael Rovatsos

12. Security of Blockchain protocols. Study the underpinnings of blockchain based distributed protocols, including the mechanisms behind Bitcoin, Ethereum and other cryptocurrency systems. Contact: Aggelos Kiayias

13. Privacy in communication systems. Study the concept of privacy in communications and data sharing and design and analyze systems that facilitate it using suitable cryptographic and statistical methods. Contact: Aggelos Kiayias

14. Applied and Theoretical Cryptography. Study cryptography from both applied and theoretical angles and apply it to solve problems such as secure channels, identification systems, cloud storage, secure digital content distribution and others. Contact: Aggelos Kiayias

15. Automatic Vulnerability Predicition and Discovery. Software vulnerabilities continue to plague the industry. Tools help find problems, but current technology is limited and deploying patches is largely manual. Future systems will be proactive, searching for possible problems and deploying work-arounds or repairs automatically. Ideas from program synthesis, critics and abstraction-refinement may help here. Contact: David Aspinall

16. Security flaws in concurrent programs. Concurrent programs can contain subtle flaws that lead to deadlock or race conditions, but such failures can be vanishingly rare. Is it possible to provide additional conditions that guarantee that failures cannot be triggered by an attacker, or if failures occur, they can't be exploited by an attacker? Contact: David Aspinall

17. User Interfaces for Sensitive Health Data. How can we help users control who can see sensitive information about their health and well-being? This is particularly relevant for people who live with a long-term condition that requires support from formal carers, such as health professionals, and informal carers, such as family and friends, and for people with a stigmatised condition, such as HIV+, schizophrenia, or urinary incontinence. Contact: Maria Wolters

18. Keeping Digital Heritage Private. Just as previous generations amassed letters, books, and physical artefacts throughout their lives, our generation amasses digital artefacts. How can we help users find and designate digital artefacts they would like to preserve for themselves, and artefacts that can be passed on to future generations, in a way that properly respects desires for privacy, for them and their descendants? Contact: Maria Wolters