-
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.
[ 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 ]
-
Relaxed exception semantics for Arm-A (extended
version), Ben Simner, Alasdair Armstrong, Thomas Bauereiss,
Brian Campbell, Ohad Kammar, Jean Pichon-Pharabod, and Peter Sewell, 2024.
[ bib |
arXiv |
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 ]
-
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, Proc. ACM Programming Languages 7, POPL, Article 1.
[ 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 ]
-
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 ]