Persistent systems security and programme verification
Start date1 October 2019
Total funding: £68,000 including fees and stipend of £16,000 per year
Persistent memory (e.g., NVDIMM-P and F-RAM) is a new memory technology that preserves state in case of a system crash or power loss. It has the potential to vastly improve system speed and stability. However, it introduces several research challenges: rebooting from persistent memory can leave the system in an unsafe or insecure state. In fact, the use of a persistent state exacerbates known safety and security issues from standard systems.
The security of software and computer systems is increasingly being breached due to low-level micro-architectural features (e.g., caches with speculative execution), which can enhance system performance but have security vulnerabilities when their effects are observable.
This project will focus on non-volatile memory, an upcoming memory paradigm where memory contents persist even in the presence of a system crash. Non-volatile memory is already being deployed and is expected to become pervasive in the coming years since it improves both speed and stability. However, it also presents greater security risks. Because memory contents are preserved after power loss, there is a greater attack surface in comparison to traditional memory systems. For example, an attacker may deliberately shut down a system and access secrets upon reboot and recovery.
This project will develop models for non-volatile memory to address such security vulnerabilities and verification techniques to prove that the systems developed are secure.
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.
We ask the following four key research questions:
Q1. How does persistency for low-level read/write actions interact with known semantics modelling information flow?
Q2. What are the high-level security requirements of persistent storage abstractions?
Q3. How can these security requirements be guaranteed by an implementation?
Q4. How can the security verification techniques be mechanised?
For a candidate profile, please see the Eligibility tab above.
Related linksPersistency for Synchronization-Free Regions Intel® Optane™ Technology Non-volatile random-access memory
Open to UK or EU applicants.
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).
- Bachelor’s degree in Computer Science or Mathematics (UK equivalent first class or an upper second)
- 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.
- IELTS of 6.5 or above
- 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)