Verifiable Cryptography and Trusted Hardware

The student will be based in the Department of Computer Science at the University of Surrey, UK.

Supervisory team: Dr François Dupressoir, (http://www.surrey.ac.uk/cs/people/francois_dupressoir) and Prof Steve Schneider (https://www.surrey.ac.uk/cs/people/steve_schneider), with support from Dr Santiago Zanella-Béguelin (https://www.microsoft.com/en-us/research/people/santiago/) as Microsoft Research supervisor.

Duration of Studentship: 4 years

Eligibility: The studentship will be funded by Microsoft Research and EPSRC through Microsoft’s PhD Scholarship Programme (https://www.microsoft.com/en-us/research/academic-program/phd-scholarship-europe-middle-east-africa). The standard EPSRC eligibility rules (https://www.epsrc.ac.uk/skills/students/help/eligibility/) apply, including some residence requirements. Normally, to be eligible for the studentship, the student must have no restrictions on how long they can stay in the UK and have been ordinarily resident in the UK for at least 3 years prior to the start of the studentship (with some further constraint regarding residence for education).

Vacancy Information: The student will be registered with the University of Surrey and join a team of researchers at the Surrey Centre for Cyber Security (http://www.surrey.ac.uk/sccs), one of only 14 UK government-recognised Academic Centres of Excellence in Cyber Security Research (ACE-CSR, https://www.ncsc.gov.uk/articles/academic-centres-excellence-cyber-security-research).

Project Description

Providing and Verifying Security on Compromised Platforms

Recent years have seen tremendous progress in the development of formal techniques and tools for the development of software systems that are and remain correct and secure against traditional network-based adversaries. This recent progress is a significant step towards establishing trust in the security of computer systems and digital infrastructure in the presence of misbehaving state-level actors (that may, for example, tamper with standards and software or compromise service providers), as it supports the production of independently-verifiable evidence of the security of a system.

However, the threat models considered so far have necessarily been limited to network-based adversaries. This does not take into account the growing number of security-critical systems—including consumer appliances, but also infrastructure—that are deployed without physical security, giving a determined adversary a lot more capabilities through physical access. For example, such an adversary could observe physical side-channels (timing, power consumption) that leak information about the data being manipulated by a device, or could perform fault attacks to tamper with the very execution of the system.

Establishing trust in the presence of these more powerful threats often requires the use of trusted hardware—small, tamper-resistant hardware tokens that serve as roots of trust to bootstrap digital security in adversarial physical environments. However, the precise security guarantees expected of such roots of trust (for example, Trusted Platform Modules (TPM), Intel® SGX, or Arm Trustzone) are still not fully understood, and they are often difficult for developers of hardware or software appliances to use effectively to bootstrap security. This difficulty comes in part from their complexity, but also from the fact that application developers are often assumed to understand security—including security against side-channel and physical attacks. This assumption is, in practice, often wrong.

In this project, the student will, in collaboration with supervisors and a growing team of researchers, investigate all aspects of these roots of trust from a formal point of view. This will involve:
- Understanding and formalising the security properties of these roots of trust in powerful adversary models;
- Developing and applying techniques and tools to prove that given implementations of such roots of trust do indeed provide these security properties;
- Developing techniques and tools that make it easier for application developers to check that their use of their chosen root of trust provides them with the level of security they expect.

Application domains of relevance to the Department include electronic voting, automotive and transport security, and electronic health.

The student may focus in-depth on one or two of these aspects, or more superficially cover all three.