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}}
@misc{n3005,
optkey = {},
author = {Jens Gustedt and Peter Sewell and Kayvan Memarian and Victor B. F. Gomes and Martin Uecker},
title = {N3005: A Provenance-aware Memory Object Model for {C}. Working Draft {Technical Specification ISO/IEC TS 6010:2023 (E)}},
howpublished = {ISO/IEC JTC1/SC22/WG14 N3005 \url{http://www.open-std.org/jtc1/sc22/wg14/www/docs/n3005.pdf}},
pdf = {http://www.open-std.org/jtc1/sc22/wg14/www/docs/n3005.pdf},
month = jun,
year = {2022},
abstract = {In a committee discussion from 2004 concerning DR260, WG14 confirmed the concept of provenance of pointers,
introduced as means to track and distinguish pointer values that represent storage instances with same address but
non-overlapping lifetimes. 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 Technical Specification 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.},
elver = {true},
topic = {WG14},
recent = {true},
optnote = {},
optannote = {}
}
@misc{acs-2020,
optkey = {},
author = {Peter Sewell and Christopher Pulte and Shaked Flur and Mark Batty and Luc Maranget and Alasdair Armstrong},
title = {Multicore Semantics: Making Sense of Relaxed Memory (MPhil slides)},
opthowpublished = {},
month = oct,
year = 2022,
optnote = {\url{https://www.cl.cam.ac.uk/~pes20/slides-acs-2022.pdf}},
url = {https://www.cl.cam.ac.uk/~pes20/slides-acs-2022.pdf},
optannote = {},
recent = {true},
topic = {Power_and_ARM},
topictwo = {ISA_semantics}
}
@inproceedings{2022-popl-vip,
author = {Rodolphe Lepigre and Michael Sammler and Kayvan Memarian and Robbert Krebbers and Derek Dreyer and Peter Sewell},
title = {{VIP}: Verifying Real-World {C} Idioms with Integer-Pointer Casts},
optcrossref = {},
optkey = {},
conf = {POPL 2022},
booktitle = {Proceedings of the 49th ACM SIGPLAN Symposium on Principles of Programming Languages},
optbooktitle = {},
year = {2022},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optpages = {},
month = jan,
optaddress = {},
optorganization = {},
optpublisher = {},
note = {Proc. ACM Program. Lang. 6, POPL, Article 20},
optnote = {},
optannote = {},
doi = {10.1145/3498681},
abstract = {Systems code often requires fine-grained control over memory layout and pointers, expressed using low-level (e.g.~bitwise) operations on pointer values.
Since these operations go beyond what basic pointer arithmetic in C allows, they are performed with the help of \emph{integer-pointer casts}.
Prior work has explored increasingly realistic memory object models for C that account for the desired semantics of integer-pointer casts while also being sound w.r.t.\ compiler optimisations, culminating in PNVI, the preferred memory object model in ongoing discussions within the ISO WG14 C standards committee.
However, its complexity makes it an unappealing target for verification, and no tools currently exist to verify C programs under PNVI.
In this paper, we introduce VIP, a new memory object model aimed at supporting C verification.
VIP sidesteps the complexities of PNVI with a simple but effective idea: a new construct that lets programmers express the intended provenances of integer-pointer casts explicitly.
At the same time, we prove VIP compatible with PNVI, thus enabling verification on top of VIP to benefit from PNVI's validation with respect to practice.
In particular, we build a verification tool, RefinedC-VIP, for verifying programs under VIP semantics.
As the name suggests, RefinedC-VIP extends the recently developed RefinedC tool, which is automated yet also produces foundational proofs in Coq.
We evaluate RefinedC-VIP on a range of systems-code idioms, and validate VIP's expressiveness via an implementation in the Cerberus C semantics.},
optapollourl = {https://www.repository.cam.ac.uk/handle/1810/288588},
pdf = {http://www.cl.cam.ac.uk/users/pes20/2022-popl-vip.pdf},
supplementarymaterial = {https://doi.org/10.5281/zenodo.5662349},
topic = {Cerberus},
project = {https://gitlab.mpi-sws.org/iris/refinedc},
elver = {true},
recent = {true},
pkvm = {true}
}
@inproceedings{relaxedVM-esop2022,
author = {
Ben Simner and
Alasdair Armstrong and
Jean Pichon-Pharabod and
Christopher Pulte and
Richard Grisenthwaite and
Peter Sewell
},
title = {Relaxed virtual memory in {Armv8-A}},
optcrossref = {},
optkey = {},
conf = {ESOP 2022},
booktitle = {Proceedings of the 31st European Symposium on Programming},
year = {2022},
optbooktitle = {},
optyear = {},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optpages = {},
month = apr,
optaddress = {},
optorganization = {},
optpublisher = {},
optnote = {},
optannote = {},
optbooktitle = {Programming Languages and Systems - 31st European Symposium on Programming,
{ESOP} 2022, Held as Part of the European Joint Conferences on Theory
and Practice of Software, {ETAPS} 2022, Munich, Germany, April 2-7,
2022, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {13240},
pages = {143--173},
publisher = {Springer},
optyear = {2022},
url = {https://doi.org/10.1007/978-3-030-99336-8\_6},
doi = {10.1007/978-3-030-99336-8\_6},
timestamp = {Fri, 01 Apr 2022 15:49:28 +0200},
biburl = {https://dblp.org/rec/conf/esop/SimnerAPPGS22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org},
abstract = {
Virtual memory is an essential mechanism for enforcing security boundaries,
but its relaxed-memory concurrency semantics has not previously been investigated in detail. The concurrent systems code managing virtual memory has been left on an entirely informal basis, and
OS and hypervisor verification has had to make major simplifying assumptions.
We explore the design space for relaxed virtual memory semantics in the Armv8-A architecture, to support future system-software verification. We identify many design questions, in discussion with Arm; develop a test suite, including use cases from the pKVM production hypervisor under development by Google; delimit the design space with axiomatic-style concurrency models; prove that under simple stable configurations our architectural model collapses to previous ``user'' models; develop tooling to compute allowed behaviours in the model integrated with the full Armv8-A ISA semantics; and develop a hardware test harness.
This lays out some of the main issues in relaxed virtual memory bringing these security-critical systems phenomena into the domain of programming-language semantics and verification with foundational architecture semantics.
},
pdf = {http://www.cl.cam.ac.uk/users/pes20/RelaxedVM-Arm/RelaxedVM-Arm-esop2022.pdf},
topic = {Power_and_ARM},
elver = {true},
project = {http://www.cl.cam.ac.uk/~pes20/RelaxedVM-Arm},
recent = {true},
pkvm = {true}
}
@inproceedings{morello-proofs-esop2022,
author = {Bauereiss, Thomas and Campbell, Brian and Sewell, Thomas
and Armstrong, Alasdair and Esswood, Lawrence and Stark,
Ian and Barnes, Graeme and Watson, Robert N. M. and Sewell,
Peter},
title = {Verified Security for the {Morello} Capability-enhanced
Prototype {Arm} Architecture},
optcrossref = {},
optkey = {},
conf = {ESOP 2022},
booktitle = {Proceedings of the 31st European Symposium on Programming},
year = {2022},
optbooktitle = {},
optyear = {},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optpages = {},
month = apr,
optaddress = {},
optorganization = {},
optpublisher = {},
opteditor = {Ilya Sergey},
opttitle = {Verified Security for the Morello Capability-enhanced Prototype Arm
Architecture},
optbooktitle = {Programming Languages and Systems - 31st European Symposium on Programming,
{ESOP} 2022, Held as Part of the European Joint Conferences on Theory
and Practice of Software, {ETAPS} 2022, Munich, Germany, April 2-7,
2022, Proceedings},
optseries = {Lecture Notes in Computer Science},
optvolume = {13240},
pages = {174--203},
publisher = {Springer},
url = {https://doi.org/10.1007/978-3-030-99336-8\_7},
doi = {10.1007/978-3-030-99336-8\_7},
timestamp = {Fri, 01 Apr 2022 15:49:28 +0200},
biburl = {https://dblp.org/rec/conf/esop/BauereissCSAESB22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org},
optnote = {},
optannote = {},
abstract = {Memory safety bugs continue to be a major source of security vulnerabilities in our critical infrastructure. The CHERI project has proposed extending conventional architectures with hardware-supported \emph{capabilities} to enable fine-grained memory protection and scalable compartmentalisation, allowing historically memory-unsafe C and C++ to be adapted to deterministically mitigate large classes of vulnerabilities, while requiring only minor changes to existing system software sources. Arm is currently designing and building Morello, a CHERI-enabled prototype architecture, processor, SoC, and board, extending the high-per\-for\-mance Neoverse N1, to enable industrial evaluation of CHERI and pave the way for potential mass-market adoption. However, for such a major new security-oriented architecture feature, it is important to establish high confidence that it does provide the intended protections, and that cannot be done with conventional engineering techniques.
In this paper we put the Morello architecture on a solid mathematical footing from the outset. We define the fundamental security property that Morello aims to provide, reachable capability monotonicity, and prove that the architecture definition satisfies it. This proof is mechanised in Isabelle/HOL, and applies to a translation of the official Arm specification of the Morello instruction-set architecture (ISA) into Isabelle. The main challenge is handling the complexity and scale of a production architecture: 62,000 lines of specification, translated to 210,000 lines of Isabelle. We do so by factoring the proof via a narrow abstraction capturing essential properties of arbitrary CHERI ISAs, expressed above a monadic intra-instruction semantics. We also develop a model-based test generator, which generates instruction-sequence tests that give good specification coverage, used in early testing of the Morello implementation and in Morello QEMU development, and we use Arm's internal test suite to validate our model.
This gives us machine-checked mathematical proofs of whole-ISA security properties of a full-scale industry architecture, at design-time. To the best of our knowledge, this is the first demonstration that that is feasible, and it significantly increases confidence in Morello.
},
pdf = {http://www.cl.cam.ac.uk/~pes20/morello-proofs-esop2022.pdf},
project = {https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/},
topic = {cheri},
topictwo = {ISA_semantics},
cheriformal = {true},
elver = {true},
recent = {true}
}
@inproceedings{2022-pldi-islaris,
author = {Michael Sammler and Angus Hammond and Rodolphe Lepigre and Brian Campbell and Jean Pichon-Pharabod and Derek Dreyer and Deepak Garg and Peter Sewell},
title = {{Islaris}: Verification of Machine Code Against Authoritative {ISA} Semantics},
optcrossref = {},
optkey = {},
doi = {10.1145/3519939.3523434},
year = {2022},
isbn = {978-1-4503-9265-5/22/06},
conf = {PLDI 2022},
booktitle = {Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation},
optbooktitle = {San Diego, CA, USA},
optyear = {},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optpages = {},
month = jun,
optaddress = {},
optorganization = {},
optpublisher = {},
optnote = {},
optannote = {},
abstract = {
Recent years have seen great advances towards verifying large-scale systems code. However, these verifications are usually based on hand-written assembly or machine-code semantics for the underlying architecture that only cover a small part of the instruction set architecture (ISA). In contrast, other recent work has used Sail to establish formal models for large real-world architectures, including Armv8-A and RISC-V, that are comprehensive (complete enough to boot an operating system or hypervisor) and authoritative (automatically derived from the Arm internal model and validated against the Arm validation suite, and adopted as the official formal specification by RISC-V International, respectively). But the scale and complexity of these models makes them challenging to use as a basis for verification.
In this paper, we propose Islaris, the first system to support verification of machine code above these complete and authoritative real-world ISA specifications. Islaris uses a novel combination of \emph{SMT-solver-based symbolic execution} (the Isla symbolic executor) and \emph{automated reasoning in a foundational program logic} (a new separation logic we derive using Iris in Coq). We show that this approach can handle Armv8-A and RISC-V machine code exercising a wide range of systems features, including installing and calling exception vectors, code parametric on a relocation address offset (from the production pKVM hypervisor); unaligned access faults; memory-mapped IO; and compiled C code using inline assembly and function pointers.
},
pdf = {http://www.cl.cam.ac.uk/~pes20/2022-pldi-islaris.pdf},
project = {https://github.com/rems-project/islaris},
topic = {ISA_semantics},
recent = {true},
elver = {true},
pkvm = {true}
}
@misc{cheri-formal-blog,
optkey = {},
author = {Peter Sewell and Thomas Bauereiss and Brian Campbell and Robert N. M. Watson},
title = {Formal {CHERI}: rigorous engineering and design-time proof of full-scale architecture security properties},
howpublished = {Blog post, \url{https://www.lightbluetouchpaper.org/2022/07/22/formal-cheri/}},
month = jul,
year = {2022},
optnote = {},
optannote = {},
project = {https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/},
url = {https://www.lightbluetouchpaper.org/2022/07/22/formal-cheri/},
topic = {cheri},
cheriformal = {true},
elver = {true},
recent = {true}
}
@misc{reviewing-blog,
optkey = {},
author = {Peter Sewell},
title = {Bad Reasons to Reject Good Papers, and vice versa},
howpublished = {SIGPLAN PL Perspectives Blog},
month = dec,
year = 2021,
url = {https://blog.sigplan.org/2021/12/07/bad-reasons-to-reject-good-papers-and-vice-versa/},
note = {Also published 2022-12-07 on the Communications of the ACM Blog \url{https://cacm.acm.org/blogs/blog-cacm/267440-bad-reasons-to-reject-good-papers-and-vice-versa/fulltext}},
optannote = {},
recent = {true},
misc = {true},
topic = {misc}
}
@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{nextwave2023,
author = {Robert N. M. Watson and Peter Sewell and William Martin},
title = {Improving Security with Hardware Support: {CHERI} and {Arm's Morello}},
journal = {The Next Wave (The National Security Agency's review of emerging technologies)},
year = 2023,
optkey = {},
volume = 4,
number = 1,
pages = {10--21},
optmonth = {},
pdf = {https://media.defense.gov/2023/Jan/23/2003148354/-1/-1/0/TNW_24-1_2023_20230112.PDF},
note = {ISSN 2640-1789 (print), ISSN 2640-1797 (online)},
optannote = {},
project = {https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/},
topic = {cheri},
cheriformal = {true},
elver = {true},
recent = {true},
abstract = {
The CHERI project, from the University of Cambridge and SRI International, extends
instruction-set architectures (ISAs) with unforgeable architectural capabilities, to be
used in place of conventional machine-word addresses to access memory. CHERI, which
stands for Capability Hardware Enhanced Reduced Instruction Set Computer (RISC) Instructions,
deterministically protects C/C++ pointers and other references, and also enables in-address-space software sandboxing. With changes to the compiler and operating system (OS), CHERI
enables new hardware-software security protection models for existing software (typically with
only very minor changes for memory safety):
- Deterministic fine-grained C/C++ memory protection at low overheads; and
- Scalable software compartmentalization, including sandboxed libraries, with interprocess communication performance improvements and function-call-like domain transition.
In a 2020 blog post evaluating CHERI, the Microsoft Security Response Centre (MSRC) wrote:
``We've assessed the theoretical impact of CHERI on all the memory safety vulnerabilities we
received in 2019, and concluded that in its current state, and combined with other mitigations,
it would have deterministically mitigated at least two thirds of all those issues''[1]. Scalable
single-address software sandboxing has the potential to mitigate many more, and to enable a
more disruptive shift to stronger compartmentalized software architectures.
Arm has recently developed the Morello architecture and processor, incorporating the CHERI
protection model into a contemporary high-performance Arm design. Morello is an experimental
prototype extending the existing Armv8-A architecture and Neoverse N1 64-bit processor
design to support CHERI research and evaluation on the path to eventual productization, and
to demonstrate the viability of the CHERI technology using real commercial processes and
manufacturing. Extensive software porting is establishing feasibility. Development boards are
available for research and prototyping as of early 2022, and are already running significant
open-source software stacks, such as an adapted version of the FreeBSD OS and KDE desktop
stack running with strong memory safety [2].
In this article we give an overview of CHERI and Morello, and pointers to full discussions
elsewhere. It is based largely on material from the "Introduction to CHERI" [3] and "Verified
security for the Morello capability-enhanced prototype Arm architecture" [4] technical reports;
it does not contain new research results.
}
}
@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{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.
},
recent = {true},
elver = {true}
}
@misc{simner2024relaxedexceptionsemanticsarma,
title = {Relaxed exception semantics for {Arm-A} (extended version)},
author = {Ben Simner and Alasdair Armstrong and Thomas Bauereiss and Brian Campbell and Ohad Kammar and Jean Pichon-Pharabod and Peter Sewell},
year = {2024},
eprint = {2412.15140},
archiveprefix = {arXiv},
primaryclass = {cs.AR},
url = {https://arxiv.org/abs/2412.15140},
pdf = {https://arxiv.org/pdf/2412.15140},
abstract = {
To manage exceptions, software relies on a key architectural guarantee, 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}
}
@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 = {},
optnote = {},
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},
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}
}