SCorCH: Secure Code for Capability Hardware

Computers and smart phones are now used in all areas of everyday life, from business to education to entertainment. From the individual to the national level, we have become reliant on software systems and risk substantial loss if these systems fail or have their security compromised. The only way to protect against this is to ensure that the software has no inherent weakness, and this requires that we use the power of mathematics to ensure that the software is both safe and secure.

As software systems grow more complex the potential for failure grows. Traditional testing approaches become unscalable and give weaker assurances about the safety of software systems. Similarly, our software systems are increasingly subject to attacks from those who seek to exploit our dependence on technology for their own nefarious purposes. These so-called cyber attacks are becoming more elaborate, actively seeking to subvert existing methods of detection. Only by removing the underlying vulnerabilities we can truly protect ourselves. Therefore, to properly handle notions of safety and security we must focus on fundamental properties of software systems and reason about them generally.

However, software systems are not isolated, they run on hardware alongside other software and the safety and security of any software is dependent on this context. Ideally, we have safety and security `all the way down' from semicolons to silicon. A recent effort, let by ARM and the University of Cambridge, has introduced a new model for safe and secure systems: Capability Hardware. The most significant set of security vulnerabilities stem from memory being accessed or manipulated by a process that should not be allowed to access or manipulate that memory. The idea behind Capability Hardware is to provide security guarantees at the hardware level with special so-called capabilities, a special kind of memory that knows who is allowed to do what with it. The result should be much more secure and robust software systems. However, now that we have more security at the hardware level, it is key that we ensure that this is correctly utilised at the software level.

This project aims to transport the substantial advanced in software verification to the setting of this new capability hardware. In general, we will extend existing tools and create new tools able to reason about the safety and security of industrially relevant software systems running on Capability Hardware. There will be a significant focus on achieving high technological readiness, ensuring that when the international community is ready to embrace Capability Hardware there already exists a mature set of tools able to verify the safety and security of the software sitting on top of it.

Through creating the ICSF Digital Security by Design Challenge the Industrial Strategy Challenge Fund and EPSRC have identified an opportunity to have a significant impact on the landscape of embedded systems, IoT and Edge computing through a focus on Capability Hardware. We will join this effort in contributing to a shared vision of fully-verifiable safe and secure software, where underlying hardware/software architectures are built with strong symbolic and mathematical guarantees.

We aim to make a significant impact on three groups of people and emphasise these expected impacts and how we plan to achieve them below.

Users of Software for Capability Hardware. Firstly, ARM chips are ubiquitous and the hope is that eventually, an ARM chip with capabilities will become ubiquitous too, providing security guarantees to the billions of users of devices containing such chips. We will contribute to this vision by providing tools to support the development of safe and secure hardware running on these devices. To deliver impact we will stay aligned to the overall vision of this generational challenge.

Developers of Software for Capability Hardware. These are our end-users, the people we want to be using our verification tools. The aim is to support and optimise their work in assuring the security of the software they write to run on top of capability hardware. It is, therefore, important that not only ensure that the tools do the job required (e.g. verification) but that they are usable and developers are supported in their use. To this end, we will (i) arrange user workshops to provide tutorials and showcases for the tools, and (ii) develop additional resources in the form of online demonstrations, user guides, and demonstration projects. The ultimate goal is for the SCorCH verification stack to be part of the toolbox of all future developers targeting capability hardware.

Developers of Software Verification and Automated Reasoning Tools. The development of such tools is gaining a growing interest in academia and industry. Alongside our efforts to support Capability Hardware, we are also proposing key contributions to such techniques that will impact the broader community. Ideas from SCorCH can be implemented in other tools and the SCorCH verification stack itself may be utilised by other tool-chains. To support this activity we will establish two new workshop series, to be co-located with leading conferences, on the topics of Automated Reasoning Support for Security and Scalable Program Verification.

Overall, we expect SCorCH to contribute to more secure devices in the long-term, happier software developers for capability hardware in the medium-term, and a growing community of researchers interested in building tools to produce safe and secure software in the short-term.