SCorCH: Secure Code for Capability Hardware
Lead Research Organisation:
The University of Manchester
Department Name: Computer Science
Abstract
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.
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.
Planned Impact
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.
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.
Publications

Aljaafari F
(2022)
Combining BMC and Fuzzing Techniques for Finding Software Vulnerabilities in Concurrent Programs
in IEEE Access



Bitchebe S
(2023)
GuaNary: Efficient Buffer Overflow Detection In Virtualized Clouds Using Intel EPT-based Sub-Page Write Protection Support
in Proceedings of the ACM on Measurement and Analysis of Computing Systems

Brauße F
(2023)
The ksmt calculus is a d-complete decision procedure for non-linear constraints
in Theoretical Computer Science

Cavalcante T
(2022)
Formal synthesis of non-fragile state-feedback digital controllers considering performance requirements for step response.
in Scientific reports
Title | Conffuzz Artifacts |
Description | This repository contains a data set of CIVs generated by ConfFuzz. Please see the paper for more information: Lefeuvre, Hugo, Vlad-Andrei Badoiu, Yi Chien, Felipe Huici, Nathan Dautenhahn, and Pierre Olivier. "Assessing the Impact of Interface Vulnerabilities in Compartmentalized Software." In Proceedings of 30th Network and Distributed System Security (NDSS'23). Internet Society, 2022. |
Type Of Material | Database/Collection of data |
Year Produced | 2023 |
Provided To Others? | Yes |
Impact | We just open sourced the data set so no particular impact yet. |
URL | https://github.com/conffuzz/conffuzz-ndss-data |
Title | FlexOS Artifacts |
Description | These are the artifacts for our paper "FlexOS: Towards Flexible OS Isolation". The paper was accepted in the ASPLOS'22 conference and we went through artifact evaluation. The artifact contains the source code of FlexOS, the proof-of concept of our flexible isolation approach, along with all scripts necessary to reproduce the paper's measurements and plots. The goal of this artifact is to allow readers to reproduce the paper's results, and build new research on top of FlexOS. Please note that these artifact received the "best artifact award" at the conference (see here: https://asplos-conference.org/). |
Type Of Material | Database/Collection of data |
Year Produced | 2022 |
Provided To Others? | Yes |
Impact | Received the "best artifact award" at the ASPLOS'22 conference https://asplos-conference.org/. |
URL | https://github.com/project-flexos/asplos22-ae |
Title | The FormAI Dataset: Generative AI in Software Security through the Lens of Formal Verification |
Description | FormAI is a novel AI-generated dataset comprising 112,000 compilable and independent C programs. All the programs in the dataset were generated by GPT-3.5-turbo using a dynamic zero-shot prompting technique and comprised programs with varying levels of complexity. Some programs handle complicated tasks such as network management, table games, or encryption, while others deal with simpler tasks like string manipulation. Each program is labeled based on vulnerabilities in the code using a formal verification method based on the Efficient SMT-based Bounded Model Checker (ESBMC). This strategy conclusively identifies vulnerabilities without reporting false positives (due to the presence of counter-examples) or false negatives (up to a certain bound). The labeled samples can be utilized to train Large Language Models (LLMs) since they contain the exact program location of the software vulnerability. |
Type Of Material | Database/Collection of data |
Year Produced | 2023 |
Provided To Others? | Yes |
Impact | The formAI dataset reveals that GPT-3.5-turbo introduces vulnerabilities when generating C code. The diverse set of programming scenarios exposed risky coding strategies and practices used by GPT-3.5 when handling certain tasks. We employed a zero-shot prompting method to encompass numerous programming situations for C code generation using GPT-3.5-turbo. We used the ESBMC bounded model checker to produce formally verifiable labels for bugs and vulnerabilities. In our experiment, we allocated a verification time of 30 seconds to each program, with the unwinding parameter set to 1. In total 197800 vulnerabilities were detected by ESBMC. Some programs contain multiple different errors. The labeling is provided in a .csv file, which includes: Filename, Vulnerability type, Function name, Line number, and Error type. In addition, we offer a separate .csv file containing the C code as a separate column. Finally, we connected the identified vulnerabilities to CWE identifiers. Based on these findings, we answer our research questions: - RQ1: How likely is purely LLM-generated code to contain vulnerabilities on the first output when using simple zero-shot text-based prompts? Answer: At least 51.24\% of the samples from the 112,000 C programs contain vulnerabilities. This indicates that GPT-3.5 often produces vulnerable code. Therefore, one should exercise caution when considering its output for real-world projects. - RQ2: What are the most typical vulnerabilities LLMs introduce when generating code? Answer: For GPT-3.5: Arithmetic Overflow, Array Bounds Violation, Buffer Overflow, and various Dereference Failure issues were among the most common vulnerabilities. These vulnerabilities are pertinent to MITRE's Top 25 list of CWEs. |
URL | https://github.com/FormAI-Dataset |
Title | ConfFuzz |
Description | This repository contains the main tree of our ConfFuzz proof-of-concept. ConfFuzz is an in-memory fuzzer aimed at detecting interface vulnerabilities in compartmentalized contexts. ConfFuzz is a cooperation between the University of Manchester, University Politehnica of Bucharest, Rice University, and Unikraft.io. It has been accepted to appear in NDSS'23. For more information see the paper Lefeuvre, Hugo, Vlad-Andrei Badoiu, Yi Chien, Felipe Huici, Nathan Dautenhahn, and Pierre Olivier. "Assessing the Impact of Interface Vulnerabilities in Compartmentalized Software." In Proceedings of 30th Network and Distributed System Security (NDSS'23). Internet Society, 2022. |
Type Of Technology | Software |
Year Produced | 2023 |
Open Source License? | Yes |
Impact | We just open sourced the tool so no impact yet |
Title | FlexOS |
Description | At design time, modern operating systems are locked in a specific safety and isolation strategy that mixes one or more hardware/software protection mechanisms (e.g. user/kernel separation); revisiting these choices after deployment requires a major refactoring effort. This rigid approach shows its limits given the wide variety of modern applications' safety/performance requirements, when new hardware isolation mechanisms are rolled out, or when existing ones break. We present FlexOS, a novel OS allowing users to easily specialize the safety and isolation strategy of an OS at compilation/deployment time instead of design time. This modular LibOS is composed of fine-grained components that can be isolated via a range of hardware protection mechanisms with various data sharing strategies and additional software hardening. The OS ships with an exploration technique helping the user navigate the vast safety/performance design space it unlocks. We implement a prototype of the system and demonstrate, for several applications (Redis/Nginx/SQLite), FlexOS' vast configuration space as well as the efficiency of the exploration technique: we evaluate 80 FlexOS configurations for Redis and show how that space can be probabilistically subset to the 5 safest ones under a given performance budget. We also show that, under equivalent configurations, FlexOS performs similarly or better than several baselines/competitors. |
Type Of Technology | Software |
Year Produced | 2021 |
Open Source License? | Yes |
Impact | Paper accepted at the prestigious A* ASPLOS conference. |
URL | https://github.com/project-flexos/unikraft |
Title | FuSeBMC: A White-Box Fuzzer for Finding Security Vulnerabilities in C Programs |
Description | FuSeBMC is a test generator for finding security vulnerabilities in C programs. FuSeBMC incrementally injects labels to guide Bounded Model Checking (BMC) and Evolutionary Fuzzing engines to produce test cases for code coverage and bug finding. Additionally, FuSeBMC uses both engines to produce smart seeds. First, the engines run with a short time limit on a lightly instrumented version of the program to generate the seeds. The BMC engine is particularly useful in producing seeds that can pass through complex mathematical guards. Then, FuSeBMC runs its engines with extended time limits using the smart seeds created in the previous round. FuSeBMC manages this process in two main ways using its Tracer subsystem. Firstly, it uses shared memory to record the labels covered by each test case. Secondly, it evaluates test cases, and those of high impact are turned into seeds for subsequent test fuzzing. We evaluated FuSeBMC by participating in Test-Comp 2022 to test the tool's ability in two categories of the competition: code coverage and bug detection. The Test-Comp 2022 results show that we significantly increased our code coverage score from last year, outperforming all tools in all categories. During years (2021 & 2022), FuSeBMC achieved six awards (4 Gold Medals, 1 Silver Medal, 1 Bronze Medal). |
Type Of Technology | Software |
Year Produced | 2021 |
Open Source License? | Yes |
Impact | FuSeBMC is part of a broader effort from the software testing community to find security vulnerabilities in programs. Since its first publication in 2021, FuSeBMC has attracted the attention of several researchers both from academia and industry. As FuSeBMC is currently the only test case generator that efficiently and effectively combines various Fuzzing and BMC techniques, we aim to verify industrial-grade learning-based systems implemented in C in the following years of the EnnCore award. |
URL | https://ssvlab.github.io/lucasccordeiro/papers/fase2022.pdf |
Title | Ports of the Unikraft/FlexOS operating systems to the ARM Morello platform |
Description | This is our ports of the Unikraft and FlexOS operating systems to the ARM Morello platform, using its hybrid capability mode. This software was developed as part of the research effort that led to this paper: John Alistair Kressel, Hugo Lefeuvre, and Pierre Olivier, "Software Compartmentalization Trade-Offs with Hardware Capabilities", Workshop on Programming Languages and Operating Systems (PLOS), 2023 For more information see the project's website https://olivierpierre.github.io/project-flexcap/ |
Type Of Technology | Software |
Year Produced | 2023 |
Open Source License? | Yes |
Impact | We published a paper in the PLOS'23 workshop. We were invited to give a talk presenting that research at the CHERITech'24 workshop. |
URL | https://olivierpierre.github.io/project-flexcap/ |
Title | Vampire theorem prover 4.6 |
Description | An automated theorem prover able to construct proofs (or in some cases establish that no proof can be found) for problems in polymorphic first-order logic with theories (arithmetic, arrays, datatypes) and higher-order logic. |
Type Of Technology | Software |
Year Produced | 2021 |
Open Source License? | Yes |
Impact | Vampire is used within academic and industrial projects as a black box able to discharge sub-problems (such as verification conditions). |
URL | https://vprover.github.io/ |