It is time to standardize principles and practices for
software memory safety (extended version).
Robert N. M. Watson, John Baldwin, Tony Chen, David Chisnall, Jessica
Clarke, Brooks Davis, Nathaniel Wesley Filardo, Brett Gutstein, Graeme
Jenkinson, Christoph Kern, Ben Laurie, Alfredo Mazzinghi, Simon W. Moore,
Peter G. Neumann, Hamed Okhravi, Alex Rebert, Alex Richardson, Peter Sewell,
Laurence Tratt, Murali Vijayaraghavan, Hugo Vincent, and Konrad Witaszczyk.
Technical Report UCAM-CL-TR-996, University of Cambridge, Computer
Laboratory, February 2025.
[ bib |
doi |
.pdf ]
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 ]
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 ]
The Cerberus C semantics.
Kayvan Memarian.
Technical Report UCAM-CL-TR-981, University of Cambridge, Computer
Laboratory, May 2023.
PhD thesis.
[ bib |
doi |
.pdf |
abstract ]
MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe
Code.
Alexandra E. Michael, Anitha Gollamudi, Jay Bosamiya, Evan Johnson,
Aidan Denlinger, Craig Disselkoen, Conrad Watt, Bryan Parno, Marco
Patrignani, Marco Vassena, and Deian Stefan.
Proc. ACM Program. Lang., 7(POPL):425--454, January 2023.
[ 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 ]
The RISC-V Instruction Set Manual Volume I: Unprivileged
ISA.
Andrew Waterman and Krste Asanović, editors.
December 2019.
Document Version 20191213. 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, Ken
Dockser, Roger Espasa, Shaked Flur, Stefan Freudenberger, Marc Gauthier, Andy
Glew, Jan Gray, Michael Hamburg, John Hauser, David Horner, Bruce Hoult, Bill
Huffman, Alexandre Joannou, Olof Johansson, Ben Keller, David Kruckemyer,
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, Josh Scheid, 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 ]
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 ]
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 ]
P1726R0: Pointer lifetime-end zap, Paul E.
McKenney, Maged Michael, Jens Mauer, Peter Sewell, Martin Uecker, Hans Boehm,
Hubert Tong, and Niall Douglas.
ISO/IEC JTC1/SC22/WG21 P1726R0, June 2019.
[ bib |
pdf ]
Weakening WebAssembly.
Conrad Watt, Andreas Rossberg, and Jean Pichon-Pharabod.
Proc. ACM Program. Lang., 3(OOPSLA):133:1--133:28, 2019.
[ bib |
doi |
http ]
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.
Technical Report UCAM-CL-TR-932, University of Cambridge, Computer
Laboratory, January 2019.
[ bib |
project page |
pdf |
abstract ]
Through computer architecture, darkly.
A. Theodore Markettos, Robert N. M. Watson, Simon W. Moore, Peter
Sewell, and Peter G. Neumann.
Commun. ACM, 62(6):25--27, 2019.
[ bib |
doi |
http ]
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 ]
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 ]
Not-quite-so-broken TLS: lessons in re-engineering a security
protocol specification and implementation, David Kaloper
Meršinjak, Hannes Mehnert, Anil Madhavapeddy, and Peter Sewell, May
2015.
Presentation at HCSS 2015: the Fifteenth Annual High Confidence
Software and Systems Conference.
[ bib |
project page |
abstract ]
Cerberus: towards an Executable Semantics for Sequential and
Concurrent C11, Kayvan Memarian, Kyndylan Nienhuis, Justus
Matthiesen, James Lingard, and Peter Sewell, May 2015.
Presentation at HCSS 2015: the Fifteenth Annual High Confidence
Software and Systems Conference.
[ bib |
project page |
abstract ]
Rigorous Architectural Modelling for Production
Multiprocessors, S. Flur, K. Gray, G. Kerneis, D. Mulligan,
C. Pulte, S. Sarkar, and P. Sewell, May 2015.
Presentation at HCSS 2015: the Fifteenth Annual High Confidence
Software and Systems Conference.
[ bib |
abstract ]
The C11 and C++11 Concurrency Model.
Mark John Batty.
PhD thesis, University of Cambridge, 2014.
2015 SIGPLAN John C. Reynolds Doctoral Dissertation award and 2015
CPHC/BCS Distinguished Dissertation Competition winner.
[ bib |
pdf |
abstract ]
Principles of POPL.
Derek Dreyer, John Field, Roberto Giacobazzi, Michael Hicks, Suresh
Jagannathan, Mooly Sagiv, Peter Sewell, and Phil Wadler.
SIGPLAN Notices, 48(4S):12--16, July 2013.
[ bib |
doi ]
Responses to FoC Questions, Peter O'Hearn,
February 2011.
Briefing note for EPSRC ICT team, with contributions and input from
Anuj Dawar, Philippa Gardner, Chris Hankin, Tom Melham, Faron Moller, Andrew
Pitts, Uday Reddy, Peter Sewell, and Philip Wadler. 11pp.
[ bib ]
Fundamentals of Computing Research: a perspective from the
ground, Peter Sewell, February 2011.
Briefing note for EPSRC ICT team, with input from Anuj Dawar, Chris
Hankin, Tom Melham, Faron Moller, Peter O'Hearn, and Phil Wadler. 6pp.
[ bib ]
Robin Milner 1934--2010: verification, languages, and
concurrency.
Andrew D. Gordon, Robert Harper, John Harrison, Alan Jeffrey, and
Peter Sewell.
In POPL 2011.
[ bib |
doi ]
N3196: Omnibus Memory Model and Atomics Paper,
P. McKenney, M. Batty, C. Nelson, H. Boehm, A. Williams, S. Owens, S. Sarkar,
P. Sewell, T. Weber, M.Wong, L. Crowl, and B. Kosnik.
ISO JTC1/SC22/WG21 -- The C++ Standards Committee. Working Paper,
November 2010.
[ bib ]
N3125: Omnibus Memory Model and Atomics Paper,
P. McKenney, M. Batty, C. Nelson, H. Boehm, A. Williams, S. Owens, S. Sarkar,
P. Sewell, T. Weber, M.Wong, and L. Crowl.
ISO JTC1/SC22/WG21 - The C++ Standards Committee. Working Paper,
August 2010.
[ bib ]
N3132: Mathematizing C++ Concurrency: The Post-Rapperswil
Model, M. Batty, S. Owens, S. Sarkar, P. Sewell, and
T. Weber.
ISO JTC1/SC22/WG21 - The C++ Standards Committee. Working Paper,
August 2010.
[ bib ]
Ott: Effective Tool Support for the Working
Semanticist.
Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine,
Thomas Ridge, Susmit Sarkar, and Rok Strniša.
Journal of Functional Programming, 20(1):70--122, January 2010.
Invited submission from ICFP 2007, which was awarded the ACM SIGPLAN
Most Influential ICFP 2007 Paper, in 2017.
[ bib |
doi |
project page |
pdf |
abstract ]
An approximation to the real TCP state diagram,
Steven Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael
Smith, and Keith Wansbrough, March 2005.
This is a poster with a version of the "TCP state diagram" extracted
from the specification. It is rather more complete than the usual diagram,
but is still a very abstract and simplified view of the state space of our
specification. It is intended to be printed at A1 size or bigger.
[ bib |
project page |
ps |
pdf ]
Acute release, Peter Sewell, James J. Leifer,
Keith Wansbrough, Mair Allen-Williams, Francesco Zappa Nardelli, Pierre
Habouzit, and Viktor Vafeiadis, January 2005.
[ bib |
project page |
http ]
Acute and TCP: specifying and developing abstractions for
global computation.
James Leifer, Michael Norrish, Peter Sewell, and Keith Wansbrough.
In APPSEM II Workshop, 2004, 2pp.
[ bib ]
Global abstraction-safe marshalling with hash
types.
James Leifer, Gilles Peskine, Peter Sewell, and Keith Wansbrough.
Technical Report UCAM-CL-TR-569, University of Cambridge Computer
Laboratory, June 2003.
Also published as INRIA Rocquencourt report RR-4851. 86pp.
[ bib |
ps |
pdf |
.html |
abstract ]
A Brief Introduction to Applied π, Peter
Sewell, January 1999.
Lecture notes for the Mathfit Instructional Meeting on Recent
Advances in Semantics and Types for Concurrency: Theory and Practice, July
1998.
[ bib |
.html ]
The Ott tool for writing definitions of programming languages
and calculi, Peter Sewell, Francesco Zappa Nardelli, Scott
Owens, Joey Eremondi, Hannes Mehnert, Karl Palmskog, Thibaut Perami, Matthew
Parkinson, Hannes Mehnert, kit-ty kate, Brian Campbell, Francois Pottier,
Gilles Peskine, Alastair Reid, Tom Ridge, Susmit Sarkar, Rok Strniša,
and Viktor Vafeiadis, 2005--2024.
[ bib |
project page |
github ]
Lem, a tool for lightweight executable
mathematics, Dominic Mulligan, Thomas Bauereiss, Kathryn E.
Gray, Scott Owens, Peter Sewell, Thomas Tuerk, Basile Clement, Brian
Campbell, Christopher Pulte, David Sheets, Fabian Immler, Frederic Loulergue,
Francesco Zappa Nardelli, Gabriel Kerneis, James Lingard, Jean
Pichon-Pharabod, Justus Matthiesen, Kayvan Memarian, Kyndylan Nienhuis, Lars
Hupel, Mark Batty, Michael Greenberg, Michael Norrish, Ohad Kammar, Peter
Boehm, Robert Norton, Sami Mäkelä, Shaked Flur, Stephen Kell, Thibaut
Pérami, Thomas Bauereiss, Thomas Williams, Victor Gomes, and emersion,
2010--2023.
[ bib |
project page |
github ]
CN C verification and testing tool, Christopher
Pulte, Dhruv C. Makwana, Thomas Sewell, Kayvan Memarian, Rini Banerjee, Peter
Sewell, and Neel Krishnaswami, 2023--.
[ bib |
github ]
Sail CHERI-RISC-V instruction-set architecture (ISA)
model, Alasdair Armstrong, Thomas Bauereiss, Brian Campbell,
Jessica Clarke, Nathaniel Wesley Filardo, Google, Alexandre Joannou,
Microsoft, Prashanth Mundkur, Robert Norton-Wright, Alexander Richardson,
Peter Rugg, and Peter Sewell, 2019--2024.
[ bib |
project page |
github ]
Sail CHERI-MIPS instruction-set architecture (ISA)
model, Alasdair Armstrong, Thomas Bauereiss, Brian Campbell,
Jessica Clarke, Nathaniel Filardo, Shaked Flur, Jon French, Kathryn E. Gray,
Alexandre Joannou, Robert Norton-Wright, Christopher Pulte, Alexander
Richardson, and Peter Sewell, 2016--2021.
[ bib |
project page |
github ]
Sail RISC-V instruction-set architecture (ISA)
model, ahadali5000, Alasdair Armstrong, Alexander Richardson,
Aril Computer Corp. (for contributions by Scott Johnson), Ben Marshall,
Bicheng Yang, Bilal Sakhawat, Brian Campbell, Chris Casinghino, Christopher
Pulte, Martin Berger Codasip (for contributions by Tim Hutt, Ben Fletcher),
dylux, eroom1966, Google LLC (for contributions by its employees), Hesham
Almatary, Jan Henrik Weinstock, Jessica Clarke, Jon French, Martin Berger,
Michael Sammler, Microsoft (for contributions by Robert Norton-Wright,
Nathaniel Wesley Filardo), Muhammad Bilal Sakhawat, Nathaniel Wesley Filardo,
Paul A. Clarke, Peter Rugg, Peter Sewell, Philipp Tomsich, Prashanth Mundkur,
Rafael Sene, Rishiyur S. Nikhil (Bluespec, Inc.), Robert Norton-Wright,
Shaked Flur, Thibaut Pérami, Thomas Bauereiss, VRULL GmbH (for contributions
by its employees), William McSpaddden, and Xinlai Wan, 2014--2024.
[ bib |
project page |
github ]
The Sail Instruction-Set Architecture (ISA) specification
language, Alasdair Armstrong, Thomas Bauereiss, Brian
Campbell, Shaked Flur, Jon French, Kathryn E. Gray, Stephen Kell, Gabriel
Kerneis, Neel Krishnaswami, Prashanth Mundkur, Robert Norton-Wright,
Christopher Pulte, Alastair Reid, Peter Sewell, Ian Stark, and Mark Wassell,
2013--2024.
[ bib |
project page |
github ]
P1796R0: Effective Types: Examples, Peter
Sewell, Kayvan Memarian, Victor B. F. Gomes, Jens Gustedt, and Hubert Tong.
ISO/IEC JTC1/SC22/WG21 P1796R0.
[ bib |
pdf ]