recent.bib

@comment{{This file has been generated by bib2bib 1.99}}

@comment{{Command line: bibtex2html-1.99/bib2bib -c recent:"true" -ob recent.bib sewellbib2.bib}}

@inproceedings{Cerberus-PLDI16,
  author = {
Kayvan Memarian and 
Justus Matthiesen and 
James Lingard and
Kyndylan Nienhuis and
David Chisnall and
Robert N.M. Watson and
Peter Sewell
},
  title = {Into the depths of {C}: elaborating the de facto standards},
  abstract = {
C remains central to our computing infrastructure.  It is notionally defined by ISO standards, but in reality the properties of C assumed by systems code and those implemented by compilers have diverged, both from the ISO standards and from each other, and none of these are clearly understood.

We make two contributions to help improve this error-prone situation.  First, we describe an in-depth analysis of the design space for the semantics of pointers and memory in C as it is used in practice.  We articulate many specific questions, build a suite of semantic test cases, gather experimental data from multiple implementations, and survey what C experts believe about the de facto standards.  We identify questions where there is a consensus (either following ISO or differing) and where there are conflicts. We apply all this to an experimental C implemented above capability hardware.  Second, we describe a formal model, Cerberus, for large parts of C.  Cerberus is parameterised on its memory model; it is linkable either with a candidate de facto memory object model, under construction, or with an operational C11 concurrency model; it is defined by elaboration to a much simpler Core language for accessibility, and it is executable as a test oracle on small examples.

This should provide a solid basis for discussion of what mainstream C is now: what programmers and analysis tools can assume and what compilers aim to implement. Ultimately we hope it will be a step towards clear, consistent, and accepted semantics for the various use-cases of C.
},
  optcrossref = {},
  optkey = {},
  conf = {PLDI 2016},
  booktitle = {Proceedings of the 37th ACM SIGPLAN conference on Programming Language Design and Implementation},
  optpages = {},
  year = {2016},
  opteditor = {},
  optvolume = {},
  optnumber = {},
  optseries = {},
  optaddress = {},
  month = jun,
  optorganization = {},
  optpublisher = {},
  note = {PLDI 2016 Distinguished Paper award},
  project = {http://www.cl.cam.ac.uk/~pes20/cerberus},
  url = {http://doi.acm.org/10.1145/2908080.2908081},
  doi = {10.1145/2908080.2908081},
  pdf = {http://www.cl.cam.ac.uk/users/pes20/cerberus/pldi16.pdf},
  optannote = {},
  topic = {Cerberus},
  topictwo = {cheri},
  topicthree = {WG14},
  cheriformal = {true},
  recent = {true}
}

@inproceedings{kell_missing_2016,
  author = {Stephen Kell and Dominic P. Mulligan and Peter Sewell},
  title = {The missing link: explaining {ELF} static linking, semantically},
  conf = {OOPSLA 2016},
  booktitle = {Proceedings of the ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications},
  series = {OOPSLA 2016},
  year = {2016},
  month = nov,
  location = {Amsterdam, The Netherlands},
  numpages = {17},
  publisher = {ACM},
  address = {New York, NY, USA},
  keywords = {Linking, formal specification, Executable and Linkable Format (ELF), theorem-proving},
  abstract = {Beneath the surface, software usually depends on complex \emph{linker
  behaviour} to work as intended.  Even linking
\texttt{hello\_world.c} is surprisingly involved, and systems software
such as \texttt{libc} and operating system kernels rely on a host of
linker features.  But linking is poorly understood by working
programmers and has largely been neglected by language researchers.

In this paper we survey the many use-cases that linkers support and
the poorly specified \emph{linker speak} by which they are controlled:
metadata in object files, command-line options, and linker-script
language.  We provide the first validated formalisation of a realistic
executable and linkable format (ELF), and capture aspects of the
Application Binary Interfaces for four mainstream platforms (AArch64,
AMD64, Power64, and IA32).  Using these, we develop an executable
specification of static linking, covering (among other things) enough to link
small C programs (we use the example of \textsf{bzip2}) into a correctly
running executable.  We
provide our specification in Lem and Isabelle/HOL forms.  This is the
first formal specification of mainstream linking.  We have used the
Isabelle/HOL version to prove a sample
correctness property for one case of AMD64 ABI relocation,
demonstrating that the specification supports formal proof, and as a
first step towards the much more ambitious goal of verified linking.
Our work should enable several novel strands of research, including
linker-aware verified compilation and program analysis, and better
languages for controlling linking.
},
  url = {http://doi.acm.org/10.1145/2983990.2983996},
  doi = {10.1145/2983990.2983996},
  pdf = {http://www.cl.cam.ac.uk/~pes20/rems/papers/oopsla-elf-linking-2016.pdf},
  project = {https://github.com/rems-project/linksem},
  topic = {linksem},
  recent = {true}
}

@inproceedings{operational-semantics-c11-2016,
  author = {Kyndylan Nienhuis and Kayvan Memarian and Peter Sewell},
  title = {An operational semantics for {C/C++11} concurrency},
  conf = {OOPSLA 2016},
  booktitle = {Proceedings of the ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications},
  location = {Amsterdam, The Netherlands},
  numpages = {18},
  publisher = {ACM},
  address = {New York, NY, USA},
  month = nov,
  year = {2016},
  abstract = {The C/C++11 concurrency model balances two goals: it is relaxed enough to be efficiently implementable and (leaving aside the ``thin-air'' problem) it is strong enough to give useful guarantees to programmers. It is mathematically precise and has been used in verification research and compiler testing. However, the model is expressed in an axiomatic style, as predicates on complete candidate executions. This suffices for computing the set of allowed executions of a small litmus test, but it does not directly support the incremental construction of executions of larger programs. It is also at odds with conventional operational semantics, as used implicitly in the rest of the C/C++ standards.

Our main contribution is the development of an operational model for C/C++11 concurrency. This covers all the features of the previous formalised axiomatic model, and we have a mechanised proof that the two are equivalent, in Isabelle/HOL. We also integrate this semantics with an operational semantics for sequential C (described elsewhere); the combined semantics can incrementally execute programs in a small fragment of C.

Doing this uncovered several new aspects of the C/C++11 model: we show that one cannot build an equivalent operational model that simply follows program order, sequential consistent order, or the synchronises-with order. The first negative result is forced by hardware-observable behaviour, but the latter two are not, and so might be ameliorated by changing C/C++11. More generally, we hope that this work, with its focus on incremental construction of executions, will inform the future design of new concurrency models.},
  url = {http://doi.acm.org/10.1145/2983990.2983997},
  doi = {10.1145/2983990.2983997},
  pdf = {http://www.cl.cam.ac.uk/~pes20/rems/papers/nienhuis-oopsla-2016.pdf},
  topic = {c11},
  recent = {true}
}

@inproceedings{mixed17,
  author = {Shaked Flur and Susmit Sarkar and Christopher Pulte and Kyndylan Nienhuis and Luc Maranget and Kathryn E. Gray and Ali Sezgin and Mark Batty and Peter Sewell},
  title = {Mixed-size Concurrency: {ARM}, {POWER}, {C/C++11}, and {SC}},
  conf = {POPL 2017},
  booktitle = {Proceedings of the 44th {ACM} {SIGPLAN-SIGACT} Symposium on Principles of
               Programming Languages (Paris)},
  year = {2017},
  month = jan,
  pages = {429--442},
  numpages = {14},
  opturl = {http://doi.acm.org/10.1145/3009837.3009839},
  doi = {10.1145/3009837.3009839},
  project = {http://www.cl.cam.ac.uk/users/pes20/popl17/},
  abstract = {Previous work on the semantics of relaxed shared-memory concurrency has only considered the case in which each load reads the data of exactly one store.  In practice, however, multiprocessors support mixed-size accesses, and these are used by systems software and (to some degree) exposed at the C/C++ language level.  A semantic foundation for software, therefore, has to address them.


We investigate the mixed-size behaviour of ARMv8 and IBM POWER architectures and implementations: by experiment, by developing semantic models, by testing the correspondence between these, and by discussion with ARM and IBM staff.  This turns out to be surprisingly subtle, and on the way we have to revisit the fundamental concepts of coherence and sequential consistency, which change in this setting.  In particular, we show that adding a memory barrier between each instruction does not restore sequential consistency.  We go on to extend the C/C++11 model to support non-atomic mixed-size memory accesses.


This is a necessary step towards semantics for real-world shared-memory concurrent code, beyond litmus tests.
},
  pdf = {http://www.cl.cam.ac.uk/~pes20/popl17/mixed-size.pdf},
  topic = {Power_and_ARM},
  topictwo = {ISA_semantics},
  recent = {true}
}

@inproceedings{armv8-mca,
  author = {Christopher Pulte and Shaked Flur and Will Deacon and Jon French and Susmit Sarkar and Peter Sewell},
  title = {{Simplifying ARM Concurrency: Multicopy-atomic Axiomatic and Operational Models for ARMv8}},
  optcrossref = {},
  optkey = {},
  conf = {POPL 2018},
  booktitle = {Proceedings of the 45th ACM SIGPLAN Symposium on Principles of Programming Languages},
  optpages = {},
  year = {2018},
  opteditor = {},
  optvolume = {},
  optnumber = {},
  optseries = {},
  optaddress = {},
  doi = {10.1145/3158107},
  month = jan,
  optorganization = {},
  optpublisher = {},
  optnote = {Draft},
  optannote = {},
  pdf = {http://www.cl.cam.ac.uk/~pes20/armv8-mca/armv8-mca-draft.pdf},
  project = {http://www.cl.cam.ac.uk/~pes20/armv8-mca/},
  abstract = {ARM has a relaxed memory model, previously specified in informal prose for ARMv7 and ARMv8.  Over time, and partly due to work building formal semantics for ARM concurrency, it has become clear that some of the complexity of the model is not justified by the potential benefits.  In particular, the model was originally \emph{non-multicopy-atomic}: writes could become visible to some other threads before becoming visible to all --- but this has not been exploited in production implementations, the corresponding potential hardware optimisations are thought to have insufficient benefits in the ARM context, and it gives rise to subtle complications when combined with other ARMv8 features.  The ARMv8 architecture has therefore been revised: it now has a multicopy-atomic model.  It has also been simplified in other respects, including more straightforward notions of dependency, and the architecture now includes a formal concurrency model.

In this paper we detail these changes and discuss their motivation. We define two formal concurrency models: an operational one, simplifying the Flowing model of Flur et al., and the axiomatic model of the revised ARMv8 specification. The models were developed by an academic group and by ARM staff, respectively, and this extended collaboration partly motivated the above changes. We prove the equivalence of the two models. The operational model is integrated into an executable exploration tool with new web interface, demonstrated by exhaustively checking the possible behaviours of a loop-unrolled version of a Linux kernel lock implementation, a previously known bug due to unprevented speculation, and a fixed version.},
  topic = {Power_and_ARM},
  topictwo = {ISA_semantics},
  recent = {true}
}

@inproceedings{cerberus-popl2019,
  author = {Kayvan Memarian and Victor B. F. Gomes and Brooks Davis and Stephen Kell and Alexander Richardson and Robert N. M. Watson and Peter Sewell},
  title = {Exploring {C} Semantics and Pointer Provenance},
  optcrossref = {},
  optkey = {},
  conf = {POPL 2019},
  booktitle = {Proceedings of the 46th ACM SIGPLAN Symposium on Principles of Programming Languages},
  optbooktitle = {},
  year = {2019},
  opteditor = {},
  optvolume = {},
  optnumber = {},
  optseries = {},
  optpages = {},
  month = jan,
  optaddress = {},
  optorganization = {},
  optpublisher = {},
  note = {Proc. ACM Program. Lang. 3, POPL, Article 67. Also available as ISO/IEC JTC1/SC22/WG14 N2311 },
  optannote = {},
  doi = {10.1145/3290380},
  pdf = {http://www.cl.cam.ac.uk/users/pes20/cerberus/cerberus-popl2019.pdf},
  supplementarymaterial = {http://www.cl.cam.ac.uk/users/pes20/cerberus/supplementary-material-popl2019},
  topic = {Cerberus},
  topictwo = {cheri},
  topicthree = {WG14},
  cheriformal = {true},
  project = {http://www.cl.cam.ac.uk/~pes20/cerberus},
  abstract = {The semantics of pointers and memory objects in C has been a vexed question for many years.  C values cannot be treated as either purely abstract or purely concrete entities: the language exposes their representations, but compiler optimisations rely on analyses that reason about provenance and initialisation status, not just runtime representations. The ISO WG14 standard leaves much of this unclear, and in some respects differs with de facto standard usage --- which itself is difficult to investigate.

In this paper we explore the possible source-language semantics for memory objects and pointers, in ISO C and in C as it is used and implemented in practice, focussing especially on pointer provenance.  We aim to, as far as possible, reconcile the ISO C standard, mainstream compiler behaviour, and the semantics relied on by the corpus of existing C code.  We present two coherent proposals, tracking provenance via integers and not; both address many design questions. We highlight some pros and cons and open questions, and illustrate the discussion with a library of test cases.  We make our semantics executable as a test oracle, integrating it with the Cerberus semantics for much of the rest of C, which we have made substantially more complete and robust, and equipped with a web-interface GUI.  This allows us to experimentally assess our proposals on those test cases.  To assess their viability with respect to larger bodies of C code, we analyse the changes required and the resulting behaviour for a port of FreeBSD to CHERI, a research architecture supporting hardware capabilities, which (roughly speaking) traps on the memory safety violations which our proposals deem undefined behaviour. We also develop a new runtime instrumentation tool to detect possible provenance violations in normal C code, and apply it to some of the SPEC benchmarks.  We compare our proposal with a source-language variant of the twin-allocation LLVM semantics proposal of Lee et al.  Finally, we describe ongoing interactions with WG14, exploring how our proposals could be incorporated into the ISO standard.
},
  recent = {true}
}

@inproceedings{sail-popl2019,
  author = {Alasdair Armstrong and Thomas Bauereiss and Brian Campbell and Alastair Reid and Kathryn E. Gray and Robert M. Norton and Prashanth Mundkur and Mark Wassell and Jon French and Christopher Pulte and Shaked Flur and Ian Stark and Neel Krishnaswami and Peter Sewell},
  title = {{ISA} Semantics for {ARMv8-A, RISC-V, and CHERI-MIPS}},
  optcrossref = {},
  optkey = {},
  conf = {POPL 2019},
  booktitle = {Proceedings of the 46th ACM SIGPLAN Symposium on Principles of Programming Languages},
  optbooktitle = {},
  year = {2019},
  opteditor = {},
  optvolume = {},
  optnumber = {},
  optseries = {},
  optpages = {},
  month = jan,
  optaddress = {},
  optorganization = {},
  optpublisher = {},
  note = {Proc. ACM Program. Lang. 3, POPL, Article 71},
  optnote = {},
  optannote = {},
  doi = {10.1145/3290384},
  abstract = {Architecture specifications notionally define the fundamental interface between hardware and software: the envelope of allowed behaviour for processor implementations, and the basic assumptions for software development and verification.  But in practice, they are typically prose and pseudocode documents, not rigorous or executable artifacts, leaving software and verification on shaky ground.

In this paper, we present rigorous semantic models for the sequential behaviour of large parts of the mainstream ARMv8-A, RISC-V, and MIPS architectures, and the research CHERI-MIPS architecture, that are complete enough to boot operating systems, variously Linux, FreeBSD, or seL4.  Our ARMv8-A models are automatically translated from authoritative ARM-internal definitions, and (in one variant) tested against the ARM Architecture Validation Suite.

We do this using a custom language for ISA semantics, Sail, with a lightweight dependent type system, that supports automatic generation of emulator code in C and OCaml, and automatic generation of proof-assistant definitions for Isabelle, HOL4, and (currently only for MIPS) Coq.  We use the former for validation, and to assess specification coverage.  To demonstrate the usability of the latter, we prove (in Isabelle) correctness of a purely functional characterisation of ARMv8-A address translation.  We moreover integrate the RISC-V model into the RMEM tool for (user-mode) relaxed-memory concurrency exploration.  We prove (on paper) the soundness of the core Sail type system.

We thereby take a big step towards making the architectural abstraction actually well-defined, establishing foundations for verification and reasoning.
},
  pdf = {http://www.cl.cam.ac.uk/users/pes20/sail/sail-popl2019.pdf},
  supplementarymaterial = {http://www.cl.cam.ac.uk/users/pes20/sail/popl2019.html},
  topic = {ISA_semantics},
  topictwo = {cheri},
  cheriformal = {true},
  project = {http://www.cl.cam.ac.uk/~pes20/sail/},
  recent = {true}
}

@article{tcp3draft,
  optkey = {},
  author = {Steve Bishop and Matthew Fairbairn and Hannes Mehnert and Michael Norrish and Tom Ridge and Peter Sewell and Michael Smith and Keith Wansbrough},
  title = {Engineering with Logic: Rigorous Test-Oracle Specification and Validation for {TCP/IP} and the {Sockets API}},
  journal = {J. ACM},
  opthowpublished = {},
  optmonth = {},
  issue_date = {December 2018},
  volume = {66},
  number = {1},
  month = dec,
  year = {2018},
  issn = {0004-5411},
  pages = {1:1--1:77},
  articleno = {1},
  numpages = {77},
  url = {http://doi.acm.org/10.1145/3243650},
  doi = {10.1145/3243650},
  acmid = {3243650},
  publisher = {ACM},
  optaddress = {New York, NY, USA},
  optnote = {Accepted for publication 2018-08},
  optannote = {},
  pdf = {http://www.cl.cam.ac.uk/~pes20/Netsem/paper3.pdf},
  project = {http://www.cl.cam.ac.uk/~pes20/Netsem/index.html},
  recent = {true},
  topic = {netsem},
  abstract = {
Conventional computer engineering relies on test-and-debug development
processes, with the behaviour of common interfaces described (at best)
with prose specification documents.  But prose specifications cannot be used in
test-and-debug development in any automated way, and prose is a poor
medium for expressing complex (and loose) specifications. 

The TCP/IP protocols and Sockets API are a good example of this:
they play a vital role in modern communication and computation, and
interoperability between implementations is essential.  But what
exactly they are is surprisingly obscure: their original development
focussed on ``rough consensus and running code'', augmented by prose
RFC specifications that do not precisely define what it means for an
implementation to be correct.  Ultimately, the actual standard is the
de facto one of the common implementations, including, for example,
the 15\,000--20\,000 lines of the BSD implementation --- optimised and
multithreaded C code, time-dependent, with asynchronous event
handlers, intertwined with the operating system, and
security-critical.

This paper reports on work done in the \emph{Netsem} project to
develop lightweight mathematically rigorous techniques that can be
applied to such systems: to specify their behaviour precisely (but
loosely enough to permit the required implementation variation) and to
test whether these specifications and the implementations correspond,
with specifications that are \emph{executable as test oracles}.
We developed post-hoc specifications of TCP, UDP, and the Sockets API, both of
the service that they provide to applications (in terms of TCP
bidirectional stream connections), and of the internal operation of
the protocol (in terms of TCP segments and UDP datagrams), together
with a testable abstraction function relating the two.  These specifications
are rigorous, detailed, readable, with broad coverage, and are rather
accurate.  Working within a general-purpose proof assistant (HOL4), we
developed \emph{language idioms} (within higher-order logic) in which
to write the specifications: operational semantics with
nondeterminism, time, system calls, monadic relational programming,
etc.  We followed an \emph{experimental semantics} approach,
validating the specifications against several thousand traces captured
from three implementations (FreeBSD, Linux, and WinXP).  Many
differences between these were identified, and a number of bugs.
Validation was done using a special-purpose \emph{symbolic model
  checker} programmed above HOL4.

Having demonstrated that our logic-based engineering techniques
suffice for handling real-world protocols, we argue that similar
techniques could be applied to future critical software infrastructure
at design time, leading to cleaner designs and (via
specification-based testing) more robust and predictable
implementations.  In cases where specification looseness can be
controlled, this should be possible with lightweight techniques,
without the need for a general-purpose proof assistant, at relatively
little cost.
}
}

@book{riscv-20181221-Public-Review-draft,
  optkey = {},
  editor = {Andrew Waterman and Krste Asanovi{\'{c}}},
  optauthor = {},
  title = {The {RISC-V} Instruction Set Manual  {Volume I: Unprivileged ISA}},
  howpublished = {\url{https://github.com/riscv/riscv-isa-manual/releases/download/draft-20181227-c6741cb/riscv-spec.pdf}},
  month = dec,
  year = 2018,
  note = {Document Version {20181221-Public-Review-draft. Contributors: Arvind, Krste Asanovi\'{c}, Rimas Avi\v{z}ienis, Jacob Bachmeyer, Christopher
F. Batten, Allen J. Baum, Alex Bradbury, Scott Beamer, Preston Briggs,
Christopher Celio, Chuanhua Chang, David Chisnall, Paul Clayton, Palmer
Dabbelt, Roger Espasa, Shaked Flur, Stefan Freudenberger, Jan Gray, Michael
Hamburg, John Hauser, David Horner, Bruce Hoult, Alexandre Joannou,
Olof Johansson, Ben Keller, Yunsup Lee,
Paul Loewenstein, Daniel Lustig, Yatin Manerkar, Luc Maranget, Margaret
Martonosi, Joseph Myers, Vijayanand Nagarajan, Rishiyur Nikhil, Jonas
Oberhauser, Stefan O'Rear, Albert Ou, John Ousterhout, David Patterson,
Christopher Pulte, Jose Renau, Colin Schmidt, Peter Sewell, Susmit Sarkar,
Michael Taylor, Wesley Terpstra, Matt Thomas, Tommy Thorn, Caroline Trippel,
Ray VanDeWalker, Muralidaran Vijayaraghavan, Megan Wachs, Andrew Waterman,
Robert Watson, Derek Williams, Andrew Wright, Reinoud Zandijk, and Sizhuo Zhang}},
  optannote = {},
  topic = {Power_and_ARM},
  recent = {true},
  pdf = {https://github.com/riscv/riscv-isa-manual/releases/download/draft-20181227-c6741cb/riscv-spec.pdf}
}

@misc{rems-summary,
  optkey = {},
  author = {Peter Sewell},
  title = {{REMS: Rigorous Engineering for Mainstream Systems. Summary 2013-03 -- 2019-01}},
  opthowpublished = {},
  month = feb,
  year = {2019},
  optnote = {},
  pdf = {http://www.cl.cam.ac.uk/users/pes20/rems/report-2019-web.pdf},
  optannote = {},
  abstract = {REMS, \emph{Rigorous Engineering for Mainstream Systems}, is an
EPSRC-funded Programme Grant (2013--2020, \pounds 5.6M, Cambridge,
Imperial, and Edinburgh) to explore how
we can use rigorous mathematics to improve engineering practice for
mainstream computer systems, to make them more robust and secure: 
broadly, to \emph{``create the intellectual and software tools to apply
semantics and verification at the heart of mainstream system
engineering''}.
%
REMS brings together an unusual combination of researchers to achieve this: in
architecture, operating systems, security, and networks,  and in
semantics, programming languages, and mechanised reasoning.
%
Our work is in close collaboration with a range of industrial
partners, including ARM, IBM, and the standards committees for C,
JavaScript, WebAssembly, and TLS. 

We are building accurate full-scale mathematical models of some of the
key computational abstractions (processor architectures, programming
languages, concurrent OS interfaces, and network protocols), studying
how this can best be done, and investigating how such models can be used
for new verification research and in new systems and programming
language research.  For many of these abstractions, our work has
exposed and clarified fundamental questions about what the
abstractions are, and provided tools to let them be explored.   Supporting all this, we are also developing new
specification tools.  Most of our models and tools are publicly
available under permissive open-source licences. 

This note summarises REMS progress to date.  Highlights include
models and tools for the production ARMv8-A architecture (including
user-mode concurrency and the full ISA), the RISC-V and research
CHERI-MIPS architectures, the C, JavaScript, and WebAssembly
programming languages, ELF linking, POSIX filesystems, the TLS and TCP
protocols, and extensive work on concurrency verification.
},
  recent = {true}
}

@inproceedings{cheriABIsub,
  optkey = {},
  author = {Brooks Davis and
              Robert N. M. Watson and
              Alexander Richardson and
              Peter G. Neumann and
              Simon W. Moore and
              John Baldwin and
              David Chisnall and
              James Clarke and
              Nathaniel Wesley Filardo and 
Khilan Gudka and
              Alexandre Joannou and
              Ben Laurie and
              A. Theodore Markettos and
              J. Edward Maste and
              Alfredo Mazzinghi and
           Edward Tomasz Napierala and
              Robert M. Norton and
              Michael Roe and
              Peter Sewell and
              Stacey Son and
              Jonathan Woodruff},
  title = {{CheriABI}: Enforcing Valid Pointer Provenance and Minimizing
              Pointer Privilege in the {POSIX C} Run-time Environment},
  opthowpublished = {Submitted for publication},
  conf = {ASPLOS 2019},
  booktitle = {the 24th ACM International Conference on Architectural Support for Programming Languages and Operating Systems},
  month = apr,
  year = {2019},
  note = {Best paper award},
  url = {http://doi.acm.org/10.1145/3297858.3304042},
  doi = {10.1145/3297858.3304042},
  acmid = {3304042},
  publisher = {ACM},
  optannote = {},
  abstract = {The CHERI architecture allows pointers to be implemented as
capabilities (rather than integer virtual addresses) in a manner that
is compatible with, and strengthens, the
semantics of the C language.
In addition to the spatial protections offered by conventional fat pointers,
CHERI capabilities offer strong integrity, enforced provenance validity, and
access monotonicity.
The stronger guarantees of these architectural capabilities must be reconciled with the real-world behavior of operating systems, run-time environments, and applications.
When the process model, user-kernel interactions, dynamic linking, and memory
management are all considered, we observe that simple derivation of architectural capabilities is insufficient to describe appropriate access to memory.
We bridge this conceptual gap with a notional \emph{abstract capability} that
describes the accesses that should be allowed at a given point in execution,
whether in the kernel or userspace.
To investigate this notion at scale, we describe the first adaptation of a
full C-language operating system (FreeBSD) with an enterprise database
(PostgreSQL) for complete spatial and referential memory safety.
We show that awareness of abstract capabilities, coupled with CHERI
architectural capabilities, can provide more complete protection, strong
compatibility, and acceptable performance overhead compared with the pre-CHERI
baseline and software-only approaches.
Our observations also have potentially significant implications for other
mitigation techniques.},
  pdf = {https://www.cl.cam.ac.uk/research/security/ctsrd/pdfs/201904-asplos-cheriabi.pdf},
  project = {https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/},
  topic = {cheri},
  cheriformal = {true},
  recent = {true}
}

@inproceedings{cerberusBMC,
  author = {Stella Lau and Victor B. F. Gomes and Kayvan Memarian and Jean Pichon-Pharabod and Peter Sewell},
  title = {{Cerberus-BMC}: a Principled Reference Semantics and Exploration
  Tool for Concurrent and Sequential {C}},
  optcrossref = {},
  optkey = {},
  conf = {CAV 2019},
  booktitle = {Proc. 31st International Conference on Computer-Aided Verification},
  optpages = {},
  year = {2019},
  opteditor = {},
  optvolume = {},
  optnumber = {},
  optseries = {},
  optaddress = {},
  month = jul,
  optorganization = {},
  optpublisher = {},
  optnote = {},
  optannote = {},
  pdf = {http://www.cl.cam.ac.uk/users/pes20/cerberus/bmc-cerberus.pdf},
  topic = {Cerberus},
  project = {http://www.cl.cam.ac.uk/~pes20/cerberus},
  abstract = {C remains central to our infrastructure, making verification of C code
an essential and much-researched topic, but the semantics of C is
remarkably complex, and important aspects of it are still unsettled,
leaving programmers and verification tool builders on shaky
ground.

This paper describes a tool, Cerberus-BMC, that for the first time
provides a principled reference semantics that simultaneously supports
(1) a choice of concurrency memory model (including substantial
fragments of the C11, RC11, and Linux kernel memory models), (2) a modern memory object model,
and (3) a well-validated thread-local semantics for a large fragment
of the language.
The tool should be useful for C programmers, compiler writers,
verification tool builders, and members of the C/C++ standards committees.
},
  recent = {true}
}

@techreport{UCAM-CL-TR-927,
  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 Chisnall, David
          	  and Davis, Brooks and Filardo, Nathaniel Wesley 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, Alex
          	  and Rugg, Peter and Sewell, Peter and Son, Stacey and Xia,
          	  Hongyan},
  title = {{Capability Hardware Enhanced RISC Instructions: CHERI
         	   Instruction-Set Architecture (Version 7)}},
  year = 2019,
  month = jun,
  pdf = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-927.pdf},
  institution = {University of Cambridge, Computer Laboratory},
  number = {UCAM-CL-TR-927},
  note = {496pp},
  topic = {CHERI},
  abstract = {This technical report describes CHERI ISAv7, the seventh version of the
Capability Hardware Enhanced RISC Instructions (CHERI) Instruction-Set
Architecture (ISA)
being developed by SRI International and the University of Cambridge.
This design captures nine years of research, development, experimentation,
refinement, formal analysis, and validation through hardware and software
implementation.
CHERI ISAv7 is a substantial enhancement to prior ISA versions.
We differentiate an architecture-neutral protection model vs.
architecture-specific instantiations in 64-bit MIPS, 64-bit RISC-V, and
x86-64.
We have defined a new CHERI Concentrate compression model.
CHERI-RISC-V is more substantially elaborated.
A new compartment-ID register assists in resisting microarchitectural
side-channel attacks.
Experimental features include linear capabilities, capability coloring,
temporal memory safety, and 64-bit capabilities for 32-bit architectures.

CHERI is a {\em hybrid capability-system architecture} that adds new
capability-system primitives to commodity 64-bit RISC ISAs, enabling software
to efficiently implement {\em fine-grained memory protection} and {\em
scalable software compartmentalization}.
Design goals include incremental adoptability within current ISAs and
software stacks, low performance overhead for memory protection, significant
performance improvements for software compartmentalization, formal grounding,
and programmer-friendly underpinnings.
We have focused on providing strong, non-probabilistic, efficient
architectural foundations for the principles of \textit{least privilege} and
\textit{intentional use} in the execution of software at multiple levels of
abstraction, preventing and mitigating vulnerabilities.

The CHERI system architecture purposefully addresses known performance and
robustness gaps in commodity ISAs that hinder the adoption of more secure
programming models centered around the principle of least privilege.
To this end, CHERI blends traditional paged virtual memory with an
in-address-space capability model that includes capability registers,
capability instructions, and tagged memory.
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 also improving
control-flow robustness.
Strong capability integrity and monotonicity properties allow the CHERI model
to express a variety of protection properties, 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 capability-system approach, inspired by the Capsicum security
model, allows incremental adoption of capability-oriented design: software
implementations that are more robust and resilient can be deployed where they
are most needed, while leaving less critical software largely unmodified, but
nevertheless suitably constrained to be incapable of having adverse effects.
Potential deployment scenarios include low-level software Trusted Computing
Bases (TCBs) such as separation kernels, hypervisors, and operating-system
kernels, as well as userspace TCBs such as language runtimes and web browsers.
We also see potential early-use scenarios around 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, while leaving
containing applications unchanged.
  },
  cheriformal = {true},
  recent = {true}
}

@techreport{cheri-formal-tr,
  optkey = {},
  author = {
  Kyndylan Nienhuis
  and Alexandre Joannou
  and Anthony Fox
  and Michael Roe
  and Thomas Bauereiss
  and Brian Campbell
  and Matthew Naylor
  and Robert M. Norton
  and Simon W. Moore
  and Peter G. Neumann
  and Ian Stark
  and Robert N. M. Watson
  and Peter Sewell
  },
  title = {Rigorous engineering for hardware security: Formal modelling and proof in the {CHERI} design and implementation process},
  institution = {University of Cambridge, Computer Laboratory},
  number = {UCAM-CL-TR-940},
  opthowpublished = {Draft},
  month = sep,
  year = {2019},
  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 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.
},
  optproject = {https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/},
  opttopic = {cheri},
  cheriformal = {true},
  recent = {true},
  pdf = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-940.pdf}
}

@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 = {},
  optpages = {},
  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},
  project = {https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/},
  topic = {cheri},
  cheriformal = {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 (extended version)},
  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 = {},
  note = {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},
  project = {http://www.cl.cam.ac.uk/~pes20/iflat},
  pdf = {http://www.cl.cam.ac.uk/~pes20/iflat/top-extended.pdf}
}