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: I work in
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 Semantics, Systems, Security,
and Computer Architecture colleagues in Cambridge, other academics worldwide, and colleagues in Arm, Google, IBM, and elsewhere.
REMS was originally
funded by the eponymous EPSRC
REMS Programme Grant, with Imperial and Edinburgh; it now continues with other funding, including the EU ERC Advanced Grant ELVER: Engineering with Logic and Verification: Mathematically Rigorous Engineering for Safe and Secure
Computer Systems, and donations from Arm and Google.
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--2024, is developing
the industrial prototype Arm Morello CHERI-ARM 64-bit CPU,
SoC, and board, to evaluate and demonstrate the mass-market industrial feasibility of CHERI.
Here are our DSbD
pages.
Recent Papers
-
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 ]
-
An axiomatic basis for computer programming on the relaxed
Arm-A architecture: the AxSL logic.
Angus Hammond*, Zongyuan Liu*, Thibaut Pérami, Peter
Sewell, Lars Birkedal, and Jean Pichon-Pharabod.
In POPL 2024, *These authors contributed equally. Proc. ACM
Program. Lang. 8, POPL, Article 21.
[ bib |
doi |
pdf |
abstract ]
-
Isla: Integrating full-scale ISA semantics and axiomatic
concurrency models (extended version).
Alasdair Armstrong, Brian Campbell, Ben Simner, Christopher Pulte,
and Peter Sewell.
Formal Methods in System Design, May 2023.
[ bib |
doi |
pdf |
http |
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 |
http |
abstract ]
-
Improving Security with Hardware Support: CHERI and Arm's
Morello.
Robert N. M. Watson, Peter Sewell, and William Martin.
The Next Wave (The National Security Agency's review of emerging
technologies), 4(1):10--21, 2023.
ISSN 2640-1789 (print), ISSN 2640-1797 (online).
[ bib |
project page |
pdf |
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.
[ bib |
doi |
project page |
pdf |
abstract ]
-
Multicore Semantics: Making Sense of Relaxed Memory (MPhil
slides), Peter Sewell, Christopher Pulte, Shaked Flur, Mark
Batty, Luc Maranget, and Alasdair Armstrong, October 2022.
[ bib |
.pdf ]
-
Formal CHERI: rigorous engineering and design-time proof of
full-scale architecture security properties, Peter Sewell,
Thomas Bauereiss, Brian Campbell, and Robert N. M. Watson.
Blog post,
https://www.lightbluetouchpaper.org/2022/07/22/formal-cheri/, July
2022.
[ bib |
project page |
http ]
-
Islaris: Verification of Machine Code Against Authoritative
ISA Semantics.
Michael Sammler, Angus Hammond, Rodolphe Lepigre, Brian Campbell,
Jean Pichon-Pharabod, Derek Dreyer, Deepak Garg, and Peter Sewell.
In PLDI 2022.
[ bib |
doi |
project page |
pdf |
abstract ]
-
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, and Martin
Uecker.
ISO/IEC JTC1/SC22/WG14 N3005
http://www.open-std.org/jtc1/sc22/wg14/www/docs/n3005.pdf, June 2022.
[ bib |
pdf |
abstract ]
-
Verified Security for the Morello Capability-enhanced
Prototype Arm Architecture.
Thomas Bauereiss, Brian Campbell, Thomas Sewell, Alasdair Armstrong,
Lawrence Esswood, Ian Stark, Graeme Barnes, Robert N. M. Watson, and Peter
Sewell.
In ESOP 2022.
[ bib |
doi |
project page |
pdf |
http |
abstract ]
-
Relaxed virtual memory in Armv8-A.
Ben Simner, Alasdair Armstrong, Jean Pichon-Pharabod, Christopher
Pulte, Richard Grisenthwaite, and Peter Sewell.
In ESOP 2022.
[ bib |
doi |
project page |
pdf |
http |
abstract ]
-
Relaxed virtual memory in Armv8-A (extended
version), Ben Simner, Alasdair Armstrong, Jean
Pichon-Pharabod, Christopher Pulte, Richard Grisenthwaite, and Peter Sewell,
March 2022.
http://arxiv.org/abs/2203.00642.
[ bib |
project page |
pdf |
abstract ]
-
VIP: Verifying Real-World C Idioms with Integer-Pointer
Casts.
Rodolphe Lepigre, Michael Sammler, Kayvan Memarian, Robbert Krebbers,
Derek Dreyer, and Peter Sewell.
In POPL 2022, Proc. ACM Program. Lang. 6, POPL, Article 20.
[ bib |
doi |
supplementary material |
project page |
pdf |
abstract ]
-
Bad Reasons to Reject Good Papers, and vice
versa, Peter Sewell.
SIGPLAN PL Perspectives Blog, December 2021.
Also published 2022-12-07 on the Communications of the ACM Blog
https://cacm.acm.org/blogs/blog-cacm/267440-bad-reasons-to-reject-good-papers-and-vice-versa/fulltext.
[ bib |
http ]
-
Isla: Integrating full-scale ISA semantics and axiomatic
concurrency models.
Alasdair Armstrong, Brian Campbell, Ben Simner, Christopher Pulte,
and Peter Sewell.
In CAV 2021.
[ bib |
doi |
pdf |
http |
abstract ]
-
Capability Hardware Enhanced RISC Instructions: CHERI
Instruction-Set Architecture (Version 8).
Robert N. M. Watson, Peter G. Neumann, Jonathan Woodruff, Michael
Roe, Hesham Almatary, Jonathan Anderson, John Baldwin, Graeme Barnes, David
Chisnall, Jessica Clarke, Brooks Davis, Lee Eisen, Nathaniel Wesley Filardo,
Richard Grisenthwaite, Alexandre Joannou, Ben Laurie, A. Theodore Markettos,
Simon W. Moore, Steven J. Murdoch, Kyndylan Nienhuis, Robert Norton,
Alexander Richardson, Peter Rugg, Peter Sewell, Stacey Son, and Hongyan Xia.
Technical Report UCAM-CL-TR-951, University of Cambridge, Computer
Laboratory, October 2020.
[ bib |
doi |
project page |
pdf |
abstract ]
-
CHERI C/C++ Programming Guide.
Robert N. M. Watson, Alexander Richardson, Brooks Davis, John
Baldwin, David Chisnall, Jessica Clarke, Nathaniel Filardo, Simon W. Moore,
Edward Napierala, Peter Sewell, and Peter G. Neumann.
Technical Report UCAM-CL-TR-947, University of Cambridge, Computer
Laboratory, June 2020.
[ bib |
project page |
pdf |
abstract ]
-
Cornucopia: Temporal Safety for CHERI Heaps.
Nathaniel Wesley Filardo, Brett F. Gutstein, Jonathan Woodruff, Sam
Ainsworth, Lucian Paul-Trifu, Brooks Davis, Hongyan Xia, Edward Tomasz
Napierala, Alexander Richardson, John Baldwin, David Chisnall, Jessica
Clarke, Khilan Gudka, Alexandre Joannou, A. Theodore Markettos, Alfredo
Mazzinghi, Robert M. Norton, Michael Roe, Peter Sewell, Stacey Son,
Timothy M. Jones, Simon W. Moore, Peter G. Neumann, and Robert N. M. Watson.
In Security and Privacy 2020.
[ bib |
doi |
project page |
pdf |
abstract ]
-
Rigorous engineering for hardware security: Formal modelling
and proof in the CHERI design and implementation process.
Kyndylan Nienhuis, Alexandre Joannou, Thomas Bauereiss, Anthony Fox,
Michael Roe, Brian Campbell, Matthew Naylor, Robert M. Norton, Simon W.
Moore, Peter G. Neumann, Ian Stark, Robert N. M. Watson, and Peter Sewell.
In Security and Privacy 2020.
[ bib |
doi |
project page |
pdf |
abstract ]
-
ARMv8-A system semantics: instruction fetch in relaxed
architectures.
Ben Simner, Shaked Flur, Christopher Pulte, Alasdair Armstrong, Jean
Pichon-Pharabod, Luc Maranget, and Peter Sewell.
In ESOP 2020.
[ bib |
project page |
errata |
pdf |
abstract ]
-
An Introduction to CHERI.
Robert N. M. Watson, Simon W. Moore, Peter Sewell, and Peter Neumann.
Technical Report UCAM-CL-TR-941, University of Cambridge, Computer
Laboratory, September 2019.
[ bib |
project page |
pdf |
abstract ]
Research Topics
I also maintain
a page of
Action
Calculi links.
Other
Another photo
[Validate this page.]