CHERITech22 -- Talks
Capabilities and Information Flow
David Clark (University College London)
Hypertesting is a form of metamorphic testing that can be used to check whether software conforms to a policy or to discover what policy the software does conform to. Since it is a form of testing, the traditional caveat applies: there is no guarantee and exploration discovers what it discovers. Software syntax coverage is useful but inadequate so test sets need to be extended with high information content tests to improve exploration. Policy teleology can include confidentiality, integrity, fairness and causal discovery but policies cannot be divorced from flow (hyper)properties. A failing hypertest can be viewed as a witness to the failure of the flow property in the context of the software's policy. Recent research into hypertesting of confidentiality properties for programs has demonstrated that hypertests can identify, measure and assist in the automated repair of confidentiality leaks. In this context it is evident that leaks can be due either to memory related errors (buffer overflows, for example) or to incorrect program flow structure (transitive direct and implicit flows). A practical, scalable, flow testing technique for achieving end to end software security seems complementary to CHERI's capability based approach. Rather than noninterference, a more natural security property to test against might be Liskov and Myer's Distributed Label Model.
Intravisor: type-3 hypervisor for capability-based virtual machines
Vasily Sartakov (Imperial College London)
Intravisor uses hardware memory capabilities as a mechanism for insolation and sharing. It manages CAP-VMs (cVMs), a new VM-like abstraction that enables the execution of capability-unaware code in a constrained way. cVMs use capability-based IPC primitives for efficient cross-cVM communication. They are fully compatible with Linux due to the use of the Linux Kernel Library as a de-privileged kernel and enable the execution of native code without recompilation. In this talk, I will present the current state of the project: general idea, architecture, IPC mechanisms, the hostcall interface. I will also present new features, such as the support for pure-cap cVMs, and will discuss the future directions in the development of the project.
CHERI and Trusted Execution Environments
Jennifer Jackson (University of Birmingham)
Trusted execution environments shield sensitive computation inside a secure enclave away from the rest of the software stack and untrusted operating system. Capabilities are a powerful and flexible security mechanism for implementing fine-grained memory access control and for compartmentalizing untrusted software components. Object capabilities in particular provide encapsulation, and when invoked in pairs they can be used to trigger a domain transition into a trusted region of memory. This talk discusses object capabilities and how they can be used to access enclaves within a trusted execution environment.
Towards a Safe, High-Performance Heap Allocator: Lessons from CHERIfying snmalloc
David Chisnall (Microsoft Research Cambridge)
Memory allocators play a key role in CHERI-enlightened software. They serve as the TCB's mechanism for mapping language-level notions of objects (in particular, objects' spatial and temporal extents) into the capability bounds central to CHERI architectures. Whereas pre-CHERI allocators have adopted a number of structural or probabilistic defenses against accidental or malicious corruption, allocators have generally not been considered part of the TCB, traditionally defined in terms of process (address space) boundaries. Adapting to the privileged and sensitive position imposed by CHERI requires revising our threat models, introducing new mechanisms (spanning the full gamut of mundane to novel), and increasing the auditability of allocator code. This talk will give an overview of the problem and some of our initial and ongoing work to harden snmalloc while preserving its high performance.
Compartments and other aspects of Morello software work
Yury Khrustalev (Arm)
A lot of work is being carried out to enable Morello experimentation and research. Various tools and libraries are available for Android and Linux. These components allow building and running Morello applications on various platforms including Morello boards and help research different aspects of Morello and CHERI such as compartmentalisation. This talk will provide an overview of the work on Morello software at Arm including Android and Linux enablement status, PCuABI specification, toolchains, C libraries and tools like Cheriseed and Morello IE. Recent advances in exploring capability-based compartmentalisation will also be covered from the software point of view.
Bringing Rust support to Morello
Simon Cooksey (University of Kent)
Rust is a language with a rich type system designed to eliminate memory safety bugs in the majority of code, it has seen adoption by major tech companies like Microsoft, Mozilla, and Cloudflare, and is now a second language for the Linux kernel. We explore an approach for porting Rust to the Morello prototype hardware. This has involved changes to the Rust compiler which were interesting and an opportunity to explore some design space. This talk will tell you about the approach we took for porting Rust to Morello, and the bits of friction we encountered on the way. We will also try and give you a taste of where this work is headed next!
Data Compartmentalization for Hybrid CHERI
Andrei Lascu (King's College London)
The addition of CHERI's capabilities means that a new field of efficient and secure compartmentalization is available for programmers. However, in order to make use of these additional guarantees, we emphasise two major issues: adapting existing code to a CHERI, and reasoning about capabilities. Both of these would put great amount of work on the users of CHERI, namely programmers, and would affect the rate of adoption. Thus, we propose using hybrid CHERI, and an API to abstract away compartmentalization to a more familiar interface. Due to using hybrid CHERI, it means capabilities must be explicitly constructed, leading to easier reasoning about security guarantees. We will present our efforts of writing an API to spawn sibling VM compartments, with minimal effect on the provided user-code.
Porting C/C++ software to Morello
Alex Richardson (Google)
CHERI fundamentally changes the representation of pointers and therefore imposes certain restrictions on C/C++ code. Despite these wide-ranging changes, existing well-behaved codebases can usually be compiled for CHERI-enabled architectures such as Morello without any code changes. However, many programmers rely on implementation-defined behaviour (usually whatever worked when using GCC for x86 targets). Some of these assumptions, e.g. size_t being the same width as a pointer, no longer hold when targeting Morello and therefore existing software may require some changes -- in many ways similar to those needed in the transition from 32-bit to 64-bit. Having a mature software ecosystem with commonly used open-source libraries is essential for the adoption of CHERI. Therefore, this talk will give an overview of code patterns that are incompatible with CHERI and show techniques to find, diagnose and fix these. As part of this talk I will present compiler diagnostics as well as the CHERI-UBSan instrumentation that can be used to more accurately diagnose issues. I will also present some examples of changes made to open-source software projects such as FreeBSD, Qt, KDE, X11 and more.
