AdaCore Blog

CheriBSD: A Showcase for Hardware-Supported Security

CheriBSD: A Showcase for Hardware-Supported Security

by Johannes Kliemann

Introduction

Over the course of the last few years and as part of the 'Edge Avionics' project, funded by the Rapid Capabilities Office (RCO) of the UK Royal Air Force (UK RAF), AdaCore has been developing toolchain solutions for Capability Hardware Enhanced RISC Instructions (CHERI) microprocessor architectures. In addition, AdaCore evaluated security claims made by the CHERI community through the Digital Security by Design (DSbD) initiative. The goal was to inform Edge Avionics project partners about the level of security assurance offered by the Arm Morello microprocessor; a modified Arm Neoverse N1 supporting the Armv8-A architecture and conforming to the CHERI compartmentalization specification. The DSbD project is now in the final stages, the overarching goal of mass adoption of CHERI-architectures is now looked after by the CHERI Alliance.

The investigation strategies, security verification specifics, and results are publicly available. More specifically, during the Embedded Real-Time Systems conference in Toulouse, France, in 2024, AdaCore presented a paper titled "Security by Default - CHERI ISA Extensions Coupled with a Security-Enhanced Ada Runtime." The paper, which has since been published in the conference journal <ERTS 2024 Tu.4.c.1>, discusses security claims around CHERI and the direct role the hardware can play in achieving security airworthiness. The paper can be read on our website, and you can read more about the report in this previous blog.

Furthermore, all materials and techniques required to reproduce the security verification tests, including the ones discussed in this blog, are publicly available via our AdaCore CHERI examples repository on GitHub.

Today's blog will focus on a particularly interesting security measure offered by the CheriBSD operating system: library-level compartmentalization!

CheriBSD is a Capability Enabled, Unix-like Operating System that extends FreeBSD to take advantage of Capability Hardware on Arm’s Morello and CHERI-RISC-V platforms. CheriBSD implements memory protection and software compartmentalization features, and is developed by SRI International and the University of Cambridge. To learn more about CheriBSD be sure to visit www.cheribsd.org.

The Problem Space

Operating systems and software libraries are at the core of modern computing. They enable modern features that cover increasingly complex use cases by encapsulating that complexity and providing abstractions. A significant part of this software is written in memory unsafe languages like C. Using unsafe memory languages has often led to security problems and will continue to do so in the foreseeable future.

There are safer languages that can match the performance of C, such as Ada and Rust, that have gained popularity and are increasingly used for new libraries and operating systems. While these will improve the situation with newly written code, they will unlikely solve the problem with existing software. There are millions, if not billions, of lines of C code. Rewriting all of these in memory-safe languages would require an unrealistic amount of effort and time.

The CHERI architecture extension aims to solve these problems on a language-agnostic level. It provides a memory model that allows tagging pointers to ensure their validity and also allows reducing their permissions if needed. The hardware ensures that invalid memory accesses, e.g. through an access outside the bounds associated with a pointer, are detected and an exception is raised instead of continuing to run the affected code in an undefined state. This improves the memory safety of unsafe languages but also enhances unsafe features of otherwise safe languages.

CheriBSD is a FreeBSD derivative ported to the ARM Morello platform, an Aarch64-based implementation of CHERI. It shows that existing code can be ported to a CHERI platform with manageable effort while still benefitting from the capabilities provided by the CHERI architecture.

Security Limitations of OS Processes

Operating systems provide their own security mechanisms, most notably the concept of processes enabling them to isolate different applications from each other. This isolation is done by providing each process with its own address space. When starting a process the kernel populates this address space with some resources, such as memory for the heap and static allocations. The process can also request further memory from the operating system, e.g. for heap allocations.

However, within its allocated memory, the process is free to do whatever it wants. From the system's perspective, the static allocations, the heap, and the stack are only unstructured blocks of memory. The application’s code is responsible for using this memory properly. This also means that any code executed in the process's context has access to all of its memory.

Most applications use software libraries to access functionality already implemented by others. However, this also means that the library’s code has access to the whole process, and any software defects in this library also affect the whole process. Even worse, a third-party library may be affected by a supply chain attack, executing malicious code in the context of the process.

Shared Libraries and Compartmentalization

While attacking software through defects on CHERI is extremely difficult, if not impossible, malicious code is still able to extend its access to the program beyond its assigned resources. We have evaluated both scenarios in our research. We executed a return-oriented programming exploit on a CHERI system and were able to validate that this attack was stopped, even when assuming very favorable conditions for the attacker. However, we were able to show that malicious code, e.g. as part of a software library, can extend its access to the program beyond its intentionally assigned resources.

Within complex scenarios, such as running an operating system like CheriBSD, it is very difficult to evaluate every library used due to the significant amount of third-party code involved. With static libraries, this is even more of a problem since they are linked into the application at compile time, making them indistinguishable from application code.

Furthermore, operating systems often use shared libraries for third-party code, one reason being to reduce disk usage and allow centralized updating. Shared libraries are only referenced at compile time, but the library itself is linked at runtime time by the system's dynamic linker.

This is where CheriBSD’s compartmentalization feature comes into play. It uses CHERI’s capabilities to efficiently execute shared library code in its own compartment within the same process. Similar approaches have been taken on other systems; however, they often have a significant performance impact due to using separate processes for shared libraries. Because it runs within the same process, CheriBSD’s mechanism incurs only a small overhead.

We evaluated this feature in our research and were able to show that with compartmentalization enabled, our malicious library could not access information beyond its own compartment. Our attack path, involving decoding and tracing capabilities on the stack until we could maliciously manipulate program state, no longer worked; we could no longer find capabilities allowing access to information outside our own compartment. It is important to note that libraries still have access to memory accessible through capabilities intentionally passed as an argument to a library call. However, this should be guarded against through inspection of the library API during system design; it is not a security limitation in the CheriBSD compartmentalization model.

Conclusion

CHERI significantly reduces the risk that a software defect causes a loss of integrity or confidentiality by raising a hardware exception if the memory restrictions employed by it are violated. The specific impact on the executing application, when a CHERI hardware exception is raised, is dependent on how the underlying runtime catches and processes the hardware signals. Typically the impact is either causing the application to stop executing entirely or, as is the case with AdaCore's GNAT Pro for CHERI solutions, the hardware exception will be propagated to an application software exception handler and the application will decide how to react to the fault. Either way, the CHERI hardware trap ensures that the application never enters an undefined and possibly dangerous state. While this still impacts a system's availability, it prevents malicious code execution or unauthorized access to secrets.

While it may seem that an application stopping instead of continuing to run may cause problems in safety-critical contexts, an application running in an undefined state is arguably a much worse scenario. Safety-critical applications are designed and built with strict rules, ensuring their correct and safe behavior in all circumstances. If the appearance of an exception is taken into account here it can be handled properly. For example the affected system could go into a properly defined recovery process. If the defect is not detected the availability of the application may seemingly not be impacted, but the assumptions under which the safety of the software can be guaranteed no longer hold causing a reduction in safety assurance and an invalid safety case argument.

Furthermore, CheriBSD proves that porting large existing code bases to this new platform can be done with manageable effort while still benefiting from enhanced security. The security mechanisms provided by CHERI, while overlapping with those provided by an operating system, enhance existing security mechanisms.

Finally, CheriBSD’s compartmentalization feature goes beyond the already strong protection against software faults. It allows executing code with reduced trust and can constrain a security breach initiated via a shared library to just the memory regions allocated to that library.

Posted in #CHERI   

About Johannes Kliemann

Johannes Kliemann

Johannes Kliemann is a cross and embedded engineer at AdaCore. He specializes in systems architecture and security and is interested in formal verification, operating systems development and embedded devices.