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 Cambrige Computer
Laboratory, from 2018-10 to 2024-03.
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
Papers
-
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.
[ 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 ]
-
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 ]
-
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 |
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 |
doi |
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--2022.
[ 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--2022.
[ 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--2022.
[web interface].
[ bib |
project page |
github ]
-
RMEM: Executable operational concurrency model exploration
tool for ARMv8, RISC-V, Power, and x86, Peter Sewell,
Shaked Flur, Christopher Pulte, Susmit Sarkar, Jon French, Kathryn E. Gray,
Luc Maranget, Robert Norton-Wright, Pankaj Pawan, Stephen Kell, Ohad Kammar,
Sela Mador-Haim, Linden Ralph, Francesco Zappa Nardelli, Gabriel Kerneis,
Jean Pichon-Pharabod, Kyndylan Nienhuis, Ali Sezgin, Dominic Mulligan, Victor
Gomes, Mark Batty, Richard Bornat, Kayvan Memarian, Anthony Fox, and Alasdair
Armstrong, 2010--2022.
[web interface].
[ bib |
github ]
-
Sail CHERI-RISC-V instruction-set architecture (ISA)
model, Alasdair Armstrong, Thomas Bauereiss, Brian Campbell,
Jessica Clarke, Nathaniel Wesley Filardo, Alexandre Joannou, Prashanth
Mundkur, Robert Norton-Wright, Alexander Richardson, Peter Rugg, and Peter
Sewell, 2019--2022.
[ bib |
project page |
github ]
-
Sail RISC-V instruction-set architecture (ISA)
model, Prashanth Mundkur, Rishiyur S. Nikhil, Jon French,
Brian Campbell, Robert Norton-Wright, Alasdair Armstrong, Thomas Bauereiss,
Shaked Flur, Christopher Pulte, Peter Sewell, Alexander Richardson, Hesham
Almatary, Jessica Clarke, Nathaniel Wesley Filardo, Peter Rugg, and Scott
Johnson, 2014--2022.
[ bib |
project page |
github ]
-
Sail 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.
[ 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 Sewell, and Dhruv Makwana, 2019--2022.
[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--2022.
[ bib |
project page |
github ]
[Validate this page.]