SCorCH will apply formal analysis tools to detect security issues in capability hardware. We give a brief overview of those concepts (in reverse order) here.

Capability Hardware

The underlying idea behind capability hardware is that the architecture is extended with so-called capabilities that provide enhanced security features. This project builds on the the CHERI project led by the University of Cambridge and SRI International since 2010. The CHERI website contains a lot of information on the architecture and developments so far. They summarise CHERI as:

CHERI (Capability Hardware Enhanced RISC Instructions) extends conventional hardware Instruction-Set Architectures (ISAs) with new architectural features to enable fine-grained memory protection and highly scalable software compartmentalisation. The CHERI memory-protection features allow historically memory-unsafe programming languages such as C and C++ to be adapted to provide strong, compatible, and efficient protection against many currently widely exploited vulnerabilities.

As described below, this additional hardware support is very welcome in avoiding certain classes of security vulnerabilities but now requires tools to ensure that software is using it correctly, which is the focus of SCorCH.

In 2019, UKRI announced the Digital Security by Design Challenge in partnership with ARM. As part of this challenge, ARM announced the Morello Board, a CPU, SoC, and board integrating CHERI support into an ARMv8-A baseline system. The CHERI website provides further details on what this will entail.

Making things Secure

SCorCH will focus on ensuring security by supporting the formal analysis of two classes of vulnerability mitigations.

Memory Safety

The majority of code that runs will, at some point, rely on code written in C or C++. Much of our low-level infrastracture is written directly in C/C++ and the ecosystems of many higher-level languages often use C/C++ under the hood. A well-known issue with C and C++ is that it is not memory safe, e.g. it is possible to access arbitrary parts of the memory, which can cause many problems.

Common memory safety issues are well-known. For example, the classic stack overflow where a program writes off the end of a stack into memory it should not access. Other issues are more subtle, such as use-after-free where a dangling pointer is dereferenced.

So why do we care about memory safety? In a recent talk, Matt Miller from the Microsoft Security Response Center explained that roughly 70% of vulnerabilities addressed through security updates were memory safety issues. Malicious actors can take advantage of memory safety issues to subvert protection mechanisms, leak information, and more.

What can we do? CHERI aims to build memory safety protection in at the architectural level via smart pointers called capabilities. However, this requires software to make proper use of these pointers. SCorCH will use formal analysis techniques (model checking) to statically analyse C programs using CHERI to detect potential memory safety issues.

Compartmentalisation

Ultimately, given the complexity of modern systems, exploits and attacks are inevitable. So how do we minimise the impact if it happens? We want to restrict the damage to the smallest part of the system that we can. This is the idea behind compartmentalisation, to put up walls between distinct components of a system and enforce that separation.

CHERI provides hardware-enabled support for compartmentalisation through memory tags. However, again we need to ensure that the software is using these mechanisms correctly. SCorCH will utilise a combination of static and dynamic analysis to ensure that compartmentalisation strategies are implemented correctly in code.

Formal Analysis

SCorCH will leverage powerful and mature formal analysis techniques to provide a SCorCH verification stack that can automatically detect security vulnerabilities in code utilising capability hardware.

Model Checking

Abstractly, model checking is the process of checking whether a finite-state model or abstraction of a system meets a given specification. This specification may be as simple as we never reach a bad state or may relate to the order in which states of the system are reached (e.g. a pointer is never dereferenced after it is freed).

Algorithmically, model checkers work by exploring the state space of the system. This runs into scalability issues when the state space is ample and decades of research has provided a range of solutions to this issue, including symbolic representation of the state space, and bounded model checking where the state space is explored at iteratively greater depths.

SCorCH will utilise two bounded software model checkers - ESBMC and CBMC, developed at Manchester and Oxford, to search for memory safety issues and will employ hardware model checking techniques to check security properties of the underlying architectural design.

Runtime Verification

Whilst static analysis techniques such as model checkers have enjoyed considerable success in recent years, they can still struggle when we bring together many components of a system, thus exploding the state space. Additionally, static techniques must always approximate actual behaviour as some things are necessarily unknown.

Conversely, runtime verification is a lightweight dynamic analysis technique that aims to check that the current run of a system conforms to the given properties. SCorCH will explore a hybrid, collaborative, approach where runtime verification and (bounded) model checking cooperate to detect security vulnerabilities.

Automated Reasoning

Automated theorem provers are the workhorse of the verification community. A typical approach is to translate a given task into a series of logical proof obligations to be handled by a theorem prover. This process includes the above model checking tools, as well as tools for directly proving security properties of hardware designs (utilised elsewhere in the CHERI ecosystem).

To reason about proof obligations involving capabilities, it is necessary to translate their properties into logic alongside the property being checked. SCorCH will extend world-leading automated theorem provers (Vampire and iProver) with native support for the theory of capabilities, thereby improving their performance in this setting.