What is CAMB?

CAMB is a research project funded by UKRI as part of the UKRI’s DSbD (Digital Security by Design) challenge. It started in Apr 2021 to run for 30 months.

People

• Jon (jon.crowcroft@cl.cam.ac.uk) is the PI of the project: the Marconi Professor of Communications Systems in the Computer Lab, at the University of Cambridge. He is the PI (principal investigator) of the CAMB's project and responsible for overall guidance.


• Carlos (carlos.molina@cl.cam.ac.uk) is the researcher-coinvestigator and contact of the project: a senior researcher in the Computer Lab, at the University of Cambridge. He is responsible for the implementation and administration activities of the project.


• Dann (dann.toliver@todaqfinance.com) a non-grant claiming partner of the project from TODAQ and a visitor to the Computer Lab, at the University of Cambridge. He acts as an advisor in implementation issues.


• Hazem (hazemdanny.nakib@gmail.com) a non-grant claiming partner of the project from Sentinel Capital Group and a visitor to the Computer Lab, at the University of Cambridge. He acts as an advisor in legal, financial and commercialization issues.

Overview

CAMB's overall aim is to take advantage of the built-in hardware capabilities of Morello Boards and the CHERI software stack to implement attestables.

The Morello Board (also called the Morello System Development Platform or SDP) is an experimental architecture protection model that resulted from the extension of Armv8.2-A profile. It implements the 129-bit Capability Hardware Enhanced RISC Instructions (CHERI) capability protection model. Physically, the Morello Board is a prototype system-on-chip (SoC) designed by ARM as a development board and released to industry and academic partners for testing in spring 2022.

CHERI is an Instruction Set Architecture (ISA) that improves system memory security. It includes instructions for scalable memory compartmentalisation.

An attestable is a conceptual model that can serve as the basis for implementing secure execution environments that are capable of executing exfiltration-sensitive applications without leaking information.
At execution time, an attestable guarantees the following three properties against external code, including its initiator.

1. Concealment: It prevents observation of its data and computation, that is, it behaves like a black box.
2. Independent execution: It prevents changes to the code that it is running.
3. Attestation: It can be initiated and attested by a cloud provider who can produce an attestation certificate that certifies that the attestable is able to guarantee properties 1 and 2.

CAMB's technical aim:

The aim is to build attestables on Morello Boards to test them and demonstrate that they are able to guarantee the three properties mentioned above without degrading performance severely.
In pursuit of this aim, we will use the CHERI Software Stack to implement attestables as compartments that can be nested and communicate with other compartments deployed on the same or different Morello Boards.
To test the security strengths and performance of the attestables, we will use them for executing FEWD (Fair Exchange Without Disputes). Fair exchange protocols, are run collaborativelly between two parties for exchanging items fairly, that is, either the two items are swapped or the exchange is aborted and none of the items is given away. They are used in several practical applications, for example, to exchange payment for an item sold online and to claim a delivery receipt in certified delivery. We will use FEWD because it involves computations that are highly sensitive to exfiltration.

Outcomes

CAMB has produced the following documents and software released in CAMB-DSbD (Cloud Attestables on Morello Boards: a DSbD project) Git organization account.

• Morello Board Set-up: is a document details our very personal experience gained from the set-up of the Morello Boards.
• teriOS: is a multi-tenant Trusted Execution Environment (TEE) implemented in C with some assembly lines by Kian Cross to complete is MPhil degree.
  • The tereios repo contains the sources.
  • Its current version runs on the FVP and demonstrates how TEEs with properties similar to Intel SGX enclaves' can be implemented in the current Morello Board. It explains the technical challenges that emerge mainly from the absent of a Trusted Platform Module and an attestation mechanism in the Morello Board.
  • Kian's slides provide additional thoughts about these issues.
• FEWD: is a fair exchange protocol that we are implementing to use as a use case to evaluate attestables. We have separated the code into two parts:
  1. Communication between the applications of the participants over secure channels, for example, to exchange encrypted versions of the documents under exchange. It also involves communication with a public bulletin board over secure channels. We have implemented this part in Python and uploaded the software to the FEWD repo
  2. Computation of highly sensitive information, for example to lock in and verify the documents under exchange before releasing them. Such computation need the protection of trusted execution environment like the attestables envisioned in the CAMB project. We are in the process of implementing them.
     • An atttestable is a model that satisfy strict properties aimed at preventing malicious and accidental data exfiltration. It interacts with its environment through a simple API. The Attestable Model: properties and API documents these properties and API.
     • As documented in Implementation of FEWD (fair exchange without disputes) with Attestables attestable play a central role in the implementation of FEWD.
     • The implementation of FEWD involves the creation of secure channels over the SSL/TLS protocol. Secure channels rely on the standard X.509-format certificates. For experimental work, its is desirable to use self-signed certificates. The procedure involves several technicalities and is not documented with practical examples. How to Create Self-singned Certificates might be helpful.

Introduction to cheri capabilities

Capabilities are a protection mechanism that grant or deny a program, access to resources including main memory space (defined by a range of addresses) disk files, input/output devices and other resources within the name space of the program.
They are defined as unforgeable tokens that a program either has or does not have. A capability can be though as physical key that the holder can use for opening the door to resource.
For an illuminating comparison between capabilities and access control lists (ACL) that most current protection mechanisms use, see the Secure Distributed Computing chapter of the The E Language in a Walnut book.
These examples of cheri capabilities show beginners how capabilities can be programmed in C (for example, print, set and change permission).

Related projects

CAMB is one of the the on-going projects funded by UKRI under the DSbD programme and as such, it is related to all of them. But it is particularly, related to the following projects:

• CAMB is one of the results of the work that the creators of the Centre for Redecentralisation (CRDC) have been conducting of the last two years.
• CAMB implementation will take advantage of the software produced by the CHERI research group of the Computer Laboratory of University of Cambridge.
• The CAP-TEE (Capability Architectures in Trusted Execution) is an on-going DSbD proyect of the University of Birminham and is aimed at implementing trusted execution environments using capabilities, as such, its closely related to CAMB.

Manuals

This section includes links to manuals that describe the Morello Board and CHERI architectures in detail.

• Architectures, Processors, and Devices Development Article is a seven page document by ARM that helps understand the technical terminology used by ARM in their technical documents.


• Learn the architecture - Introducing the Arm architecture is a 24 page document by ARM that explains ARM three architecture profiles (A: application, R: real time and M: microcontroller), architecture versions (e.g., Armv8-A and Armv9-A) and documentation.


• ARM Morello System Development Platform: Technical Reference Manual is a 24 page document by ARM with an in-depth description of the hardware (SoC, and back pannel with connection ports) of the Morello Board. It includes directions for setting the Morello Board up.


• Arm Architecture Reference Manual Supplement Morello for A-profile Architecture Is a comprenhensive 259 page manual by ARM that describes the Morello Board architecture at ISA level with a thorough discussion of it cability registers.


• Capability Hardware Enhanced RISC Instructions: CHERI Instruction-Set Architecture (Version 8) Is a 590 page technical report by the CHERI team of University of Cambridge that describes version 8 of the CHERI Instruction-Set architecture. An Introduction to CHERI is a shorter technical report that summarises the disscussion in 43 pages.

Publications related to capabilities

This section includes links documents realted to capabilities.

Recent publications

• Formal Reasoning about Hardware Capability Architectures is Thomas Van Strydonck's PhD dissertation on capabilities. It was completed in Jun 2022 and contains an in deeph discussion of the implementation of trusted execution environments using capabilities. It has the background to understand the approach taken by the CAP-TEE (Capability Architectures in Trusted Execution) project.


• Formal Reasoning about Capability Machines is Lau Skorstengaard's PhD dissertation on capabilities completed in Aug 2019. It examines the fundamental concepts of capabilities formally. For example, the discussion of Well-bracketed control flow (WBCF), Local state encapsulation (LSE), Linear capabilities (non-duplicable capabilities) and sealead capabilities is illuminating.


• CheriOS: Designing an untrusted single-address-space capability operating system utilising capability hardware and a minimal hypervisor is Lawrence G. Esswood PhD dissertation on the desing of a CheriOS: a microkernel that supports the implementation of secure compartments (trusted execution environments) in a trust model where even the microkernel can behave maliciously. CheriOS uses capabilities and is grounded on trusted hardware.


• Hardware support for compartmentalisation is Robert M. Norton PhD dissertation on the desing of ... expand this!

The seminal papers

The idea behind capabilities can be traced back several decades. This section lists the seminal publications.

• The seminal paper that brought capabilities to the attention of the research community interested in access control in multiprogrammed computer is Programming Semantics for Multiprogrammed Computations which was published by Dennis and Van Horn in 1966.
  
  
• Capability-Based Addressing is another seminal paper published by R.S. Fabry in 1974. It continues the discussion triggered by Dennis and Van Horn. It highlights the advantages of using capabilities as a means of addressing computer resources (objects).
  
  
• Naming and Protection in Extendible Operating Systems is a PhD dissertation completed by David D. Redell in in 1974 under R.S. Fabry's guidance. It contains a through discussion of capabilities as a concept without blurring the discussion with implementation details.
  
  
• To understand capabilities, it helps to regard them as an alternative implementation of Lampson's access matrix for granting access to computer resources under security policies. The matrix is presented in Lampson's widely cited Protection paper written in 1974.

The Introductory papers to capabilities

The seminal papers are for readers familiar with concepts of access control to computer resources in multiprogrammed computer systems. Readers outside of this category might find the following book chapters useful.

• The Capability-Based Computer Systems was written in 1984 by Henry M. Levy and contains a thorough survey and description of capability-based systems of that time. The first chapter (pp 1-18) is very accessible and explains Lampson's access matrix.
  
  
• Lampson's access matrix and other fundamental capabilities concepts are discussed in Chapter 10: Protection pp 211-245, by Donal W. Davies of the Distributed Systems-- Architecture and Implementation: An Advanced Course book published by Springer in 1981 vol 105 of LNCS.
  
  

CAMB's progress

This section shows the progress of the CAMB project. It includes links to some documents.

• 01 Apr 2022: CAMB launched.
  
  
• 10 May 2022: Project web page built.
  
  
• 26 Aug 2022: Morello Boards set-up with cheriBSD version 22.05p1.
  
  
• 10 Oct 2022: First Quaterly Report submitted.
  
  
• 06 Sep 2022: Carlos attended the #CHERITech22 Technical Workshop in King’s College.
  
  
• 12 Oct 2022: Carlos attended the DSbD All Hands in the Grand Station, Wolverhampton.
  
  
• 30 Nov 2022: Kick-off online meeting:
  attended by Carlos, Jon, Stephanie Williams (EPSRC UKRI), John Goodacre (UKRI Challenge Director, Innovate UK) and Georgios Papadakis (Senior Innovation Lead-DSbD, Innovate UK). Feed back taken and incorporated into project web page and research strategy.
  
  
• 02 Dec 2022: Carlos reacted on feed back from kick-off meeting:
  CAMB project web page update (e.g., relevance of fair exchange protocols to CAMB project, explained) and research strategy taken into account.
  
  
• 20 Dec 2022: Carlos released capability examples to chericapas Git repo:
  These examples show beginners how capabilities can be programmed in C (for example, print, set and change permission); more importanlty they are basis for the implementation of the attestables that the CAMB project will implement.
  
  
• 13 Jan 2023: Carlos upgraded Operating systems of Morello boards:
  The operating systems of two out of three Morello Boards have been upgraded from cheriBSD version 22.05p1 to the latest version 22.12 released in Dec 2022. The aim was to take advantage if the facilities newly incorporated to the cheriBSD 22.12 version; in particular to evaluate its library-based software compartmentalization as a facility for building the attestables needed by the CAMB project.
  
  
• 15 Jan 2023: Carlos updated the set-up with cheriBSD version 22.12 document.
  This document explains how to setup the Morello Boards.
  
  
• 05 Dec 2022: Kian Cross joins the project as a MPhil student to write his dissertation in a related topic under Jon's and Carlos' supervision.
  
  
• 14 Feb 2023: UKRI sends two morello boards to Dann from TODAQ.
  
  
• 31 Mar 2023: Carlos and Kian attended the CHERI Technical Workshop 2023 at the University of Glasgow.
  From discussion with UKRI people they learned that the current release of the Morello Board is aimed at the evaluation of cheri capabilities in a trust model where the application trusts the Kernel. Therefore it does not include hardware or ISA instructions to match the facilities that commercial trusted hardware like Intel SGX provides, such as remote attestation and exclusive memory access to applications.
  
  
• 17 Apr 2023: Erick Derohaniand and Jon Irving Levin (both from TODAQ in Toronto) join the Camb project as volunteers to write and contribute open source software. Both are expert software developers and interested in Rust, Wasm and others security technologies.
  
  
• 27 Apr 2023: Jon Crowcroft, Carlos and Kian attended DsBD all DSbD All Hands in De Vere Grand Connaught Rooms London WC2B 5BZ.
  
  From discussion with attendees they learned that there is no consensus about what a cheri compartment is. Different people (government, companies, developers and academics) have different definitions and therefore, have different trust models and different safety and liveness properties.
  
  
• 01 Jun 2023: Kian Cross releases teriOS to Github--the result of his MPhil dissertation.
  The accompanying 67-page pdf document ( Investigating the feasibility of using CHERI-enabled Arm Morello boards for cloud-based trusted execution) explains that teriOS is a cloud-based multi-tenant TEE (Trusted Execution Environment) platform developed for the Arm Morello Board. One of its salient features is that it assumes partial mutual distrust between TEEs and privileged code (e.g. the Kernel).
  
  
• 07 Jun 2023: Erik Derohaniand from TODAQ-in Toronto visited the Computer Lab to discuss ongoing work on Morello Boards and attestables with Carlos.
  
  
• 18 Sep 2023: Stephanie Williams (EPSRC UKRI) and John Goodacre (UKRI Challenge Director, Innovate UK) visited Jon Crowcroft and Carlos Molina in the Computer Laboratory for Mid Project review of the CAMB project.
  
  
• 16 Oct 2024: CAMB close-out meeting online attended by Stephanie Williams (EPSRC UKRI), John Goodacre (UKRI Challenge Director, Innovate UK), Georgios Papadakis (Senior Innovation Lead-DSbD, Innovate UK), Jon Crowcroft (project's PI) and Carlos Molina (Researcher Co-investigator).
  A list of pending question emerged from the project's review to be responded in the corresponding Quarterly report.
  
  
• 18 Sep 2024: Carlos attended the DSbD All Hands event in The Queen’s Hotel, Leeds. The presentations are on line.
  The Sonata board left a very good impression to the audience. A sonata board is a secure-by-design, embedded micro-controller. It has been developed by lowRISC to implement CHERIoT-Ibex, which is itself based on CHERI. Like the Morello Board, the sonata board is available for free for evaluation.
  
  
• 17 Oct 2024: A pdf doc with evaluation results of compartments created on a Morello Board with the library-based compartments tool is available from a Git repository ¹.
  The Python and C programs executed in the evaluation, the metrics collected in csv files, plots of the results, our interpretations of results and directions to replicate our experiments are available from the Git repo too.
  

¹ Safari 16.6.1 fails to open the pdf directly from Git. You might need to download it firstly or use a different browser.