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.

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

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.