skip to primary navigationskip to content

Department of Computer Science and Technology

Research Projects

CAMB (Cloud Attestables on Morello Boards)

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:


Manuals

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

Recent publications

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

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.


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