HD-Sec: Holistic Design of Secure Systems on Capability Hardware
The HD-Sec project will address engineering challenges in establishing and formally verifying the relationship between application-level security requirements and secure software implementations running on capability hardware.
Even if software has been verified as secure, it is likely to be running on hardware that is vulnerable to cyber-attack because of poor memory protection. Capability hardware, such as the CHERI architecture, provides a range of memory protection features to reduce hardware vulnerabilities. Software verification needs to make assumptions about hardware such as atomicity, separation and permission in memory operations, especially in the context of concurrent software; capability hardware should allow for simplification of these assumptions so there is a need to understand how verification can be simplified while retaining soundness.