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)--a fair exchange protocol that is highly sensitive to information exfiltration.
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.

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).

Documents and publications

This section includes links to the technical reports and referred publications produced from CAMB's activities.

• The Morello Board Set-up document details our very personal experience gained from the set-up of the Morello Boards.

Git repositories

CAMB-DSbD (Cloud Attestables on Morello Boards: a DSbD project) is a Git organization account that groups all the git repositories that contain the software produced from CAMB's tasks.

• The FEWD repo contains the software of a fair exchange protocol (an example of an exfiltration sensitive process) that we will use as a payload to test the attestables.

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.

Recent publications

This section includes links to recent documents on capabilities and Morello Board.

• 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.

Related publications

This section includes links and brief summaries of documents that we consider directly related to CAMB's activities.

Visionary papers

• Redhouse Gases: A manifesto for re-decentralization

  In this position paper Jon expresses his concern about the gradual centralisation of the Internet understood as the concentration of ownership and management of core services and data in a few giant companies. He argues that centralisation leads to several technical (latency, energy consumption, privacy,etc.) and economic problems. Regarding the latter, it leads to monopolisation which has been proven to discourage innovation. He advocates for re-decentralidation and highlight the challenges involved.

The seminal papers on capabilities

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.