Security verification (obtaining mathematical proof of the behaviour of systems and pieces of hardware) is embedded into many of our projects, ensuring that formal guarantees are built into emerging technologies.
Our researchers are experts in correctness, liveness (ensuring that the technology is always ready to take the next step) and verification of security properties (ensuring that the system is not behaving in an insecure way).
Verifiably correct transactional memory
Multi-core computing architectures have become ubiquitous over the last decade. To ensure correctness, concurrent programs on multicore systems must be properly synchronised, but synchronisation invariably introduces sequential bottlenecks, causing performance to suffer.
This project addresses programmability of concurrent programs through the use of transactional memory, focusing on some of the main challenges surrounding this, and taking the key steps necessary to facilitate wide-scale adoption.
In particular, the team will develop theoretical advances in our understanding of transactional memory correctness, methodological advances in verification techniques for it, and pragmatic advances via the development of application-aware transactional memory designs. Verification tools will support each of these steps.
- Budget: £397,680
- Funding body: EPSRC
- Centre lead: Dr Brijesh Dongol
- Partners: University of Sheffield, University of Kent associate partners: ARM Ltd, Mozilla Limited, De Paul University, University of Augsburg, University of Paderborn, University of Queensland, Victoria University of Wellington
- Timeframe: 2018-2021.
Fighting strong adversaries with TEEs
While trusted execution environments (TEEs) provide hardware-support for security against strong adversaries, they are complex and their use is prone to error.
One current project is an EPSRC-sponsored iCase studentship in collaboration with Microsoft which aims to come up with a model of what secure functionality in TEEs should provide, and develop formal techniques and tools for verifying applications built on these.
Safer contactless payment
Contactless payments require no user input and are initiated spontaneously, this makes them vulnerable to attacks based on cheap wireless technology. There is therefore an urgent need for mathematical proofs that a given contactless payment was made intentionally by a genuine card holder rather than it being forged by a malicious party on the card holder’s behalf.
A PhD studentship supported by the National Cyber Security Centre and Consult Hyperion is currently investigating the cryptographic design and provable security of the ubiquitous contactless Europay, Mastercard and Visa (EMV) payment systems, with the aim of protecting customers from the threat of fraudulent payments.