Contents |
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.
- Concealment: It prevents observation of its data and computation, that is, it behaves like a black box.
- Independent execution: It prevents changes to the code that it is running.
- 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.