Peter Sewell
Professor of Computer Science,
Computer
Laboratory,
University of Cambridge
Member of the Cambridge
Programming, Logic,
and Semantics Group
Fellow of Wolfson college
Here are my contact details,
a
photo,
short bio, and
CV
PhD students, RAs, and Co-authors
Meetings
Funding
Papers (by date)
Papers (by topic)
Open positions
We are looking for postdoctoral researchers and postgraduate research
engineers to help develop semantics and verification to
improve the foundations and security of mainstream computer systems,
for CHERI verification and Arm system software verification.
Closing date 13 January 2021 - see the advert.
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
architectural description, programming languages, networking, and security,
developing and using techniques from
semantics, type systems, automated reasoning, and concurrency theory.
This work currently forms part of the REMS: Rigorous
Engineering for Mainstream Systems project, funded by the
eponymous EPSRC
Programme Grant, in collaboration with Systems, Security,
Architecture, and Semantics researchers from Cambridge, Imperial,
and Edinburgh, and with colleagues in ARM, IBM, and elsewhere,
and by the EU ERC Advanced Grant ELVER.
REMS is exploring how we can use rigorous mathematics to improve engineering practice for mainstream computer systems, to make them more robust and secure.
The REMS pages give the associated people, papers,
models, and tools.
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.
In 2019, UKRI announced the Digital Security by
Design Challenge, with £70m government and £117m industry funding,
including an industrial prototype Arm Morello CHERI-ARM 64-bit CPU,
SoC, and board. This aims to evaluate and demonstrate the mass-market
industrial
feasibility of CHERI.
Here are our DSbD
page,
blog,
and
CL
news article;
an
Arm blog
post on Morello, a UK
Government press
release, and an article
at The Register.
Recent Papers
-
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 |
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 (extended version).
Ben Simner, Shaked Flur, Christopher Pulte, Alasdair Armstrong, Jean
Pichon-Pharabod, Luc Maranget, and Peter Sewell.
In ESOP 2020.
[ bib |
project page |
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 ]
-
Rigorous engineering for hardware security: Formal modelling
and proof in the CHERI design and implementation process.
Kyndylan Nienhuis, Alexandre Joannou, Anthony Fox, Michael Roe,
Thomas Bauereiss, Brian Campbell, Matthew Naylor, Robert M. Norton, Simon W.
Moore, Peter G. Neumann, Ian Stark, Robert N. M. Watson, and Peter Sewell.
Technical Report UCAM-CL-TR-940, University of Cambridge, Computer
Laboratory, September 2019.
[ bib |
pdf |
abstract ]
-
Cerberus-BMC: a Principled Reference Semantics and
Exploration Tool for Concurrent and Sequential C.
Stella Lau, Victor B. F. Gomes, Kayvan Memarian, Jean
Pichon-Pharabod, and Peter Sewell.
In CAV 2019.
[ bib |
DOI |
project page |
pdf |
abstract ]
-
Capability Hardware Enhanced RISC Instructions: CHERI
Instruction-Set Architecture (Version 7).
Robert N. M. Watson, Peter G. Neumann, Jonathan Woodruff, Michael
Roe, Hesham Almatary, Jonathan Anderson, John Baldwin, David Chisnall, Brooks
Davis, Nathaniel Wesley Filardo, Alexandre Joannou, Ben Laurie, A. Theodore
Markettos, Simon W. Moore, Steven J. Murdoch, Kyndylan Nienhuis, Robert
Norton, Alex Richardson, Peter Rugg, Peter Sewell, Stacey Son, and Hongyan
Xia.
Technical Report UCAM-CL-TR-927, University of Cambridge, Computer
Laboratory, June 2019.
496pp.
[ bib |
pdf |
abstract ]
-
CheriABI: Enforcing Valid Pointer Provenance and Minimizing
Pointer Privilege in the POSIX C Run-time Environment.
Brooks Davis, Robert N. M. Watson, Alexander Richardson, Peter G.
Neumann, Simon W. Moore, John Baldwin, David Chisnall, James Clarke,
Nathaniel Wesley Filardo, Khilan Gudka, Alexandre Joannou, Ben Laurie,
A. Theodore Markettos, J. Edward Maste, Alfredo Mazzinghi, Edward Tomasz
Napierala, Robert M. Norton, Michael Roe, Peter Sewell, Stacey Son, and
Jonathan Woodruff.
In ASPLOS 2019, Best paper award.
[ bib |
DOI |
project page |
pdf |
http |
abstract ]
-
REMS: Rigorous Engineering for Mainstream Systems. Summary
2013-03 -- 2019-01, Peter Sewell, February 2019.
[ bib |
pdf |
abstract ]
-
ISA Semantics for ARMv8-A, RISC-V, and
CHERI-MIPS.
Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Alastair Reid,
Kathryn E. Gray, Robert M. Norton, Prashanth Mundkur, Mark Wassell, Jon
French, Christopher Pulte, Shaked Flur, Ian Stark, Neel Krishnaswami, and
Peter Sewell.
In POPL 2019, Proc. ACM Program. Lang. 3, POPL, Article 71.
[ bib |
DOI |
supplementary material |
project page |
pdf |
abstract ]
-
Exploring C Semantics and Pointer Provenance.
Kayvan Memarian, Victor B. F. Gomes, Brooks Davis, Stephen Kell,
Alexander Richardson, Robert N. M. Watson, and Peter Sewell.
In POPL 2019, Proc. ACM Program. Lang. 3, POPL, Article 67. Also
available as ISO/IEC JTC1/SC22/WG14 N2311.
[ bib |
DOI |
supplementary material |
project page |
pdf |
abstract ]
-
The RISC-V Instruction Set Manual Volume I: Unprivileged
ISA.
Andrew Waterman and Krste Asanović, editors.
December 2018.
Document Version 20181221-Public-Review-draft. Contributors: Arvind,
Krste Asanović, Rimas Avižienis, Jacob Bachmeyer, Christopher F.
Batten, Allen J. Baum, Alex Bradbury, Scott Beamer, Preston Briggs,
Christopher Celio, Chuanhua Chang, David Chisnall, Paul Clayton, Palmer
Dabbelt, Roger Espasa, Shaked Flur, Stefan Freudenberger, Jan Gray, Michael
Hamburg, John Hauser, David Horner, Bruce Hoult, Alexandre Joannou, Olof
Johansson, Ben Keller, Yunsup Lee, Paul Loewenstein, Daniel Lustig, Yatin
Manerkar, Luc Maranget, Margaret Martonosi, Joseph Myers, Vijayanand
Nagarajan, Rishiyur Nikhil, Jonas Oberhauser, Stefan O'Rear, Albert Ou, John
Ousterhout, David Patterson, Christopher Pulte, Jose Renau, Colin Schmidt,
Peter Sewell, Susmit Sarkar, Michael Taylor, Wesley Terpstra, Matt Thomas,
Tommy Thorn, Caroline Trippel, Ray VanDeWalker, Muralidaran Vijayaraghavan,
Megan Wachs, Andrew Waterman, Robert Watson, Derek Williams, Andrew Wright,
Reinoud Zandijk, and Sizhuo Zhang.
[ bib |
pdf ]
-
Engineering with Logic: Rigorous Test-Oracle Specification and
Validation for TCP/IP and the Sockets API.
Steve Bishop, Matthew Fairbairn, Hannes Mehnert, Michael Norrish, Tom
Ridge, Peter Sewell, Michael Smith, and Keith Wansbrough.
J. ACM, 66(1):1:1--1:77, December 2018.
[ bib |
DOI |
project page |
pdf |
http |
abstract ]
-
Simplifying ARM Concurrency: Multicopy-atomic Axiomatic and
Operational Models for ARMv8.
Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit
Sarkar, and Peter Sewell.
In POPL 2018.
[ bib |
DOI |
project page |
errata |
pdf |
abstract ]
-
Mixed-size Concurrency: ARM, POWER, C/C++11, and
SC.
Shaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis, Luc
Maranget, Kathryn E. Gray, Ali Sezgin, Mark Batty, and Peter Sewell.
In POPL 2017.
[ bib |
DOI |
project page |
pdf |
abstract ]
-
An operational semantics for C/C++11
concurrency.
Kyndylan Nienhuis, Kayvan Memarian, and Peter Sewell.
In OOPSLA 2016.
[ bib |
DOI |
pdf |
http |
abstract ]
-
The missing link: explaining ELF static linking,
semantically.
Stephen Kell, Dominic P. Mulligan, and Peter Sewell.
In OOPSLA 2016.
[ bib |
DOI |
project page |
pdf |
http |
abstract ]
-
Into the depths of C: elaborating the de facto
standards.
Kayvan Memarian, Justus Matthiesen, James Lingard, Kyndylan Nienhuis,
David Chisnall, Robert N.M. Watson, and Peter Sewell.
In PLDI 2016, PLDI 2016 Distinguished Paper award.
[ bib |
DOI |
project page |
pdf |
http |
abstract ]
Research Topics
I also maintain
a page of
Action
Calculi links.
Other
Another photo
[Validate this page.]