Peter Sewell
Professor of Computer Science,
Computer
Laboratory,
University of Cambridge
Member of the Cambridge
Programming, Logic,
and Semantics Group
Fellow of Wolfson college
Fellow of the Royal Society
Here are my contact details,
a
photo,
short bio, and
CV
REMS group (gallery)
Students and Postdocs (list)
Meetings
Funding
Group papers (by date)
Group papers (by topic)
Software
Teaching
Research
My 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.
Our REMS group (Rigorous Engineering for Mainstream Systems) does this, in collaboration with many academic colleagues
in Cambridge and elsewhere, and industry colleagues in Arm, Google, IBM, RISC-V International, and elsewhere.
REMS 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.
Recent REMS Group Papers
-
Morello-Cerise: A Proof of Strong Encapsulation for the Arm
Morello Capability Hardware Architecture.
Angus Hammond, Ricardo Almeida, Thomas Bauereiss, Brian Campbell, Ian
Stark, and Peter Sewell.
In PLDI 2025.
[ bib |
doi |
pdf |
abstract ]
-
Precise exceptions in relaxed architectures.
Ben Simner, Alasdair Armstrong, Thomas Bauereiss, Brian Campbell,
Ohad Kammar, Jean Pichon-Pharabod, and Peter Sewell.
In ISCA 2025, Best paper award.
[ bib |
doi |
pdf |
abstract ]
-
ISO/IEC TS 6010:2025 Programming languages --- C --- A
provenance-aware memory object model for C, ISO/IEC JTC 1/SC
22.
ISO, May 2025.
Based on N3005: A Provenance-aware Memory Object Model for C.
Working Draft Technical Specification ISO/IEC TS 6010:2023 (E). Jens Gustedt,
Peter Sewell, Kayvan Memarian, Victor B. F. Gomes, Martin Uecker.
http://www.open-std.org/jtc1/sc22/wg14/www/docs/n3005.pdf. June 2022.
[ bib |
.html |
abstract ]
-
Comprehensive Formal Verification of Observational Correctness
for the CHERIoT-Ibex Processor, Louis-Emile Ploix, Alasdair
Armstrong, Tom Melham, Ray Lin, Haolong Wang, and Anastasia Courtney,
February 2025.
[ bib |
arXiv |
http |
abstract ]
-
Towards general white-box automation: a typeclass-guided
context cleaner.
Thibaut Pérami.
In CoqPL 2025.
[ bib |
http ]
-
A CHERI C Memory Model for Verified Temporal
Safety.
Vadim Zaliva, Kayvan Memarian, Brian Campbell, Ricardo Almeida,
Nathaniel Wesley Filardo, Ian Stark, and Peter Sewell.
In CPP 2025.
[ bib |
doi |
http ]
-
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 ]
-
Fulminate: Testing CN Separation-Logic Specifications in
C.
Rini Banerjee, Kayvan Memarian, Dhruv Makwana, Christopher Pulte,
Neel Krishnaswami, and Peter Sewell.
In POPL 2025.
[ bib |
doi |
pdf |
abstract ]
-
Formal Mechanised Semantics of CHERI C: Capabilities,
Provenance, and Undefined Behaviour.
Vadim Zaliva, Kayvan Memarian, Ricardo Almeida, Jessica Clarke,
Brooks Davis, Alex Richardson, David Chisnall, Brian Campbell, Ian Stark,
Robert N. M. Watson, and Peter Sewell.
In ASPLOS 2024.
[ bib |
pdf |
abstract ]
-
CHERI: Hardware-Enabled C/C++ Memory Protection at
Scale.
Robert N. M. Watson, David Chisnall, Jessica Clarke, Brooks Davis,
Nathaniel Wesley Filardo, Ben Laurie, Simon W. Moore, Peter G. Neumann,
Alexander Richardson, Peter Sewell, Konrad Witaszczyk, and Jonathan Woodruff.
IEEE Secur. Priv., 22(4):50--61, 2024.
[ bib |
doi |
pdf |
http |
abstract ]
-
An axiomatic basis for computer programming on the relaxed
Arm-A architecture: the AxSL logic.
Angus Hammond1, Zongyuan Liu1, Thibaut Pérami, Peter
Sewell, Lars Birkedal, and Jean Pichon-Pharabod.
In POPL 2024, 1These authors contributed equally. Proc. ACM
Program. Lang. 8, POPL, Article 21.
[ bib |
doi |
pdf |
abstract ]
-
The Arm Morello Evaluation Platform---Validating
CHERI-Based Security in a High-Performance System.
Richard Grisenthwaite, Graeme Barnes, Robert N. M. Watson, Simon W.
Moore, Peter Sewell, and Jonathan Woodruff.
IEEE Micro, 43(3):50--57, 2023.
[ bib |
doi |
pdf |
http |
abstract ]
-
CN: Verifying systems C code with separation-logic
refinement types.
Christopher Pulte, Dhruv C. Makwana, Thomas Sewell, Kayvan Memarian,
Peter Sewell, and Neel Krishnaswami.
In POPL 2023, Proc. ACM Programming Languages 7, POPL, Article 1.
[ bib |
doi |
project page |
pdf |
abstract ]
Blog articles
Research Topics
I also maintain
a page of
Action
Calculi links.
Other
Another photo
[Validate this page.]