Our REMS group research aims to put the engineering of real-world computer
systems on better foundations, developing techniques (both
mathematically rigorous and pragmatically useful)
to make systems that are better-understood, more robust, and
more secure.
This applied semantics needs tightly integrated theoretical and practical
research, spanning a range of Computer Science:
architecture specification, programming languages, verification, security, and networking;
developing and using techniques from semantics, type systems, automated reasoning, and concurrency theory.
We currently focus on
hardware-architecture instruction semantics, especially for Arm and RISC-V, using Sail;
relaxed-memory concurrency for Arm, RISC-V, Power, x86, C/C++, Javascript, and Wasm;
C semantics with Cerberus;
verification and testing of C systems code with CN;
CHERI: Capability enhanced systems;
and critical systems code such as the Android pKVM hypervisor.
For all these, we're concerned with how one can specify the intended abstractions, and how one can use such specifications in design, documentation, testing, and proof.
This is in collaboration with many academic colleagues
in Cambridge, Edinburgh, Aarhus, and elsewhere, and industry colleagues in Arm, Google, IBM, RISC-V International, and elsewhere.
REMS (Rigorous Engineering for Mainstream Systems) was originally funded by the eponymous EPSRC
REMS Programme Grant, with Imperial and Edinburgh; it continues with other funding, including the EU ERC AdG ELVER (2018-2024), the ERC/UKRI Frontier Guarantee AdG SAFER (2024-2029), and donations from Arm, Google, Intel, and Amazon.
The CHERI
project, led by
Robert Watson,
Simon Moore,
and myself at Cambridge,
and Peter Neumann
at SRI International,
extends conventional hardware Instruction-Set Architectures (ISAs)
with new architectural features to enable fine-grained memory
protection and highly scalable software compartmentalization.
It 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.
The UKRI Digital Security by
Design Challenge, with £70m government and £117m industry funding from 2019-2025, developed
the industrial prototype Arm Morello CHERI-ARM 64-bit CPU,
SoC, board, and software stack, to evaluate and demonstrate the mass-market industrial feasibility of CHERI.
Here are our DSbD
pages.
It Is Time to Standardize Principles and Practices for Software
Memory Safety.
Robert N.M. Watson, John Baldwin, David Chisnall, Tony Chen, Jessica
Clarke, Brooks Davis, Nathaniel Filardo, Brett Gutstein, Graeme Jenkinson,
Ben Laurie, Alfredo Mazzinghi, Simon Moore, Peter G. Neumann, Hamed Okhravi,
Alex Richardson, Alex Rebert, Peter Sewell, Laurence Tratt, Murali
Vijayaraghavan, Hugo Vincent, and Konrad Witaszczyk.
Communications of the ACM, 68(2):40–45, January 2025.
[ bib |
doi |
http |
abstract ]
On long-term research vision, Peter Sewell,
January 2026.
Talk at RTFM 2026 faculty mentoring workshop (Read the Faculty
Manual) with POPL 2026, Rennes, 2026-01-13.
[ bib |
pdf ]
This is in collaboration with many academic colleagues
in Cambridge, Edinburgh, Aarhus, and elsewhere, and industry colleagues in Arm, Google, IBM, RISC-V International, and elsewhere.
REMS (Rigorous Engineering for Mainstream Systems) was originally funded by the eponymous EPSRC
REMS Programme Grant, with Imperial and Edinburgh; it continues with other funding, including the EU ERC AdG ELVER (2018-2024), the ERC/UKRI Frontier Guarantee AdG SAFER (2024-2029), and donations from Arm, Google, Intel, and Amazon.
