|Funding for:||UK Students, EU Students|
|Funding amount:||£16,000 per annum for UK/EU citizens only|
|Placed On:||2nd May 2019|
|Closes:||30th June 2019|
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?
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.
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: www.surrey.ac.uk/postgraduate/computer-science-phd
Please include your studentship title on your applications. For project inquiries, please contact Brijesh Dongol (firstname.lastname@example.org).
Closing date for applications
Sunday 30th June 2019
Brijesh Dongol, email@example.com
Type / Role: