PhD Studentship Opportunity in Persistent Safety and Security

Persistent memory introduces several research challenges: unlike volatile memory, which is simply repopulated from the hard drive when a system is started, rebooting from persistent memory can leave the system in an unsafe or insecure state. Writes to the persistent store are via flush events that are controlled by both hardware and software. Here, one must ensure that causally dependent information is persisted in the correct order (in case of a system crash). Moreover, upon reboot, any secrets stored in persistent storage must not be available to unauthorised parties.

This project studies the formal verification of persistent memory systems, that is, the application of a formal and precise logical argument that the system under consideration is correct. These arguments, where possible will be incorporated into a tool such as a theorem prover or model checker so that the proofs can be performed mechanically. This opens up possibilities for automation and scaling of the proof methods.

Q1: How does persistency for existing hardware read/write actions interact with weak memory?
Q2: What are the atomicity requirements and associated safety properties of persistent storage?
Q3: What are the security implications of persistency, including side channels that could be exposed?
Q4: What are the best tools and techniques for mechanisation?

Candidate Profile.
This project would suit those that are fascinated about computing foundations, concurrent systems, programming languages, security and like to reason abstractly about problems. You may have experience with formal methods (e.g., logics) or formal verification (e.g., theorem proving, model checking).

This PhD is sponsored by the UK Research Institute in Verified Trustworthy Software Systems (VeTSS) and aims to study techniques for formally verification of safety and security properties in the presence of persistent memory. This includes a study of its impact on programming languages (in particular C++), concurrency libraries (e.g., concurrent data structures and transactional memory), and hardware (in particular ARM and Intel).

The candidate will have many opportunities to interact with the wider VeTSS community and collaborators at the University of Sheffield.

Supervisors:
Dr Brijesh Dongol is Senior Lecturer in Secure Systems with expertise in formal verification of concurrent and real-time systems, including weak memory models and transactional memory. https://brijeshdongol.github.io/

Dr Francois Dupressoir is Lecturer in Secure Systems with expertise in formal verification security and cryptographic protocols, side channel attacks, and verification tools. https://fdupress.net/

Entry requirements:
Essential:
• Bachelor’s Degree in Computer Science or Mathematics (UK equivalent 1st classification)
• Interest in verification techniques (e.g. formal methods/analysis, logics) and/or in security
• Programming experience (any language)
• Analytical skills: knowledge of foundations of computer science (e.g., discrete mathematics); ability to think independently
• Strong verbal and written communication skills, both in plain English and scientific language for publication in relevant journals and presentation at conferences.

Desirable:
• Master’s degree (UK equivalent of Merit classification or above)
• Experience in Boolean logic, and first order logic, or other specific logics
• Experience in formal verification (model checking, theorem proving or SMT solving)
• Experience of implementation and/or experimentation with verification tools
• Knowledge of cryptography and/or information security and/or networks
• Proficiency in C++ and/or Java
• Experience with a functional programming language (e.g., Haskell, Ocaml)

How to apply:
Applicants should apply through the PhD Computer Science course page: https://www.surrey.ac.uk/postgraduate/computer-science-phd
Please include your studentship title on your applications. For project inquiries, please contact Brijesh Dongol ([Email Address Removed]).