POCL 2024 - Principles of Capability Languages

Hardware support for capabilities offers the prospect of substantially increased security for the computing infrastructure that we all depend on. Capabilities are an old idea, but in the last 15 years the CHERI project, working closely with Arm and others, has proposed extensions to conventional hardware Instruction-Set Architectures (ISAs) with new architectural features based on hardware capabilities, along with CHERI dialects of C and C++, to enable fine-grained memory protection and highly scalable software compartmentalisation. This is a hardware/software/semantics co-design project, involving architecture design, hardware implementation, system software adaption, and formal semantics and mechanised proof of security properties. Arm and the UKRI Digital Security by Design Challenge (with of the order of £200m government and industry investment from 2019–2024), has developed the industrial prototype Arm Morello CHERI-ARM 64-bit CPU, SoC, and board, to evaluate and demonstrate the mass-market industrial feasibility of CHERI. Several hundred Morello boards have been shipped to various academic and industry projects for evaluation, and millions of lines of conventional C and C++ code have been ported to CHERI; additional explorations of CHERI are underway in Microsoft and Google. Initial results suggest that existing C/C++ code can often be ported to CHERI with very few changes, and with promisingly low runtime costs.

The introduction of hardware support for capabilities, in an application-class processor and software stack, raises many compelling questions in programming languages, semantics, and verification - including verification of CHERI hardware; the semantics of the instruction-set architectures; how one can reason about that; the semantics and implementation of CHERI-enabled dialects of C, Rust, WebAssembly, and other languages; the pragmatics of porting code to these and analysis tools that can help; formal and informal reasoning about the security properties they provide; and related capability systems.

This workshop will provide an introduction to the current state of CHERI and Morello, with a combination of invited talks and talks selected from an open call for short abstracts, and stimulate discussion among interested parties. It will not have published proceedings.

Accepted and invited presentations:

• Robert Watson: the state of Morello and CHERI
• Konrad Witaszczyk: the state of Morello software and projects [OR FOLD INTO THE ABOVE?]
• Thomas Bauereiss/Brian Campbell: the Morello ISA semantics, proof, and test generation
• Angus Hammond/Ricardo Almeida: Morello Cerise (WIP)
• Dapeng Gao: Compartmentalisation models
• Elias Storme, Sander Huyghebaert, Steven Keuchel, Thomas Van Strydonck, Dominique Devriese: Secure Calling Conventions for CHERI Capability Machines in Practice (Work in Progress)
• Jeremy Singer: Sealed with a Library Call: Memory Allocators Should Track Capability Seal Operations
• Bastien Rousseau, Jean Pichon-Pharabod, Lars Birkedal: Proving capability safety in the presence of indirect sentries
• Jessica Clarke: Morello software and compilers
• Vadim Zaliva: CHERI C semantics
• Irina Dudina: CHERI static analysis
• Franz Brauße, Kunjian Song, Fedor Shmarov, Rafael Menezes, Mikhail R. Gadelha, Konstantin Korovin, Giles Reger, Lucas C. Cordeiro. ESBMC-CHERI: Towards Verification of C/C++ Programs for CHERI Platforms with ESBMC
• Sarah Harris, Simon Cooksey, Michael Vollmer, Mark Batty. Rust on Morello
• David Chisnall: Capabilities for safe cross-language interoperability
• Matthew Parkinson, Sylvan Clebsch, Tobias Wrigstad, Sophia Drossopoulou, Elias Castegren, Ellen Arvidsson, Luke Cheeseman: Concurrent Mutation must go
• Sophia Drossopolou, Susan Eisenbach, Julian Mackay, and James Noble: Object Capabilities

Schedule permitting, there may also be the opportunity for short (5 minute) talks

Call for Presentations.

Hardware support for capabilities offers the prospect of substantially increased security for the computing infrastructure that we all depend on. Capabilities are an old idea, but in the last 15 years the CHERI project, working closely with Arm and others, has proposed extensions to conventional hardware Instruction-Set Architectures (ISAs) with new architectural features based on hardware capabilities, along with CHERI dialects of C and C++, to enable fine-grained memory protection and highly scalable software compartmentalisation. This is a hardware/software/semantics co-design project, involving architecture design, hardware implementation, system software adaption, and formal semantics and mechanised proof of security properties. Arm and the UKRI Digital Security by Design Challenge (with of the order of £200m government and industry investment from 2019–2024), has developed the industrial prototype Arm Morello CHERI-ARM 64-bit CPU, SoC, and board, to evaluate and demonstrate the mass-market industrial feasibility of CHERI. Several hundred Morello boards have been shipped to various academic and industry projects for evaluation, and millions of lines of conventional C and C++ code have been ported to CHERI; additional explorations of CHERI are underway in Microsoft and Google. Initial results suggest that existing C/C++ code can often be ported to CHERI with very few changes, and with promisingly low runtime costs.

The introduction of hardware support for capabilities, in an application-class processor and software stack, raises many compelling questions in programming languages, semantics, and verification - including verification of CHERI hardware; the semantics of the instruction-set architectures; how one can reason about that; the semantics and implementation of CHERI-enabled dialects of C, Rust, WebAssembly, and other languages; the pragmatics of porting code to these and analysis tools that can help; formal and informal reasoning about the security properties they provide; and related capability systems.

This Principles of Capability Languages (POCL) workshop will provide an introduction to the current state of CHERI and Morello, with a combination of invited talks and talks selected from an open call for short abstracts, and stimulate discussion among interested parties. It will not have published proceedings.

If you would like to propose a talk, please send a plain-text email including the title, authors, and a short abstract (a paragraph or three) to Peter.Sewell@cl.cam.ac.uk by the end of Friday 27 October 2023, AoE. The organising committee will select a programme from these and other invited talks.