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{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{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},
errata = {http://www.cl.cam.ac.uk/users/pes20/isca25-113-errata.md},
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{execspec-sosp25,
author = {
Kayvan Memarian and
Ben Simner and
David Kaloper-Meršinjak and
Thibaut Pérami and
Peter Sewell
},
title = {Ghost in the {Android} Shell: Pragmatic Test-oracle Specification of a Production Hypervisor},
conf = {SOSP 2025},
organization = {ACM},
address = {Seoul, Republic of Korea},
booktitle = {Proceedings of the ACM SIGOPS 31st Symposium on Operating Systems Principles},
year = {2025},
month = oct,
doi = {10.1145/3731569.3764817},
abstract = {
Developing systems code that robustly provides its intended security guarantees remains very challenging: conventional practice does not suffice, and full functional verification, while now feasible in some contexts, has substantial barriers to entry and use.
In this paper, we explore an alternative, more lightweight approach to building confidence for a production hypervisor: the pKVM hypervisor developed by Google to protect virtual machines and the Android kernel from each other. The basic approach is very simple and dates back to the 1970s: we specify the desired behaviour in a way that can be used as a test oracle, and check correspondence between that and the implementation at runtime. The setting makes that challenging in several ways: the implementation and specification are intertwined with the underlying architecture; the hypervisor is highly concurrent; the specification has to be loose in certain ways; the hypervisor runs bare-metal in a privileged exception level; naive random testing would quickly crash the whole system; and the hypervisor is written in C using conventional methods. We show how all of these can be overcome to make a practically useful specification, finding a number of critical bugs in pKVM along the way.
This is not at all what conventional developers (nor what formal verifiers) normally do -- but we argue that, with the appropriate mindset, they easily could and should.
},
pdf = {https://www.cl.cam.ac.uk/~pes20/Stuff/exec-spec-paper.pdf},
recent = {true},
elver = {true},
pkvm = {true}
}
@inproceedings{archsem-popl2026,
author = {Thibaut P{\'e}rami and Thomas Bauereiss and Brian Campbell and Zongyuan Liu and Nils Lauermann and Alasdair Armstrong and Peter Sewell},
github = {https://github.com/rems-project/archsem},
title = {{ArchSem}: Reusable rigorous semantics of relaxed architectures},
optcrossref = {},
optkey = {},
conf = {POPL 2026},
booktitle = {POPL 2026},
booktitle = {Proceedings of the 53rd ACM SIGPLAN Symposium on Principles of Programming Languages (PACM PL Vol.~10, No.~POPL, Article~8},
year = 2026,
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optpages = {},
month = jan,
optaddress = {},
optorganization = {},
optpublisher = {},
optnote = {},
optannote = {},
doi = {https://doi.org/10.1145/3776650},
pdf = {https://www.cl.cam.ac.uk/~pes20/Stuff/2025-archsem-paper.pdf},
abstract = {
The specifications of mainstream processor architectures, such as Arm, x86, and RISC-V, underlie modern computing, as the targets of compilers, operating systems, and hypervisors. However, despite extensive research and tooling for instruction-set architecture (ISA) and relaxed-memory semantics, recently including systems features, there still do not exist integrated mathematical models that suffice for foundational formal verification, of concurrent architecture properties or of systems software. Previous proof-assistant work has had to substantially simplify the ISA semantics, the concurrency model, or both.
We present ArchSem, an architecture-generic framework for architecture semantics, modularly combining ISA and concurrency models along a tractable interface of instruction-semantics effects, that covers a range of systems aspects. To do so, one has to handle many issues that were previously unclear, about the architectures themselves, the interface, the proper definition of reusable models, and the Rocq and Isabelle idioms required to make it usable. We instantiate it to the Arm-A and RISC-V instruction-set architectures and multiple concurrency models.
We demonstrate usability for proof, despite the scale, by establishing that the Arm architecture (in a particular configuration) provides a provable virtual memory abstraction, with a combination of Rocq, Isabelle, and paper proof. Previous work provides further confirmation of usability: the AxSL program logic for Arm relaxed concurrency was proved sound above an earlier version of ArchSem.
This establishes a basis for future proofs of architecture properties and systems software, above production architecture specifications.
},
recent = {true},
elver = {true},
topic = {Power_and_ARM}
}
@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}
}
@phdthesis{simner2025,
title = {Arm systems semantics},
author = {Ben Simner},
year = 2025,
month = apr,
url = {https://www.repository.cam.ac.uk/handle/1810/389436},
pdf = {https://www.repository.cam.ac.uk/bitstreams/b37a1aa9-354d-4d5e-8d80-3d10d5891ce8/download},
doi = {10.17863/CAM.121319},
school = {University of Cambridge},
abstract = {Computing relies on architecture specifications to decouple hardware and software development. Historically
these have been prose documents, with all the problems that entails, but research over the last ten years has
developed rigorous and executable-as-test-oracle specifications of mainstream architecture instruction sets
and `user-mode' concurrency, clarifying architectures and bringing them into the scope of programming-language semantics and verification.
However, the system semantics, of address translation and TLB maintenance, instruction-fetch and its
required cache maintenance, and exceptions and interrupts, remains mostly obscure, leaving us without a
solid foundation for verification of security-critical systems software.
We develop precise mathematical models, for those aspects of the Arm A-class architecture. We implement
these models as executable models, in both microarchitectural-flavoured operational and declarative
axiomatic style formats. We validate these models, against currently available hardware through the
production and evaluation of hardware test harnesses and test suites, and against the architectural intent
through discussions with Arm architects. We give a variety of hand-written and machine-generated litmus
tests, exercising parts of the architecture previously unexplored.
We discuss the nature of developing such models, and the challenges that writing specifications of existing
systems entails. We briefly touch on how these models have evolved over time, and how we imagine they
will evolve in the future as the remaining questions are resolved.},
topic = {Power_and_ARM},
elver = {true},
recent = {true},
pkvm = {true},
errata = {https://2plus2a.com/publications/errata#thesis}
}