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 sewellbib2.bib}}
@techreport{UCAM-CL-TR-941,
author = {Watson, Robert N. M. and Moore, Simon W. and
Sewell, Peter and Neumann, Peter},
title = {An Introduction to {CHERI}},
year = 2019,
month = sep,
pdf = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-941.pdf},
institution = {University of Cambridge, Computer Laboratory},
number = {UCAM-CL-TR-941},
abstract = {},
project = {https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/},
topic = {cheri},
cheriformal = {true},
elver = {true},
recent = {true}
}
@inproceedings{cheri-formal-SP2020,
author = {Kyndylan Nienhuis and Alexandre Joannou and Thomas Bauereiss and Anthony Fox and Michael Roe and Brian Campbell and Matthew Naylor and Robert M. Norton and Moore, Simon W. and Neumann, Peter G. and Ian Stark and Watson, Robert N. M. and Peter Sewell},
title = {Rigorous engineering for hardware security: Formal modelling and proof in the {CHERI} design and implementation process},
optcrossref = {},
optkey = {},
conf = {Security and Privacy 2020},
booktitle = {Proceedings of the 41st IEEE Symposium on Security and Privacy (SP)},
year = {2020},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
pages = {1007--1024},
month = may,
optaddress = {},
optorganization = {},
optpublisher = {},
optnote = {},
optannote = {},
abstract = {The root causes of many security vulnerabilities include a pernicious combination of two problems, often regarded as inescapable aspects of computing. First, the protection mechanisms provided by the mainstream processor architecture and C/C++ language abstractions, dating back to the 1970s and before, provide only coarse-grain virtual-memory-based protection. Second, mainstream system engineering relies almost exclusively on test-and-debug methods, with (at best) prose specifications. These methods have historically sufficed commercially for much of the computer industry, but they fail to prevent large numbers of exploitable bugs, and the security problems that this causes are becoming ever more acute.
In this paper we show how more rigorous engineering methods can be applied to the development of a new security-enhanced processor architecture, with its accompanying hardware implementation and software stack. We use formal models of the complete instruction-set architecture (ISA) at the heart of the design and engineering process, both in lightweight ways that support and improve normal engineering practice -- as documentation, in emulators used as a test oracle for hardware and for running software, and for test generation -- and for formal verification. We formalise key intended security properties of the design, and establish that these hold with mechanised proof. This is for the same complete ISA models (complete enough to boot operating systems), without idealisation.
We do this for CHERI, an architecture with \emph{hardware capabilities} that supports fine-grained memory protection and scalable secure compartmentalisation, while offering a smooth adoption path for existing software. CHERI is a maturing research architecture, developed since 2010, with work now underway on an Arm industrial prototype to explore its possible adoption in mass-market commercial processors. The rigorous engineering work described here has been an integral part of its development to date, enabling more rapid and confident experimentation, and boosting confidence in the design.
},
pdf = {https://www.cl.cam.ac.uk/users/pes20/cheri-formal.pdf},
apollourl = {https://www.repository.cam.ac.uk/handle/1810/302580},
publisherurl = {https://www.computer.org/csdl/proceedings-article/sp/2020/349700b007/1j2Lg3o6fdK},
doi = {10.1109/SP40000.2020.00055},
project = {https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/},
topic = {cheri},
cheriformal = {true},
elver = {true},
recent = {true}
}
@inproceedings{cornucopia,
author = {Nathaniel Wesley Filardo and Brett F. Gutstein and Jonathan Woodruff and Sam Ainsworth and Lucian Paul-Trifu and Brooks Davis and Hongyan Xia and Edward Tomasz Napierala and Alexander Richardson and John Baldwin and David Chisnall and Jessica Clarke and Khilan Gudka and Alexandre Joannou and A. Theodore Markettos and Alfredo Mazzinghi and Robert M. Norton and Michael Roe and Peter Sewell and Stacey Son and Timothy M. Jones and Simon W. Moore and Peter G. Neumann and Robert N. M. Watson},
conf = {Security and Privacy 2020},
booktitle = {Proceedings of the 41st IEEE Symposium on Security and Privacy (SP)},
title = {Cornucopia: Temporal Safety for {CHERI} Heaps},
year = {2020},
volume = {},
issn = {2375-1207},
pages = {1507-1524},
keywords = {},
doi = {10.1109/SP40000.2020.00098},
pdf = {https://www.cl.cam.ac.uk/research/security/ctsrd/pdfs/2020oakland-cornucopia.pdf},
apollourl = {https://www.repository.cam.ac.uk/handle/1810/304040},
publisherurl = {https://doi.ieeecomputersociety.org/10.1109/SP40000.2020.00098},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
month = {may},
abstract = {Use-after-free violations of temporal memory safety continue to plague software systems, underpinning many high-impact exploits. The CHERI capability system shows great promise in achieving C and C++language spatial memory safety, preventing out-of-bounds accesses. Enforcing language-level temporal safety on CHERI requires capability revocation, traditionally achieved either via table lookups (avoided for performance in the CHERI design) or by identifying capabilities in memory to revoke them (similar to a garbage-collector sweep). CHERIvoke,a prior feasibility study, suggested that CHERI’s tagged capabilities could make this latter strategy viable, but modeled only architectural limits and did not consider the full implementation or evaluation of the approach.
Cornucopia is a lightweight capability revocation system for CHERI that implements non-probabilistic C/C++temporal memory safety for standard heap allocations. It extends the CheriBSD virtual-memory subsystem to track capability flow through memory and provides a concurrent kernel-resident revocation service that is amenable to multi-processor and hardware acceleration. We demonstrate an average overhead of less than 2\% and a worst-case of 8.9\% for concurrent revocation on compatible SPECCPU2006 benchmarks on a multi-core CHERI CPU on FPGA, and we validate Cornucopia against the Juliet test suite’s corpus of temporally unsafe programs. We test its compatibility with a large corpus of C programs by using a revoking allocator as the system allocator while booting multi-user CheriBSD. Cornucopia is a viable strategy for always-on temporal heap memory safety, suitable for production environments.
},
project = {https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/},
topic = {cheri},
optcheriformal = {false},
elver = {true},
recent = {true}
}
@inproceedings{iflat-esop2020-extended,
author = {Ben Simner and Shaked Flur and Christopher Pulte and Alasdair Armstrong and Jean Pichon-Pharabod and Luc Maranget and Peter Sewell},
title = {{ARMv8-A} system semantics: instruction fetch in relaxed architectures},
optcrossref = {},
optkey = {},
conf = {ESOP 2020},
booktitle = {Proceedings of the 29th European Symposium on Programming},
year = {2020},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optpages = {},
month = apr,
optaddress = {},
optorganization = {},
optpublisher = {},
optnote = {This is an extended version of the ESOP 2020 paper, with appendices giving additional details},
optannote = {},
abstract = {Computing relies on \emph{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 \emph{system semantics}, of instruction-fetch and cache maintenance, exceptions and interrupts, and address translation, remains obscure, leaving us without a solid foundation for verification of security-critical systems software.
In this paper we establish a robust model for one aspect of system semantics: instruction fetch and cache maintenance for ARMv8-A. Systems code relies on executing instructions that were written by data writes, e.g.~in program loading, dynamic linking, JIT compilation, debugging, and OS configuration, but hardware implementations are often highly optimised, e.g.~with instruction caches, linefill buffers, out-of-order fetching, branch prediction, and instruction prefetching, which can affect programmer-observable behaviour. It is essential, both for programming and verification, to abstract from such microarchitectural details as much as possible, but no more. We explore the key architecture design questions with a series of examples, discussed in detail with senior Arm staff; capture the architectural intent in operational and axiomatic semantic models, extending previous work on ``user-mode'' concurrency; make these models executable as test oracles for small examples; and experimentally validate them against hardware behaviour (finding a bug in one hardware device). We thereby bring these subtle issues into the mathematical domain, clarifying the architecture and enabling future work on system software verification.
},
topic = {Power_and_ARM},
recent = {true},
elver = {true},
project = {http://www.cl.cam.ac.uk/~pes20/iflat},
pdf = {http://www.cl.cam.ac.uk/~pes20/iflat/top-extended.pdf},
errata = {https://www.cl.cam.ac.uk/~pes20/iflat/}
}
@techreport{UCAM-CL-TR-947,
author = {Watson, Robert N. M. and Richardson, Alexander and Davis,
Brooks and Baldwin, John and Chisnall, David and Clarke,
Jessica and Filardo, Nathaniel and Moore, Simon W. and
Napierala, Edward and Sewell, Peter and Neumann, Peter G.},
title = {{CHERI C/C++ Programming Guide}},
year = 2020,
month = jun,
pdf = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-947.pdf},
institution = {University of Cambridge, Computer Laboratory},
number = {UCAM-CL-TR-947},
abstract = {This document is a brief introduction to the CHERI C/C++ programming languages. We explain the principles underlying these language variants, and their grounding in CHERI’s multiple architectural instantiations: CHERI-MIPS, CHERI-RISC-V, and Arm’s Morello. We describe the most commonly encountered differences between these dialects and C/C++ on conventional architectures, and where existing software may require minor changes. We document new compiler warnings and errors that may be experienced compiling code with the CHERI Clang/LLVM compiler, and suggest how they may be addressed through typically minor source-code changes. We explain how modest language extensions allow selected software, such as memory allocators, to further refine permissions and bounds on pointers. This guidance is based on our experience adapting the FreeBSD operating-system userspace, and applications such as PostgreSQL and WebKit, to run in a CHERI C/C++ capability-based programming environment. We conclude by recommending further reading.},
project = {https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/},
topic = {cheri},
cheriformal = {true},
elver = {true},
recent = {true}
}
@techreport{UCAM-CL-TR-951,
author = {Watson, Robert N. M. and Neumann, Peter G. and Woodruff,
Jonathan and Roe, Michael and Almatary, Hesham and
Anderson, Jonathan and Baldwin, John and Barnes, Graeme and
Chisnall, David and Clarke, Jessica and Davis, Brooks and
Eisen, Lee and Filardo, Nathaniel Wesley and Grisenthwaite,
Richard and Joannou, Alexandre and Laurie, Ben and
Markettos, A. Theodore and Moore, Simon W. and Murdoch,
Steven J. and Nienhuis, Kyndylan and Norton, Robert and
Richardson, Alexander and Rugg, Peter and Sewell, Peter and
Son, Stacey and Xia, Hongyan},
title = {{Capability Hardware Enhanced RISC Instructions: CHERI
Instruction-Set Architecture (Version 8)}},
year = 2020,
month = oct,
pdf = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-951.pdf},
institution = {University of Cambridge, Computer Laboratory},
doi = {10.48456/tr-951},
number = {UCAM-CL-TR-951},
abstract = {This technical report describes CHERI ISAv8, the eighth version of the CHERI architecture being developed by SRI International and the University of Cambridge. This design captures ten years of research, development, experimentation, refinement, formal analysis, and validation through hardware and software implementation.
CHERI introduces an architecture-neutral capability-based protection model, which has been instantiated in various commodity base architectures to give CHERI-MIPS, CHERI-RISC-V, Arm’s prototype Morello architecture, and (sketched) CHERI-x86-64. It enables software to efficiently implement fine-grained memory protection and scalable software compartmentalization, by providing strong, non-probabilistic, efficient mechanisms to support the principles of least privilege and intentional use in the execution of software at multiple levels of abstraction, preventing and mitigating vulnerabilities. Design goals include incremental adoptability from current ISAs and software stacks, low performance overhead for memory protection, significant performance improvements for software compartmentalization, formal grounding, and programmer-friendly underpinnings.
CHERI blends traditional paged virtual memory with an in-address-space capability model that includes capability values in registers, capability instructions, and tagged memory to enforce capability integrity. This hybrid approach, inspired by the Capsicum security model, addresses the performance and robustness issues that arise when trying to express more secure programming models, minimising privilege, above conventional architectures that provide only MMU-based protection. CHERI builds on the C-language fat-pointer literature: its capabilities can describe fine-grained regions of memory, and can be substituted for data or code pointers in generated code, protecting data and improving control-flow robustness. Strong capability integrity and monotonicity properties allow CHERI to express a variety of protection idioms, from enforcing valid C-language pointer provenance and bounds checking to implementing the isolation and controlled communication structures required for software compartmentalization.
CHERI’s hybrid approach allows incremental adoption of capability-oriented design: critical components can be ported and recompiled to use capabilities throughout, providing fine-grain memory protection, or be largely unmodified but encapsulated in ways that permit only controlled interaction. Potential early deployment scenarios include low-level software Trusted Computing Bases (TCBs) such as separation kernels, hypervisors, and operating-system kernels, userspace TCBs such as language runtimes and web browsers, and particularly high-risk software libraries such as data compression, protocol parsing, and image processing (which are concentrations of both complex and historically vulnerability-prone code exposed to untrustworthy data sources).
CHERI ISAv8 is a substantial enhancement to prior ISA versions. Capability compression is now part of the abstract model. Both 32-bit and 64-bit architectural address sizes are supported. Various previously experimental features, such as sentry capabilities and CHERI-RISC-V, are now considered mature. We have defined a number of new temporal memory-safety acceleration features including MMU assistance for a load-side-barrier revocation model. We have added a chapter on practical CHERI microarchitecture. CHERI ISAv8 is synchronized with Arm Morello.
},
project = {https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/},
topic = {cheri},
optcheriformal = {false},
elver = {true},
recent = {true}
}
@inproceedings{isla-cav,
optkey = {},
author = {Alasdair Armstrong and Brian Campbell and Ben Simner and Christopher Pulte and Peter Sewell},
title = {Isla: Integrating full-scale {ISA} semantics and axiomatic concurrency models},
conf = {CAV 2021},
booktitle = {Proc. 33rd International Conference on Computer-Aided Verification},
month = jul,
year = {2021},
opteditor = {Alexandra Silva and K. Rustan M. Leino},
opttitle = {Isla: Integrating Full-Scale {ISA} Semantics and Axiomatic Concurrency
Models},
optbooktitle = {Computer Aided Verification - 33rd International Conference, {CAV}
2021, Virtual Event, July 20-23, 2021, Proceedings, Part {I}},
series = {Lecture Notes in Computer Science},
volume = {12759},
pages = {303--316},
publisher = {Springer},
optyear = {2021},
url = {https://doi.org/10.1007/978-3-030-81685-8\_14},
doi = {10.1007/978-3-030-81685-8\_14},
timestamp = {Fri, 23 Jul 2021 16:41:31 +0200},
biburl = {https://dblp.org/rec/conf/cav/ArmstrongCSPS21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org},
optpdf = {https://www.cl.cam.ac.uk/~pes20/isla/isla-cav2021.pdf},
optnote = {Extended version available at \url{https://www.cl.cam.ac.uk/~pes20/isla/isla-cav2021-extended.pdf}},
pdf = {https://www.cl.cam.ac.uk/~pes20/isla/isla-cav2021-extended.pdf},
elver = {true},
abstract = {
Architecture specifications such as Armv8-A and RISC-V are the ultimate foundation for software verification and the correctness criteria for hardware verification. They should define the allowed sequential and relaxed-memory concurrency behaviour of programs, but hitherto there has been no integration of full-scale instruction-set architecture (ISA) semantics with axiomatic concurrency models, either in mathematics or in tools. These ISA semantics can be surprisingly large and intricate, e.g.~100k+ lines for Armv8-A.
In this paper we present a tool, Isla, for computing the allowed behaviours of concurrent litmus tests with respect to full-scale ISA definitions, in Sail, and arbitrary axiomatic relaxed-memory concurrency models, in the Cat language. It is based on a generic symbolic engine for Sail ISA specifications, which should be valuable also for other verification tasks. We equip the tool with a web interface to make it widely accessible, and illustrate and evaluate it for Armv8-A and RISC-V.
By using full-scale and authoritative ISA semantics, this lets one evaluate litmus tests using arbitrary user instructions with high confidence. Moreover, because these ISA specifications give detailed and validated definitions of the sequential aspects of \emph{systems} functionality, as used by hypervisors and operating systems, e.g.~instruction fetch, exceptions, and address translation, our tool provides a basis for developing concurrency semantics for these. We demonstrate this for the Armv8-A instruction-fetch model and self-modifying code examples of Simner et al.
},
optannote = {},
topic = {Power_and_ARM},
topictwo = {ISA_semantics},
recent = {true}
}
@article{isla-cav-fmsd,
optkey = {},
author = {Alasdair Armstrong and Brian Campbell and Ben Simner and Christopher Pulte and Peter Sewell},
title = {Isla: Integrating full-scale {ISA} semantics and axiomatic concurrency models (extended version)},
journal = {Formal Methods in System Design},
month = may,
year = {2023},
optpages = {303--316},
publisher = {Springer},
optissn = {1572-8102},
optyear = {2021},
url = {https://doi.org/10.1007/s10703-023-00409-y},
doi = {10.1007/s10703-023-00409-y},
pdf = {https://link.springer.com/content/pdf/10.1007/s10703-023-00409-y.pdf},
elver = {true},
abstract = {
Architecture specifications such as Armv8-A and RISC-V are the ultimate foundation for software verification and the correctness criteria for hardware verification. They should define the allowed sequential and relaxed-memory concurrency behaviour of programs, but hitherto there has been no integration of full-scale instruction-set architecture (ISA) semantics with axiomatic concurrency models, either in mathematics or in tools. These ISA semantics can be surprisingly large and intricate, e.g. 100k+ lines for Armv8-A. In this paper we present a tool, Isla, for computing the allowed behaviours of concurrent litmus tests with respect to full-scale ISA definitions, in the Sail language, and arbitrary axiomatic relaxed-memory concurrency models, in the Cat language. It is based on a generic symbolic engine for Sail ISA specifications. We equip the tool with a web interface to make it widely accessible, and illustrate and evaluate it for Armv8-A and RISC-V. The symbolic execution engine is valuable also for other verification tasks: it has been used in automated ISA test generation for the Arm Morello prototype architecture, extending Armv8-A with CHERI capabilities, and for Iris program-logic reasoning about binary code above the Armv8-A and RISC-V ISA specifications. By using full-scale and authoritative ISA semantics, Isla lets one evaluate litmus tests using arbitrary user instructions with high confidence. Moreover, because these ISA specifications give detailed and validated definitions of the sequential aspects of systems functionality, as used by hypervisors and operating systems, e.g. instruction fetch, exceptions, and address translation, our tool provides a basis for developing concurrency semantics for these. We demonstrate this for the Armv8-A instruction-fetch and virtual-memory models and examples of Simner et al.
},
optannote = {},
topic = {Power_and_ARM},
topictwo = {ISA_semantics},
recent = {true}
}
@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}
}
@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}
}
@miscs{relaxedVM-arxiv,
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} (extended version)},
optcrossref = {},
optkey = {},
optconf = {ESOP 2022},
optbooktitle = {Proceedings of the 31st European Symposium on Programming},
year = {2022},
optbooktitle = {},
optyear = {},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optpages = {},
month = mar,
optaddress = {},
optorganization = {},
optpublisher = {},
note = {\url{http://arxiv.org/abs/2203.00642}},
optannote = {},
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 \mbox{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.
This document is an extended version of a paper in ESOP 2022, with additional explanation and examples in the main body, and appendices detailing our litmus tests, models, proofs, and test results.
},
pdf = {https://arxiv.org/pdf/2203.00642},
topic = {Power_and_ARM},
project = {http://www.cl.cam.ac.uk/~pes20/RelaxedVM-Arm},
recent = {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},
year = {2022},
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}
}
@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},
optnote = {Proc. ACM Program. Lang. 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 = {Cerberus},
project = {https://www.cl.cam.ac.uk/~cp526/popl23.html},
elver = {true},
recent = {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},
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 = {},
optbooktitle = {},
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{$^*$} and Zongyuan Liu{$^*$} 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 = {${}^*$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}
}