recent.bib
@comment{{This file has been generated by bib2bib 1.99}}
@comment{{Command line: bibtex2html-1.99-with-magiclink/bib2bib -c recent:"true" -ob recent.bib sewellandgroupbib2.bib}}
@inproceedings{2023-popl-cn,
author = {Christopher Pulte and Dhruv C. Makwana and Thomas Sewell and Kayvan Memarian and Peter Sewell and Neel Krishnaswami},
title = {{CN}: Verifying systems {C} code with separation-logic refinement types},
optcrossref = {},
optkey = {},
conf = {POPL 2023},
booktitle = {Proceedings of the 50th ACM SIGPLAN Symposium on Principles of Programming Languages},
optbooktitle = {},
year = {2023},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optpages = {},
month = jan,
optaddress = {},
optorganization = {},
optpublisher = {},
optnote = {Conditionally accepted},
note = {Proc. ACM Programming Languages 7, POPL, Article 1},
optnote = {},
optannote = {},
doi = {10.1145/3571194},
abstract = {Despite significant progress in the verification of hypervisors, operating systems, and compilers, and in verification tooling, there exists a wide gap between the approaches used in verification projects and conventional development of systems software. We see two main challenges in bringing these closer together: verification handling the complexity of code and semantics of conventional systems software, and verification usability.
We describe an experiment in verification tool design aimed at addressing some aspects of both: we design and implement CN, a separation-logic refinement type system for C systems software, aimed at predictable proof automation, based on a realistic semantics of ISO C. CN reduces refinement typing to decidable propositional logic reasoning, uses first-class resources to support pointer aliasing and pointer arithmetic, features resource inference for iterated separating conjunction, and uses a novel syntactic restriction of ghost variables in specifications to guarantee their successful inference. We implement CN and formalise key aspects of the type system, including a soundness proof of type checking. To demonstrate the usability of CN we use it to verify a substantial component of Google's pKVM hypervisor for Android.
},
optapollourl = {https://www.repository.cam.ac.uk/handle/1810/288588},
pdf = {http://www.cl.cam.ac.uk/users/pes20/cn-draft.pdf},
optsupplementarymaterial = {https://doi.org/10.5281/zenodo.5662349},
topic = {CN},
opttopictwo = {Cerberus},
project = {https://www.cl.cam.ac.uk/~cp526/popl23.html},
elver = {true},
recent = {true},
pkvm = {true}
}
@article{10123148,
author = {Grisenthwaite, Richard and Barnes, Graeme and Watson, Robert N. M. and Moore, Simon W. and Sewell, Peter and Woodruff, Jonathan},
journal = {IEEE Micro},
title = {The {Arm Morello} Evaluation Platform---Validating {CHERI}-Based Security in a High-Performance System},
year = {2023},
volume = {43},
number = {3},
pages = {50--57},
doi = {10.1109/MM.2023.3264676},
url = {https://ieeexplore.ieee.org/document/10123148},
pdf = {https://www.repository.cam.ac.uk/bitstreams/c26b2575-71fc-4ed4-bd10-4a38114531bd/download},
opturl = {https://www.repository.cam.ac.uk/items/5ce6229c-d21b-4f61-adae-483026648e84},
abstract = {Memory safety issues are a persistent source of security vulnerabilities, with conventional architectures and the C/C++ codebase chronically prone to exploitable errors. The Capability Hardware Enhanced RISC Instructions (CHERI) research project has explored a novel architectural approach to ameliorate such issues using unforgeable hardware capabilities to implement pointers. Morello is an Arm experimental platform for evaluation of CHERI in the Arm architecture context to explore its potential for mass-market adoption. This article describes the Morello Evaluation Platform, covering the motivation and functionality of the Morello architectural hardware extensions; their potential for fine-grained memory safety and software compartmentalization; formally proven security properties; impact on the microarchitecture of the high-performance, out-of-order multiprocessor Arm Morello processor; and the software-enablement program by Arm, the University of Cambridge, and Linaro. Together, this allows a wide range of researchers in both industry and academia to explore and assess the Morello platform.
},
topic = {cheri},
cheriformal = {true},
elver = {true},
recent = {true}
}
@inproceedings{cheri-c-asplos,
author = {Vadim Zaliva and Kayvan Memarian and Ricardo Almeida and Jessica Clarke and Brooks Davis and Alex Richardson and David Chisnall and Brian Campbell and Ian Stark and Robert N. M. Watson and Peter Sewell},
title = {Formal Mechanised Semantics of {CHERI C}: Capabilities, Provenance, and Undefined Behaviour},
conf = {ASPLOS 2024},
optcrossref = {},
optkey = {},
booktitle = {Proc. ACM International Conference on Architectural Support for Programming Languages and Operating Systems},
year = {2024},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optpages = {},
month = apr,
optaddress = {},
optorganization = {},
optpublisher = {},
optnote = {Accepted for publication, subject to shepherd approval},
optannote = {},
abstract = {Memory safety issues are a persistent source of security vulnerabilities, with conventional architectures and the C codebase chronically prone to exploitable errors. The CHERI research project has shown how one can provide radically improved security for that existing codebase with minimal modification, using unforgeable hardware capabilities in place of machine-word pointers in CHERI dialects of C, implemented as adaptions of Clang/LLVM and GCC. CHERI was first prototyped as extensions of MIPS and RISC-V; it is currently being evaluated by Arm and others with the Arm Morello experimental architecture, processor, and platform, to explore its potential for mass-market adoption, and by Microsoft in their CHERIoT design for embedded cores.
There is thus considerable practical experience with CHERI C implementation and use, but exactly what CHERI C's semantics is (or should be) remains an open question. In this paper, we present the first attempt to rigorously and comprehensively define CHERI C semantics, discuss key semantics design questions relating to capabilities, provenance, and undefined behaviour, and clarify them with semantics in multiple complementary forms: in prose, as an executable semantics adapting the Cerberus C semantics, and mechanised in Coq.
This establishes a solid foundation for CHERI C, for those porting code to it, for compiler implementers, and for future semantics and verification.
},
pdf = {http://www.cl.cam.ac.uk/users/pes20/asplos24spring-paper110.pdf},
topic = {cheri},
cheriformal = {true},
elver = {true},
recent = {true}
}
@inproceedings{AxSL-popl2024,
author = {Angus Hammond{$^1$} and Zongyuan Liu{$^1$} and Thibaut P{\'{e}}rami and Peter Sewell and Lars Birkedal and Jean Pichon-Pharabod},
title = {An axiomatic basis for computer programming on the relaxed {Arm-A} architecture: the {AxSL} logic},
conf = {POPL 2024},
optcrossref = {},
optkey = {},
booktitle = {Proceedings of the 51st ACM SIGPLAN Symposium on Principles of Programming Languages},
optbooktitle = {},
year = {2024},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optpages = {},
month = jan,
optaddress = {},
optorganization = {},
optpublisher = {},
note = {${}^1$These authors contributed equally. Proc. ACM Program. Lang. 8, POPL, Article 21},
optannote = {},
abstract = {Very relaxed concurrency memory models, like those of the Arm-A, RISC-V, and IBM Power hardware architectures, underpin much of computing but break a fundamental intuition about programs, namely that syntactic program order and the reads-from relation always both induce order in the execution. Instead, out-of-order execution is allowed except where prevented by certain pairwise dependencies, barriers, or other synchronisation. This means that there is no notion of the `current' state of the program, making it challenging to design (and prove sound) syntax-directed, modular reasoning methods like Hoare logics, as usable resources cannot implicitly flow from one program point to the next.
We present AxSL, a separation logic for the relaxed memory model of Arm-A, that captures the fine-grained reasoning underpinning the low-overhead synchronisation mechanisms used by high-performance systems code. In particular, AxSL allows transferring arbitrary resources using relaxed reads and writes when they induce inter-thread ordering. We mechanise AxSL in the Iris separation logic framework, illustrate it on key examples, and prove it sound with respect to the axiomatic memory model of Arm-A. Our approach is largely generic in the axiomatic model and in the instruction-set semantics, offering a potential way forward for compositional reasoning for other similar models, and for the combination of production concurrency models and full-scale ISAs.
},
doi = {10.1145/3632863},
pdf = {https://www.cl.cam.ac.uk/~pes20/axsl-popl-2024.pdf},
topic = {Power_and_ARM},
optproject = {},
elver = {true},
recent = {true},
pkvm = {true}
}
@inproceedings{fulminate-popl2025,
author = {Rini Banerjee and Kayvan Memarian and Dhruv Makwana and Christopher Pulte and Neel Krishnaswami and Peter Sewell},
title = {Fulminate: Testing {CN} Separation-Logic Specifications in {C}},
optcrossref = {},
optkey = {},
conf = {POPL 2025},
booktitle = {Proceedings of the 52nd ACM SIGPLAN Symposium on Principles of Programming Languages (Proc. PACM Programming Languages 9, POPL)},
optbooktitle = {},
year = {2025},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optpages = {},
month = jan,
optaddress = {},
optorganization = {},
publisher = {ACM},
doi = {10.1145/3704879},
pdf = {http://www.cl.cam.ac.uk/users/pes20/cn-testing-popl2025.pdf},
optnote = {},
optannote = {},
abstract = {Separation logic has become an important tool for formally capturing and reasoning about the ownership patterns of imperative programs, originally for paper proof, and now the foundation for industrial static analyses and multiple proof tools. However, there has been very little work on program \emph{testing} of separation-logic specifications in concrete execution. At first sight, separation-logic formulas are hard to evaluate in reasonable time, with their implicit quantification over heap splittings, and other explicit existentials.
In this paper we observe that a restricted fragment of separation logic, adopted in the CN proof tool to enable predictable proof automation, also has a natural and readable \emph{computational} interpretation, that makes it practically usable in runtime testing. We discuss various design issues and develop this as a C+CN source to C source translation, Fulminate. This adds checks -- including ownership checks and ownership transfer -- for C code annotated with CN pre- and post-conditions; we demonstrate this on nontrivial examples, including the allocator from a production hypervisor. We formalise our runtime ownership testing scheme, showing (and proving) how its reified ghost state correctly captures ownership passing, in a semantics for a small C-like language.
},
elver = {true},
recent = {true},
topic = {CN},
opttopictwo = {Cerberus},
pkvm = {true}
}
@article{DBLP:journals/ieeesp/WatsonCCDFLMNRSWW24,
author = {Robert N. M. Watson and
David Chisnall and
Jessica Clarke and
Brooks Davis and
Nathaniel Wesley Filardo and
Ben Laurie and
Simon W. Moore and
Peter G. Neumann and
Alexander Richardson and
Peter Sewell and
Konrad Witaszczyk and
Jonathan Woodruff},
title = {{CHERI:} Hardware-Enabled {C/C++} Memory Protection at Scale},
journal = {{IEEE} Secur. Priv.},
volume = {22},
number = {4},
pages = {50--61},
year = {2024},
url = {https://doi.org/10.1109/MSEC.2024.3396701},
pdf = {https://www.cl.cam.ac.uk/research/security/ctsrd/pdfs/20240419-ieeesp-cheri-memory-safety.pdf},
doi = {10.1109/MSEC.2024.3396701},
timestamp = {Thu, 22 Aug 2024 20:23:54 +0200},
biburl = {https://dblp.org/rec/journals/ieeesp/WatsonCCDFLMNRSWW24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org},
abstract = {The memory-safe Capability Hardware Enhanced RISC Instructions (CHERI) C and C++ languages build on architectural capabilities in the CHERI protection model. With the development of two industrial CHERI-enabled processors, Arm’s Morello and Microsoft’s CHERIoT, CHERI may offer the fastest path to widely deployed memory safety.},
topic = {cheri},
recent = {true}
}
@article{10.1145/3708553,
author = {Watson, Robert N.M. and Baldwin, John and Chisnall, David and Chen, Tony and Clarke, Jessica and Davis, Brooks and Filardo, Nathaniel and Gutstein, Brett and Jenkinson, Graeme and Laurie, Ben and Mazzinghi, Alfredo and Moore, Simon and Neumann, Peter G. and Okhravi, Hamed and Richardson, Alex and Rebert, Alex and Sewell, Peter and Tratt, Laurence and Vijayaraghavan, Murali and Vincent, Hugo and Witaszczyk, Konrad},
title = {It Is Time to Standardize Principles and Practices for Software Memory Safety},
year = {2025},
issue_date = {February 2025},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {68},
number = {2},
issn = {0001-0782},
opturl = {https://doi.org/10.1145/3708553},
url = {https://cacm.acm.org/opinion/it-is-time-to-standardize-principles-and-practices-for-software-memory-safety/},
doi = {10.1145/3708553},
abstract = {Twenty-one authors, spanning academia and industry, with expertise in memory-safety research, deployment, and policy, argue that standardization is an essential next step to achieving universal strong memory safety.},
journal = {Communications of the ACM},
month = jan,
pages = {40–45},
numpages = {6},
topic = {cheri},
recent = {true}
}
@inproceedings{DBLP:conf/cpp/ZalivaM00FSS25,
author = {Vadim Zaliva and
Kayvan Memarian and
Brian Campbell and
Ricardo Almeida and
Nathaniel Wesley Filardo and
Ian Stark and
Peter Sewell},
editor = {Kathrin Stark and
Amin Timany and
Sandrine Blazy and
Nicolas Tabareau},
title = {A {CHERI} {C} Memory Model for Verified Temporal Safety},
booktitle = {Proceedings of the 14th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2025, Denver, CO, USA, January
20-21, 2025},
conf = {CPP 2025},
pages = {112--126},
publisher = {{ACM}},
year = {2025},
url = {https://doi.org/10.1145/3703595.3705878},
doi = {10.1145/3703595.3705878},
timestamp = {Sat, 25 Jan 2025 23:07:08 +0100},
biburl = {https://dblp.org/rec/conf/cpp/ZalivaM00FSS25.bib},
bibsource = {dblp computer science bibliography, https://dblp.org},
topic = {cheri},
recent = {true},
elver = {true}
}
@misc{ts6010,
optkey = {},
author = { ISO/IEC JTC 1/SC 22},
title = {{ISO/IEC TS 6010:2025 Programming languages --- C --- A provenance-aware memory object model for C}},
howpublished = {ISO},
month = may,
year = {2025},
url = {https://www.iso.org/standard/81899.html},
note = {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. \url{http://www.open-std.org/jtc1/sc22/wg14/www/docs/n3005.pdf}. June 2022.},
optannote = {},
abstract = {This document specifies the form and establishes the interpretation of programs written in the C programming language. It is not a complete specification of that language but builds upon ISO/IEC 9899:2018 by constraining and clarifying the Memory Object Model.
The resolution of DR260 confirmed the concept of provenance of pointers, introduced as
means to track and distinguish pointer values that represent storage instances with the
same address. Implementations started to use that concept in optimisations relying on
provenance-based alias analysis, without it ever being clearly or formally defined, and
without it being integrated consistently with the rest of the C standard. This document
provides a solution for this: a provenance-aware memory object model for C to put C
programmers and implementers on a solid footing in this regard.
In addition to this document, \url{https://cerberus.cl.cam.ac.uk/cerberus} provides an
executable version of the semantics, with a web interface that allows one to explore
and visualise the behaviour of small test programs.
This document does not address subobject provenance.
},
topic = {Cerberus},
recent = {true},
elver = {true}
}
@inproceedings{simner-isca2025,
title = {Precise exceptions in relaxed architectures},
author = {Ben Simner and Alasdair Armstrong and Thomas Bauereiss and Brian Campbell and Ohad Kammar and Jean Pichon-Pharabod and Peter Sewell},
optcrossref = {},
optkey = {},
conf = {ISCA 2025},
booktitle = {International Symposium on Computer Architecture},
year = {2025},
pdf = {http://www.cl.cam.ac.uk/users/pes20/isca25-113.pdf},
doi = {https://doi.org/10.1145/3695053.3731102},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optpages = {},
month = jun,
optaddress = {},
optorganization = {},
optpublisher = {},
note = {Best paper award.},
optannote = {},
abstract = {
To manage exceptions, software relies on a key architectural guarantee, \emph{precision}: that exceptions appear to execute between instructions. However, this definition, dating back over 60 years, fundamentally assumes a sequential programmers model. Modern architectures such as Arm-A with programmer-observable relaxed behaviour make such a naive definition inadequate, and it is unclear exactly what guarantees programmers have on exception entry and exit.
In this paper, we clarify the concepts needed to discuss exceptions in the relaxed-memory setting -- a key aspect of precisely specifying the architectural interface between hardware and software. We explore the basic relaxed behaviour across exception boundaries, and the semantics of external aborts, using Arm-A as a representative modern architecture. We identify an important problem, present yet unexplored for decades: pinning down what it means for exceptions to be precise in a relaxed setting. We describe key phenomena that any definition should account for. We develop an axiomatic model for Arm-A precise exceptions, tooling for axiomatic model execution, and a library of tests. Finally we explore the relaxed semantics of software-generated interrupts, as used in sophisticated programming patterns, and sketch how they too could be modelled.
},
recent = {true},
elver = {true},
topic = {Power_and_ARM},
pkvm = {true}
}
@inproceedings{morello-cerise-pldi2025,
author = {Angus Hammond and Ricardo Almeida and Thomas Bauereiss and Brian Campbell and Ian Stark and Peter Sewell},
title = {{Morello-Cerise}: A Proof of Strong Encapsulation for the {Arm}
{Morello} Capability Hardware Architecture},
optcrossref = {},
optkey = {},
conf = {PLDI 2025},
booktitle = {Proc. ACM Programming Languages 9},
year = 2025,
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optpages = {},
month = jun,
pdf = {http://www.cl.cam.ac.uk/users/pes20/pldi25-paper646-camera-ready.pdf},
doi = {https://doi.org/10.1145/3729329},
optaddress = {},
optorganization = {},
optpublisher = {},
optnote = {},
optannote = {},
abstract = {When designing new architectural security mechanisms, a key question is whether they actually provide the intended security, but this has historically been very hard to assess. One cannot gain much confidence by testing, as such mechanisms should provide protection in the presence of arbitrary unknown code. Previously, one also could not gain confidence by mechanised proof, as the scale of production instruction-set architecture (ISA) designs, many tens or hundreds of thousands of lines of specification, made that prohibitive.
We focus in this paper especially on the secure encapsulation of software components, as supported by CHERI architectures in general and by the Arm Morello prototype architecture and hardware design in particular. Secure encapsulation is an essential security mechanism, for fault isolation and to constrain untrusted third-party code. It has previously often been implemented using virtual memory, but that does not scale to large numbers of compartments. Morello provides capability-based mechanisms that do scale, within a single address space.
We prove a strong secure encapsulation property for an example of encapsulated code running on Morello, that holds in the presence of arbitrary untrusted code, above a full-scale sequential model of the Morello ISA. To do so, we build on, extend, and unify three orthogonal lines of previous work: the Cerise proof of such an encapsulation property for a highly idealised capability machine, expressed using a logical relation in Iris; the Islaris approach for reasoning about known code in production-scale ISAs; and the T-CHERI security properties of arbitrary Morello code, previously proved only for executions up to domain crossing.
This demonstrates how one can prove such strong properties of security mechanisms for full-scale industry architectures.
},
recent = {true},
elver = {true},
topic = {cheri}
}
@inproceedings{coqPL2025,
author = {Thibaut P{\'e}rami},
title = {Towards general white-box automation: a typeclass-guided context cleaner},
optcrossref = {},
optkey = {},
booktitle = {The Eleventh International Workshop on {Coq} for Programming Languages},
conf = {CoqPL 2025},
year = {2025},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optpages = {},
month = jan,
optaddress = {},
optorganization = {},
optpublisher = {},
optnote = {},
url = {https://popl25.sigplan.org/details/CoqPL-2025-papers/10/Towards-general-white-box-automation-a-typeclass-guided-context-cleaner},
optannote = {},
elver = {true},
recent = {true},
pkvm = {true}
}
@misc{ploix2025comprehensiveformalverificationobservational,
title = {Comprehensive Formal Verification of Observational Correctness for the {CHERIoT-Ibex} Processor},
author = {Louis-Emile Ploix and Alasdair Armstrong and Tom Melham and Ray Lin and Haolong Wang and Anastasia Courtney},
year = {2025},
month = feb,
eprint = {2502.04738},
archiveprefix = {arXiv},
primaryclass = {cs.AR},
url = {https://arxiv.org/abs/2502.04738},
abstract = {The CHERI architecture equips conventional RISC ISAs with significant architectural extensions that provide a hardware-enforced mechanism for memory protection and software compartmentalisation. Architectural capabilities replace conventional integer pointers with memory addresses bound to permissions constraining their use. We present the first comprehensive formal verification of a capability extended RISC-V processor with internally `compressed' capabilities -- a concise encoding of capabilities with some resemblance to floating point number representations.
The reference model for RTL correctness is a minor variant of the full and definitive ISA description written in the Sail ISA specification language. This is made accessible to formal verification tools by a prototype flow for translation of Sail into SystemVerilog. Our verification demonstrates a methodology for establishing that the processor always produces a stream of interactions with memory that is identical to that specified in Sail, when started in the same initial state. We additionally establish liveness. This abstract, microarchitecture-independent observational correctness property provides a comprehensive and clear assurance of functional correctness for the CHERIoT-Ibex processor's observable interactions with memory.},
topictwo = {cheri},
topic = {ISA_semantics},
recent = {true}
}