-
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 ]
-
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 ]
-
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 ]
-
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 ]
-
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 ]
-
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 ]
-
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 ]
-
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.
Technical Report UCAM-CL-TR-959, University of Cambridge, Computer
Laboratory, September 2021.
[ bib |
project page |
pdf |
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 ]
-
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 ]
-
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 ]
-
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 ]
-
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 ]
-
Proving security properties of CHERI-MIPS.
Kyndylan Nienhuis, Alexandre Joannou, and Peter Sewell.
In Automated Reasoning Workshop (ARW) 2018, Two-page abstract.
[ bib |
pdf |
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 ]