ELVER: Engineering with Logic and Verification: Mathematically Rigorous Engineering for Safe and Secure Computer Systems
ELVER is an ERC Advanced Grant (AdG) led by
Peter Sewell at the
University of Cambridge Computer
Laboratory, from 2018-10 to 2024-09.
Abstract
Computer systems have become critical to modern society, but they are
pervasively subject to security flaws and malicious attacks, with
large-scale exposures of confidential data, denial-of-service and
ransom attacks, and the threat of nation-state attackers: they are
trusted, but are far from trustworthy. This is especially important
for the major pan-industry components of our information
infrastructure: processors, programming languages, operating systems,
etc.
The basic problem is that conventional engineering techniques suffice
only to make systems that usually work. The usual test-and-debug
development methods, with poorly specified abstractions described in
prose, lack the mathematical rigour of other engineering disciplines -
yet the huge investment in legacy systems and skills makes it hard to
improve.
ELVER will develop mathematically rigorous methods for specifying,
testing, and reasoning about real systems, focussed on the core
mechanisms used by hardware and software to enforce security
boundaries. It will establish mathematical models for the industry ARM
architecture, used pervasively in mobile phones and embedded devices,
and the CHERI research architecture, which protects against many
attacks. Using these, ELVER will build tools for analysis of system
software, develop techniques for mathematical proof of safety and
security properties, and explore improved systems programming
languages. ELVER will build on successful collaborations with ARM,
IBM, and the C/C++ ISO standards committees. It will directly impact
mainstream processor architectures, languages, and development
methods, smoothly complementing existing methods while simultaneously
enabling longer-term research towards the gold standard of provably
secure systems.
ELVER will thus demonstrate the feasibility and benefits of a more
rigorous approach to system engineering, putting future systems on
more solid foundations, and hence making them safer and more secure
Team
Funding
This project has received funding from the European Research Council
(ERC) under the European Union's Horizon 2020 research and innovation programme (grant agreement No 789108).
Papers
-
Towards general white-box automation: a typeclass-guided
context cleaner.
Thibaut Pérami.
In CoqPL 2025.
[ bib |
http ]
-
A CHERI C Memory Model for Verified Temporal
Safety.
Vadim Zaliva, Kayvan Memarian, Brian Campbell, Ricardo Almeida,
Nathaniel Wesley Filardo, Ian Stark, and Peter Sewell.
In CPP 2025.
[ bib |
doi |
http ]
-
Fulminate: Testing CN Separation-Logic Specifications in
C.
Rini Banerjee, Kayvan Memarian, Dhruv Makwana, Christopher Pulte,
Neel Krishnaswami, and Peter Sewell.
In POPL 2025.
[ bib |
doi |
pdf |
abstract ]
-
Formal Mechanised Semantics of CHERI C: Capabilities,
Provenance, and Undefined Behaviour.
Vadim Zaliva, Kayvan Memarian, Ricardo Almeida, Jessica Clarke,
Brooks Davis, Alex Richardson, David Chisnall, Brian Campbell, Ian Stark,
Robert N. M. Watson, and Peter Sewell.
In ASPLOS 2024.
[ bib |
pdf |
abstract ]
-
Relaxed exception semantics for Arm-A (extended
version), Ben Simner, Alasdair Armstrong, Thomas Bauereiss,
Brian Campbell, Ohad Kammar, Jean Pichon-Pharabod, and Peter Sewell, 2024.
[ bib |
arXiv |
http ]
-
An axiomatic basis for computer programming on the relaxed
Arm-A architecture: the AxSL logic.
Angus Hammond1, Zongyuan Liu1, Thibaut Pérami, Peter
Sewell, Lars Birkedal, and Jean Pichon-Pharabod.
In POPL 2024, 1These authors contributed equally. Proc. ACM
Program. Lang. 8, POPL, Article 21.
[ bib |
doi |
pdf |
abstract ]
-
The Cerberus C semantics.
Kayvan Memarian.
Technical Report UCAM-CL-TR-981, University of Cambridge, Computer
Laboratory, May 2023.
PhD thesis.
[ bib |
doi |
.pdf |
abstract ]
-
Isla: Integrating full-scale ISA semantics and axiomatic
concurrency models (extended version).
Alasdair Armstrong, Brian Campbell, Ben Simner, Christopher Pulte,
and Peter Sewell.
Formal Methods in System Design, May 2023.
[ bib |
doi |
pdf |
http |
abstract ]
-
The Arm Morello Evaluation Platform---Validating
CHERI-Based Security in a High-Performance System.
Richard Grisenthwaite, Graeme Barnes, Robert N. M. Watson, Simon W.
Moore, Peter Sewell, and Jonathan Woodruff.
IEEE Micro, 43(3):50--57, 2023.
[ bib |
doi |
pdf |
http |
abstract ]
-
Improving Security with Hardware Support: CHERI and Arm's
Morello.
Robert N. M. Watson, Peter Sewell, and William Martin.
The Next Wave (The National Security Agency's review of emerging
technologies), 4(1):10--21, 2023.
ISSN 2640-1789 (print), ISSN 2640-1797 (online).
[ bib |
project page |
pdf |
abstract ]
-
CN: Verifying systems C code with separation-logic
refinement types.
Christopher Pulte, Dhruv C. Makwana, Thomas Sewell, Kayvan Memarian,
Peter Sewell, and Neel Krishnaswami.
In POPL 2023, Proc. ACM Programming Languages 7, POPL, Article 1.
[ bib |
doi |
project page |
pdf |
abstract ]
-
Formal CHERI: rigorous engineering and design-time proof of
full-scale architecture security properties, Peter Sewell,
Thomas Bauereiss, Brian Campbell, and Robert N. M. Watson.
Blog post,
https://www.lightbluetouchpaper.org/2022/07/22/formal-cheri/, July
2022.
[ bib |
project page |
http ]
-
Islaris: Verification of Machine Code Against Authoritative
ISA Semantics.
Michael Sammler, Angus Hammond, Rodolphe Lepigre, Brian Campbell,
Jean Pichon-Pharabod, Derek Dreyer, Deepak Garg, and Peter Sewell.
In PLDI 2022.
[ bib |
doi |
project page |
pdf |
abstract ]
-
N3005: A Provenance-aware Memory Object Model for C. Working
Draft Technical Specification ISO/IEC TS 6010:2023 (E),
Jens Gustedt, Peter Sewell, Kayvan Memarian, Victor B. F. Gomes, and Martin
Uecker.
ISO/IEC JTC1/SC22/WG14 N3005
http://www.open-std.org/jtc1/sc22/wg14/www/docs/n3005.pdf, June 2022.
[ bib |
pdf |
abstract ]
-
Verified Security for the Morello Capability-enhanced
Prototype Arm Architecture.
Thomas Bauereiss, Brian Campbell, Thomas Sewell, Alasdair Armstrong,
Lawrence Esswood, Ian Stark, Graeme Barnes, Robert N. M. Watson, and Peter
Sewell.
In ESOP 2022.
[ bib |
doi |
project page |
pdf |
http |
abstract ]
-
Relaxed virtual memory in Armv8-A.
Ben Simner, Alasdair Armstrong, Jean Pichon-Pharabod, Christopher
Pulte, Richard Grisenthwaite, and Peter Sewell.
In ESOP 2022.
[ bib |
doi |
project page |
pdf |
http |
abstract ]
-
VIP: Verifying Real-World C Idioms with Integer-Pointer
Casts.
Rodolphe Lepigre, Michael Sammler, Kayvan Memarian, Robbert Krebbers,
Derek Dreyer, and Peter Sewell.
In POPL 2022, Proc. ACM Program. Lang. 6, POPL, Article 20.
[ bib |
doi |
supplementary material |
project page |
pdf |
abstract ]
-
Verified security for the Morello capability-enhanced
prototype Arm architecture.
Thomas Bauereiss, Brian Campbell, Thomas Sewell, Alasdair Armstrong,
Lawrence Esswood, Ian Stark, Graeme Barnes, Robert N. M. Watson, and Peter
Sewell.
Technical Report UCAM-CL-TR-959, University of Cambridge, Computer
Laboratory, September 2021.
[ bib |
project page |
pdf |
abstract ]
-
Isla: Integrating full-scale ISA semantics and axiomatic
concurrency models.
Alasdair Armstrong, Brian Campbell, Ben Simner, Christopher Pulte,
and Peter Sewell.
In CAV 2021.
[ bib |
doi |
pdf |
http |
abstract ]
-
N2676: A Provenance-aware Memory Object Model for C. Working
Draft Technical Specification, Jens Gustedt, Peter Sewell,
Kayvan Memarian, Victor B. F. Gomes, and Martin Uecker.
ISO/IEC JTC1/SC22/WG14 N2676
http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2676.pdf, March 2021.
[ bib |
pdf |
abstract ]
-
Two Mechanisations of WebAssembly 1.0.
Conrad Watt, Xiaojia Rao, Jean Pichon-Pharabod, Martin Bodin, and
Philippa Gardner.
In FM 2021.
[ bib |
doi |
http |
abstract ]
-
RefinedC: Automating the Foundational Verification of C Code
with Refined Ownership Types.
Michael Sammler, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian,
Derek Dreyer, and Deepak Garg.
In PLDI 2021.
[ bib |
pdf |
abstract ]
-
Capability Hardware Enhanced RISC Instructions: CHERI
Instruction-Set Architecture (Version 8).
Robert N. M. Watson, Peter G. Neumann, Jonathan Woodruff, Michael
Roe, Hesham Almatary, Jonathan Anderson, John Baldwin, Graeme Barnes, David
Chisnall, Jessica Clarke, Brooks Davis, Lee Eisen, Nathaniel Wesley Filardo,
Richard Grisenthwaite, Alexandre Joannou, Ben Laurie, A. Theodore Markettos,
Simon W. Moore, Steven J. Murdoch, Kyndylan Nienhuis, Robert Norton,
Alexander Richardson, Peter Rugg, Peter Sewell, Stacey Son, and Hongyan Xia.
Technical Report UCAM-CL-TR-951, University of Cambridge, Computer
Laboratory, October 2020.
[ bib |
doi |
project page |
pdf |
abstract ]
-
N2577: A Provenance-aware Memory Object Model for C. Working
Draft Technical Specification, Jens Gustedt, Peter Sewell,
Kayvan Memarian, Victor B. F. Gomes, and Martin Uecker.
ISO/IEC JTC1/SC22/WG14 N2577
http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2577.pdf, September
2020.
[ bib |
pdf |
abstract ]
-
CHERI C/C++ Programming Guide.
Robert N. M. Watson, Alexander Richardson, Brooks Davis, John
Baldwin, David Chisnall, Jessica Clarke, Nathaniel Filardo, Simon W. Moore,
Edward Napierala, Peter Sewell, and Peter G. Neumann.
Technical Report UCAM-CL-TR-947, University of Cambridge, Computer
Laboratory, June 2020.
[ bib |
project page |
pdf |
abstract ]
-
Cornucopia: Temporal Safety for CHERI Heaps.
Nathaniel Wesley Filardo, Brett F. Gutstein, Jonathan Woodruff, Sam
Ainsworth, Lucian Paul-Trifu, Brooks Davis, Hongyan Xia, Edward Tomasz
Napierala, Alexander Richardson, John Baldwin, David Chisnall, Jessica
Clarke, Khilan Gudka, Alexandre Joannou, A. Theodore Markettos, Alfredo
Mazzinghi, Robert M. Norton, Michael Roe, Peter Sewell, Stacey Son,
Timothy M. Jones, Simon W. Moore, Peter G. Neumann, and Robert N. M. Watson.
In Security and Privacy 2020.
[ bib |
doi |
project page |
pdf |
abstract ]
-
Rigorous engineering for hardware security: Formal modelling
and proof in the CHERI design and implementation process.
Kyndylan Nienhuis, Alexandre Joannou, Thomas Bauereiss, Anthony Fox,
Michael Roe, Brian Campbell, Matthew Naylor, Robert M. Norton, Simon W.
Moore, Peter G. Neumann, Ian Stark, Robert N. M. Watson, and Peter Sewell.
In Security and Privacy 2020.
[ bib |
doi |
project page |
pdf |
abstract ]
-
ARMv8-A system semantics: instruction fetch in relaxed
architectures.
Ben Simner, Shaked Flur, Christopher Pulte, Alasdair Armstrong, Jean
Pichon-Pharabod, Luc Maranget, and Peter Sewell.
In ESOP 2020.
[ bib |
project page |
errata |
pdf |
abstract ]
-
Repairing and mechanising the JavaScript relaxed memory
model.
Conrad Watt, Christopher Pulte, Anton Podkopaev, Guillaume Barbier,
Stephen Dolan, Shaked Flur, Jean Pichon-Pharabod, and Shu-yu Guo.
In PLDI 2020.
[ bib |
doi |
http |
abstract ]
-
An Introduction to CHERI.
Robert N. M. Watson, Simon W. Moore, Peter Sewell, and Peter Neumann.
Technical Report UCAM-CL-TR-941, University of Cambridge, Computer
Laboratory, September 2019.
[ bib |
project page |
pdf |
abstract ]
-
Cerberus-BMC: a Principled Reference Semantics and
Exploration Tool for Concurrent and Sequential C.
Stella Lau, Victor B. F. Gomes, Kayvan Memarian, Jean
Pichon-Pharabod, and Peter Sewell.
In CAV 2019.
[ bib |
project page |
pdf |
abstract ]
-
Capability Hardware Enhanced RISC Instructions: CHERI
Instruction-Set Architecture (Version 7).
Robert N. M. Watson, Peter G. Neumann, Jonathan Woodruff, Michael
Roe, Hesham Almatary, Jonathan Anderson, John Baldwin, David Chisnall, Brooks
Davis, Nathaniel Wesley Filardo, Alexandre Joannou, Ben Laurie, A. Theodore
Markettos, Simon W. Moore, Steven J. Murdoch, Kyndylan Nienhuis, Robert
Norton, Alex Richardson, Peter Rugg, Peter Sewell, Stacey Son, and Hongyan
Xia.
Technical Report UCAM-CL-TR-927, University of Cambridge, Computer
Laboratory, June 2019.
496pp.
[ bib |
pdf |
abstract ]
-
CheriABI: Enforcing Valid Pointer Provenance and Minimizing
Pointer Privilege in the POSIX C Run-time Environment.
Brooks Davis, Robert N. M. Watson, Alexander Richardson, Peter G.
Neumann, Simon W. Moore, John Baldwin, David Chisnall, James Clarke,
Nathaniel Wesley Filardo, Khilan Gudka, Alexandre Joannou, Ben Laurie,
A. Theodore Markettos, J. Edward Maste, Alfredo Mazzinghi, Edward Tomasz
Napierala, Robert M. Norton, Michael Roe, Peter Sewell, Stacey Son, and
Jonathan Woodruff.
In ASPLOS 2019, Best paper award.
[ bib |
doi |
project page |
pdf |
http |
abstract ]
-
ISA Semantics for ARMv8-A, RISC-V, and
CHERI-MIPS.
Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Alastair Reid,
Kathryn E. Gray, Robert M. Norton, Prashanth Mundkur, Mark Wassell, Jon
French, Christopher Pulte, Shaked Flur, Ian Stark, Neel Krishnaswami, and
Peter Sewell.
In POPL 2019, Proc. ACM Program. Lang. 3, POPL, Article 71.
[ bib |
doi |
supplementary material |
project page |
pdf |
abstract ]
-
Exploring C Semantics and Pointer Provenance.
Kayvan Memarian, Victor B. F. Gomes, Brooks Davis, Stephen Kell,
Alexander Richardson, Robert N. M. Watson, and Peter Sewell.
In POPL 2019, Proc. ACM Program. Lang. 3, POPL, Article 67. Also
available as ISO/IEC JTC1/SC22/WG14 N2311.
[ bib |
doi |
supplementary material |
project page |
pdf |
abstract ]
Software
-
Sail Morello (CHERI Arm) instruction-set architecture (ISA)
model, Arm Limited, Thomas Bauereiss, Brian Campbell,
Alasdair Armstrong, Alastair Reid, and Peter Sewell, 2022.
[ bib |
project page |
github ]
-
Cerberus-BMC tool for exploring the behaviour of small
concurrent C test programs with respect to an arbitrary axiomatic
concurrency model, Stella Lau, Kayvan Memarian, Victor B. F.
Gomes, Kyndylan Nienhuis, Justus Matthiesen, James Lingard, and Peter Sewell,
2019.
[web interface].
[ bib |
project page |
github ]
-
The Ott tool for writing definitions of programming languages
and calculi, Peter Sewell, Francesco Zappa Nardelli, Scott
Owens, Joey Eremondi, Hannes Mehnert, Karl Palmskog, Thibaut Perami, Matthew
Parkinson, Hannes Mehnert, kit-ty kate, Brian Campbell, Francois Pottier,
Gilles Peskine, Alastair Reid, Tom Ridge, Susmit Sarkar, Rok Strniša,
and Viktor Vafeiadis, 2005--2024.
[ bib |
project page |
github ]
-
Linksem: Executable semantic model for aspects of ELF linking
and DWARF debug information, Dominic Mulligan, Stephen
Kell, Simon Ser, Peter Sewell, Shaked Flur, Thibaut Pérami, Robert
Norton, Ramana Kumar, Jonathan French, and Thomas Bauereiss, 2014--2024.
[ bib |
github ]
-
CN C verification and testing tool, Christopher
Pulte, Dhruv C. Makwana, Thomas Sewell, Kayvan Memarian, Rini Banerjee, Peter
Sewell, and Neel Krishnaswami, 2023--.
[ bib |
github ]
-
Cerberus C executable semantics and exploration
tool, Kayvan Memarian, Victor B. F. Gomes, Justus Matthiesen,
Peter Sewell, Kyndylan Nienhuis, Stella Lau, Jean Pichon-Pharabod,
Christopher Pulte, Rodolphe Lepigre, James Lingard, Thomas Sewell, and Dhruv
Makwana, 2016--2024.
[web interface].
[ bib |
project page |
github ]
-
RMEM: Executable operational concurrency model exploration
tool for ARMv8, RISC-V, Power, and x86, Susmit
Sarkar, Peter Sewell, Luc Maranget, Shaked Flur, Christopher Pulte, Jon
French, Ben Simner, Scott Owens, Pankaj Pawan, Francesco Zappa Nardelli, Sela
Mador-Haim, Dominic Mulligan, Ohad Kammar, Jean Pichon-Pharabod, Gabriel
Kerneis, Alasdair Armstrong, Thomas Bauereiss, and Jeehoon Kang, 2010--2024.
[web interface].
[ bib |
github ]
-
Sail CHERI-RISC-V instruction-set architecture (ISA)
model, Alasdair Armstrong, Thomas Bauereiss, Brian Campbell,
Jessica Clarke, Nathaniel Wesley Filardo, Google, Alexandre Joannou,
Microsoft, Prashanth Mundkur, Robert Norton-Wright, Alexander Richardson,
Peter Rugg, and Peter Sewell, 2019--2024.
[ bib |
project page |
github ]
-
Sail RISC-V instruction-set architecture (ISA)
model, ahadali5000, Alasdair Armstrong, Alexander Richardson,
Aril Computer Corp. (for contributions by Scott Johnson), Ben Marshall,
Bicheng Yang, Bilal Sakhawat, Brian Campbell, Chris Casinghino, Christopher
Pulte, Martin Berger Codasip (for contributions by Tim Hutt, Ben Fletcher),
dylux, eroom1966, Google LLC (for contributions by its employees), Hesham
Almatary, Jan Henrik Weinstock, Jessica Clarke, Jon French, Martin Berger,
Michael Sammler, Microsoft (for contributions by Robert Norton-Wright,
Nathaniel Wesley Filardo), Muhammad Bilal Sakhawat, Nathaniel Wesley Filardo,
Paul A. Clarke, Peter Rugg, Peter Sewell, Philipp Tomsich, Prashanth Mundkur,
Rafael Sene, Rishiyur S. Nikhil (Bluespec, Inc.), Robert Norton-Wright,
Shaked Flur, Thibaut Pérami, Thomas Bauereiss, VRULL GmbH (for contributions
by its employees), William McSpaddden, and Xinlai Wan, 2014--2024.
[ bib |
project page |
github ]
-
Sail Armv9.4-A, Armv9.3-A and ARMv8.5-A instruction-set
architecture (ISA) models, Thomas Bauereiss, Brian
Campbell, Alasdair Armstrong, Alastair Reid, Kathryn E. Gray, Anthony Fox,
Peter Sewell, and Arm Limited, 2019, 2022, 2024.
[ bib |
project page |
github ]
-
The Isla symbolic evaluation engine for Sail and
Isla-axiomatic exploration tool for axiomatic concurrency
models, Alasdair Armstrong, Brian Campbell, Thibaut
Pérami, Ben Simner, Peter Sewellb, and Dhruv Makwana, 2019--2024.
[web interface].
[ bib |
project page |
github ]
-
The Sail Instruction-Set Architecture (ISA) specification
language, Alasdair Armstrong, Thomas Bauereiss, Brian
Campbell, Shaked Flur, Jon French, Kathryn E. Gray, Stephen Kell, Gabriel
Kerneis, Neel Krishnaswami, Prashanth Mundkur, Robert Norton-Wright,
Christopher Pulte, Alastair Reid, Peter Sewell, Ian Stark, and Mark Wassell,
2013--2024.
[ bib |
project page |
github ]
[Validate this page.]