Back to search results

PhD Studentship Opportunity in Persistent Safety and Security

University of Surrey

Qualification Type: PhD
Location: Guildford
Funding for: UK Students, EU Students
Funding amount: £16,000 per annum for UK/EU citizens only
Hours: Full Time
Placed On: 2nd May 2019
Closes: 30th June 2019

Studentship description

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. 

Entry requirements


  • 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.


  • 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)


University fees will be fully covered, with a stipend of approx. £16,000 per annum for UK/EU citizens only.

How to apply

Applicants should apply through the PhD Computer Science course page: 

Please include your studentship title on your applications. For project inquiries, please contact Brijesh Dongol (

Closing date for applications

Sunday 30th June 2019

Application enquiries

Brijesh Dongol,

We value your feedback on the quality of our adverts. If you have a comment to make about the overall quality of this advert, or its categorisation then please send us your feedback
Advert information

Type / Role:

Subject Area(s):


PhD tools
More PhDs from University of Surrey

Show all PhDs for this organisation …

More PhDs like this
Join in and follow us

Browser Upgrade Recommended has been optimised for the latest browsers.

For the best user experience, we recommend viewing on one of the following:

Google Chrome Firefox Microsoft Edge