REMS: Rigorous Engineering for Mainstream Systems

Lead Research Organisation: University of Cambridge
Department Name: Computer Laboratory

Abstract

Computer systems are critical to modern society, from embedded devices and mobile phones through to internet services, but traditional computer engineering cannot produce reliable and secure systems, as we see in the continual stream of errors and security flaws impacting industry and consumers everywhere. Industry relies on informal prose specifications and ad hoc testing, but the complexity and scale of today's systems make it effectively impossible to exclude errors using only these methods (even though perhaps 70\% of development staff in major vendors are devoted to testing) and adversarial exploits all too often turn errors into major security concerns, with huge financial and social costs. Compounding the problem, the industry-wide abstractions around which real systems are built, including the architectural interfaces between multiprocessor hardware and software, and programming languages such as C and C++, are ill-defined, giving rise to ambiguity and error.

This is a long-standing problem, motivating extensive research on mathematically rigorous alternatives. Until now, it has been impractical to address mainstream widely-deployed systems with rigorous techniques. Academic research has focussed instead on modest-scale safety critical systems and academic verifications of idealised systems. There has been a deep disconnect between practical industrial engineering and systems research on the one hand, and theoretical research in semantics, verification, and foundations on the other. Now, however, the new approaches that we have, with a pragmatic emphasis on the use of mathematically rigorous models where they can be most effective, finally make it feasible to address industrial-scale systems--- and the commercial and social cost of not doing so is becoming ever greater. It is time for rigorous engineering of mainstream systems, unifying practice and theory.

REMS brings together a team of leading theory and systems researchers, with key industrial partners, to establish a new synthesis. We will establish a true engineering mathematics for the construction of more robust and secure computer systems: mathematically rigorous models, verification techniques, and engineering tools applied to the construction of full-scale mainstream computer systems, including key infrastructure in widespread use today (multiprocessors, programming languages, and operating systems). We will couple this with novel programming-language and verification support for future system-building. Developing our recent work with processor vendors and language standards bodies, we will address the technical, engineering and social challenges necessary to bring these techniques into widespread use, enabling a radical improvement in computer engineering as a whole.

Planned Impact

Computer systems are pervasive, from a host of embedded devices (in everything from heating controllers and power distribution networks to cars and mobile phones), through the Internet giving us email and the web, up to the supercomputers used for weather forecasting and scientific research. We rely on them in almost everything we do, but they are fundamentally unreliable: they are developed by testing-based methods that cannot handle the complexity of modern systems. The result is a high direct cost, to build adequate systems by these inadequate methods, and a much higher indirect cost, on all of society, to handle the inevitable bugs and inexplicable behaviours that occur and to deal with the security problems that arise when the remaining errors are exploited.


The ambitious aim of the REMS project is to enable and provoke a profound change in how computer systems are engineered, placing *mathematically rigorous* engineering methods at the heart of the development of mainstream systems. This will be achieved by building on precise mathematical models of some of the key abstractions around which all computer systems are constructed: multiprocessors and the C programming language. It will not remove all problems, but it will provide a significant step towards making the products of computer engineering as reliable as the other engineering infrastructure on which society depends.

Towards this broad societal impact are many specific opportunities for economic impact, including:

- On the architectural interface between hardware and software, our processor-vendor partners ARM and IBM will benefit directly from improved specifications, the testing tools that they enable, and discussions of future architectural choices; all users of this interface (compiler and operating system vendors) will benefit from the increased clarity.

- On the definition of the C language, system developers will benefit directly from more accurate ISO standards and improved core infrastructure and, more concretely, from our static and dynamic analysis tools.

- Several start-up possibilities that may arise from particular subtasks, e.g. from some of our tool developments, which we will pursue as appropriate, building on our XenSource experience.



The most important economic impact will be via the eventual effects of deploying rigorous methods across the computing industry, improving quality and reducing time- and cost-to-market for its products. By improving the quality of these products, we will reduce the hidden cost of unreliability and insecurity in computer systems, which affect us all.

Publications

10 25 50
publication icon
Armstrong A (2019) ISA semantics for ARMv8-a, RISC-v, and CHERI-MIPS in Proceedings of the ACM on Programming Languages

publication icon
BauereiƟ T (2017) CoSMed: A Confidentiality-Verified Social Media Platform in Journal of Automated Reasoning

publication icon
Bishop S (2018) Engineering with Logic in Journal of the ACM

publication icon
Campbell B (2016) Randomised testing of a microprocessor model using SMT-solver state generation in Science of Computer Programming

publication icon
Chakraborty S (2015) Aspect-oriented linearizability proofs in Logical Methods in Computer Science

publication icon
Chisnall D (2017) CHERI JNI

publication icon
Chisnall D (2018) C is not a low-level language in Communications of the ACM

 
Description REMS: Rigorous Engineering for Mainstream Systems
EPSRC Programme Grant EP/K008528/1,
5.6M, 2013--2019 (extended to 2020)
http://www.cl.cam.ac.uk/users/pes20/rems
Progress Report, Year 5 (2017--18)


Progress in 2017--18
====================
We have aimed for a more concise report this year, just summarising the main items and including abstracts of new papers, to reduce the burden on readers. As usual, links to all the REMS papers and tools are available from the project website, at http://www.cl.cam.ac.uk/users/pes20/rems.


Ott and Lem
-----------
We continue to use and maintain our Ott and Lem tools for semantic specification. Lem is used in our Sail-to-Isabelle workflow, and to express our operational concurrency models, Cerberus C semantics, and Linksem ELF linking semantics. Ott is used (among other things) to define Sail and the Cerberus Core language.

In 2017, the original Ott paper

Ott: Effective Tool Support for the Working Semanticist.
Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine,
Thomas Ridge, Susmit Sarkar, and Rok Strnisa. ICFP 2007

was awarded the ACM SIGPLAN Most Influential ICFP Paper Award (the papers are judged by their influence over the past decade).


Sail and Instruction-set Architecture Semantics
-----------------------------------------------
We are devoting substantial effort to our Sail metalanguage for describing processor instruction semantics, and to Sail models for particular architectures.

Sail describes the intra-instruction semantics of processor architectures -- mainly their sequential behaviour, though it also provides the necessary hooks for describing their concurrency architectures.

In the last year Sail has been re-engineered with a new type checker and with backends for Isabelle, OCaml, and C.

The development is available on GitHub: https://github.com/rems-project/sail. [2017--18 people: Armstrong, Bauereiss, Campbell, Flur, Fox, French, Krishnaswami, Mundkur (SRI), Norton-Wright, Pulte, Reid (ARM), Sewell, Stark, Wassell.]

[ARM] With the help of Reid at ARM, we have an automated translation of the full ARMv8.3-A specification (in its ARM-internal ASL form) into well-typed Sail, and a preliminary translation of that (via Lem) into Isabelle to support proof.

[CHERI-MIPS] We have established a complete Sail model of our CHERI research architecture.

[RISC-V] We have established a Sail model of the core RISC-V user-mode ISA, and are working to expand this.

[x86] For x86, we have written a Sail model of a modest fragment of the user-mode ISA, suitable for mixed-size litmus tests and simple binaries.

[IBM POWER] For POWER we continue to maintain our core user-mode ISA specification semi-automatically derived from an XML version of the IBM architecture specification.



Multiprocessor Concurrency Architecture Semantics
-------------------------------------------------

[ARM] Working with Deacon at ARM, we have established provably equivalent operational and axiomatic concurrency models for ARMv8-A. The ARM concurrency architecture has been substantially simplified, partly as a result of our work, and a prose version of the axiomatic model now forms part of the official ARM specification. [POPL 2018]

[RISC-V] As part of the RISC-V Memory Model Task Group, we are contributing to the design and specification of the RISC-V concurrency architecture. [Flur, Pulte, Maranget, Sewell]

[rmem] We have continued to engineer our rmem tool, supporting interactive, random, and exhaustive exploration of the behaviour of concurrent litmus tests and small ELF binaries w.r.t. operational concurrency models and Sail ISA specifications. The tool has web and command-line interfaces. http://www.cl.cam.ac.uk/users/pes20/rmem [French, Flur, Pulte, Sewell]

Sewell gave a keynote on this work at PPoPP 2018.


CHERI
-----
We have released a new version of our CHERI architecture ISA specification. [Technical Report]

We have shown how an optimised implementation of tagged memory (as proposed in CHERI and elsewhere to provide security) can typically achieve near-zero memory traffic overhead. [ICCD 2007]

We continue to work on the formal verification of CHERI security properties. [Nienhuis]


Cerberus C Semantics
--------------------
We continue to develop our Cerberus semantics for the sequential aspects of C, informed by both the ISO and de facto standards. Cerberus now has a web interface that lets one explore the type-checking, elaboration to Core, and execution of small examples in C, identifying the relevant clauses of the ISO standard where possible: http://svr-pes20-cerberus.cl.cam.ac.uk/ [Memarian, Gomes, Sewell]

We will give a keynote on this at EuroLLVM 2018 and attend the next ISO WG14 standards committee meeting in April 2018.

We have also published an essay on the role of C in modern systems software. [Onward! 2017]


JavaScript
----------
We have developed JSExplain, a reference interpreter for JavaScript that closely follows the specification and that produces execution traces. These traces may be interactively investigated in a browser, with an interface that displays not only the code and the state of the interpreter, but also the code and the state of the interpreted program. In that respect, JSExplain is a double-debugger for the specification of JavaScript, useful both for standard developers and JavaScript programmers. [WWW'18 Companion]

We have developed JaVerT, a semi-automatic JavaScript Verification Toolchain, based on separation logic and aimed at the specialist developer wanting rich, mechanically verified specifications of critical JavaScript code. JaVerT is the first verification tool based on separation logic that targets dynamic languages. To specify JavaScript code, we provide abstractions that capture its key heap structures (for example, prototype chains and function closures), allowing the developer to write clear and succinct specifications with minimal knowledge of the JavaScript internals. To verify JavaScript programs, we develop a trusted verification pipeline consisting of: JS-2-JSIL, a well-tested compiler from JavaScript to JSIL, an intermediate goto language capturing the fundamental dynamic features of JavaScript; JSIL Verify, a semi-automatic verification tool based on a sound JSIL separation logic; and verified axiomatic specifications of the JavaScript internal functions. JaVerT has so far been used to verify functional correctness properties of: data-structure libraries (key-value map, priority queue) written in an object-oriented style; operations on data structures such as binary search trees (BSTs) and lists; examples illustrating function closures; and test cases from the official ECMAScript test suite. The verification times suggest that reasoning about larger, more complex code using JaVerT is feasible. [POPL 2018]

We have developed a system for logic-based verification of JavaScript programs. [CADE 2017]


WebAssembly
-----------
We have produced a mechanised Isabelle specification for the WebAssembly language, together with a verified executable interpreter and type checker, and a fully mechanised proof of the soundness of the WebAssembly type system. [CPP 2018]


Modular Foreign Function Interfaces
-----------------------------------
We have published a journal paper showing how ML-style module systems can support clean foreign-function interfaces. [Sci. Comp. Prog. 2017]


Reasoning about concurrency
---------------------------
We have published four papers on reasoning about different aspects of
relaxed concurrency:

Separation logic for Promising Semantics [ESOP 2018]

Algebraic laws for weak consistency [CONCUR 2017]

Verifying strong eventual consistency in distributed systems [OOPSLA 2017, Distinguished Paper Award]

Transactions with relaxed concurrency (largely non-REMS work) [VMCAI 2018]



Verified trustworthy systems
----------------------------
We have published an opinion piece with the goal of raising awareness about the pressing issues surrounding reliability of complex modern software systems and the importance of specification and verification in the industrial design process. This publication is part of a broader journal publication on Verified Trustworthy Software Systems, aimed at the general public. [Phil. Trans. A]



Confidentiality verification
----------------------------
We have published a journal paper on earlier (largely non-REMS) work on formal verification of confidentiality in a social media system. [J. Automated Reasoning 2017]


Programming and proving with classical types
--------------------------------------------

We have published the following on programming and proving with classical types, building on an MPhil dissertation of the first author supervised by REMS staff. [APLAS 2017]


Summary of REMS publications by calendar year
---------------------------------------------
The starred papers are new since the 2016--17 report.



2014

Onward! 2014
ICFP 2014
FMICS 2014
ECOOP 2014
MFPS 2014
ESOP 2014
RAMiCS 2014
PEPM 2014
POPL 2014
J. Funct. Program.

31C3 talk
Batty PhD
EuroLLVM talk
Clement MPRI


2015

MICRO 2015
APLAS 2015
CCS 2015
Onward! 2015
SOSP 2015
OOPSLA 2015
MEMOCODE 2015
ITP 2015
USENIX Security 2015
VSTTE 2015
MFPS 2015
Security and Privacy 2015
LSFA 2014
ESOP 2015
ESOP 2015
ESOP 2015
LMCS
ASPLOS 2015
ASPLOS 2015
UCAM-CL-TR-876
UCAM-CL-TR-877
HCSS talk

2016

OOPSLA 2016
OOPSLA 2016
OOPSLA 2016
FM 2016
APLAS 2016
APLAS 2016
FMCAD 2016
FMCAD 2016
IEEE Micro
OCaml 2016
OCaml 2016
CONCUR 2016
PLDI 2016
ESOP 2016
ESOP 2016
Sci. Comp. Prog.
POPL 2016
POPL 2016
AFP
WG14
WG14
TLS v1.3 TRON
TyDe 2016
Ntzik PhD
da Rocha Pinto PhD
Raad PhD

2017

ASPLOS 2017
ESOP 2017
ESOP 2017
POPL 2017
POPL 2017
CPP 2017
(*) ICCD 2017
(*) CONCUR 2017
(*) CADE 2017
(*) OOPSLA 2017
(*) APLAS 2017
(*) Sci. Comp. Prog
(*) Onward! 2017
(*) J. Aut. Reas. 2017
(*) Phil. Trans. A 2017

2018

(*) POPL 2018
(*) POPL 2018
(*) ESOP 2018
(*) CPP 2018
(*) WWW Comp. 2018
(*) VMCAI 2018

(*) UCAM-CL-TR-907


Funding
-------
To accommodate various staffing changes, the EPSRC approved a no-cost extension, to 28 Feb 2020.


People
------

Investigators:

We very sadly lost Mike Gordon, who died suddenly in August 2017. Mike made an enormous contribution to REMS, which builds on much of his work. See http://www.cl.cam.ac.uk/misc/obituaries/gordon/ for his obituary.

Neel Krishnaswami, who joined the Cambridge Computer Laboratory as a faculty member in 2016, is contributing substantially to REMS, effectively as a co-investigator.

Anil Madhavapeddy returned to his University position from sabbatical leave.

Postdocs, PhD students, and interns:

This lists the research staff involved in 2017--18 in REMS (not all REMS-funded).


Cambridge

Alasdair Armstrong (RA)
Thomas Bauereiss (RA) -- new appointment
David Chisnall (SRA)
Shaked Flur (RARS)
Anthony Fox (SRA) -- left to join ARM Research
Jon French (RAsst)
Victor Gomes (RA)
Chung-Kil Hur (SNU, South Korea) -- sabbatical visit Jul 2017 -- Feb 2018
Alexandre Joannou (RARS)
Stephen Kell (SRA) -- has accepted a faculty position at the University of Kent from August 2018
Justus Matthiesen (RS)
Hannes Mehnert (RA) -- left to work for a free software organisation in Berlin
Kayvan Memarian (RARS)
David Kaloper Mersinjak (RS)
Dominic Mulligan (RA) -- left to join ARM Research
Kyndylan Neinhuis (RARS)
Robert Norton-Wright (RA)
Jean Pichon-Pharabod (RARS) -- PhD examined
Christopher Pulte (RS)
Linden Ralph (undergraduate intern, summer 2017)
Mike Roe (SRA)
Kasper Svendsen (visiting PDRA) -- returned to Denmark
Mark Wassell (RS)
Conrad Watt (RS)

Imperial
Andrea Cerone (RA)
Emanuele D'Osualdo (RA)
Jose Fragoso Santos (RA)
Petar Maksimovic (RA)
Thomas Wood (RA)
Julian Sutherland (RS)
Shale Xiong (RS)
Gian Ntzik (RS) -- left to Amadeus Systems
Azalea Raad (RS) -- left to a PDRA position in MPI-SWS

Edinburgh
Brian Campbell (RA)

Previous REMS research staff:

Cambridge

Mark Batty (RA) -- moved to an RAEng fellowship and faculty position at Kent
Kathy Gray (RA) -- moved to Facebook (London)
Ohad Kammar (RA) -- moved to a research position at Oxford
Gabriel Kerneis (RA) -- moved to Google (Paris)
Ramana Kumar (RS) -- moved to NICTA (Australia) and now to DeepMind (London)
James Lingard (MPhil) -- moved to Microsoft Research
Magnus Myreen (proposal co-author) -- moved to a faculty position at Chalmers
Matt Naylor (RA) -- moved to another Cambridge research position
Ali Sezgin (RA)
David Sheets (RS) -- moved to Docker
Thomas Tuerk (RA) -- moved to FireEye
Susmit Sarkar (proposal co-author) -- moved to a faculty position at
t Andrews
Scott Owens (proposal co-author) -- moved to a faculty position at Kent

Imperial
Pedro da Rocha Pinto
Thomas Dinsdale-Young -- moved to a research position at Aarhus
Jules Villard -- moved to Facebook (London)
Adam Wright






Papers from 2017--18
---------------------

\bibitem[Bauereiss:2017]{Bauereiss:2017}
Thomas Bauerei{\ss}, Armando Pesenti~Gritti, Andrei Popescu, and Franco
Raimondi.
Cosmed: A confidentiality-verified social media platform.
{\em \textbf{Journal of Automated Reasoning}}, December 2017.
\begin{quote} {\bf Abstract:} This paper describes progress with our
agenda of formal verification of information flow security for realistic
systems. We present CoSMed, a social media platform with verified document
confidentiality. The system's kernel is implemented and verified in the proof
assistant Isabelle/HOL. For verification, we employ the framework of
Bounded-Deducibility (BD) Security, previously introduced for the conference
system CoCon. CoSMed is a second major case study in this framework. For
CoSMed, the static topology of declassification bounds and triggers that
characterized previous instances of BD Security has to give way to a dynamic
integration of the triggers as part of the bounds. We also show that, from a
theoretical viewpoint, the removal of triggers from the notion of BD Security
does not restrict its expressiveness. \end{quote}

\bibitem[Cerone2017Algebraic]{Cerone2017Algebraic}
Andrea Cerone, Alexey Gotsman, and Hongseok Yang.
Algebraic laws for weak consistency.
In {\em \textbf{CONCUR 2017}: Proceedings of 28th International
Conference on Concurrency Theory}, September 2017.
\begin{quote} {\bf Abstract:} Modern distributed systems often rely
on so called weakly-consistent databases, which achieve scalability by
sacrificing the consistency guarantee of distributed transaction processing.
Such databases have been formalised in two different styles, one based on
abstract executions and the other based on dependency graphs. The choice
between these styles has been made according to intended applications. The
former has been used for specifying and verifying the implementation of these
databases, while the latter for proving properties of client programs of the
databases. In this paper, we present a set of novel algebraic laws (i.e.
inequations) that connect these two styles of specifications. The laws relate
binary relations used in a specification based on abstract executions, to
those used in a specification based on dependency graphs. We then show that
this algebraic connection gives rise to so called robustness criteria,
conditions which ensure that a client program of a weakly-consistent database
does not exhibit anomalous behaviours due to weak consistency. These criteria
make it easy to reason about these client programs, and may become a basis
for dynamic or static program analyses. For a certain class of consistency
models specifications, we prove a full abstraction result that connects the
two styles of specifications. \end{quote}

\bibitem[Chargueraud2018JSExplain]{Chargueraud2018JSExplain}
Arthur Chargu{\'e}raud, Alan Schmitt, and Thomas Wood.
{JSExplain}: a double debugger for {JavaScript}.
In {\em \textbf{WWW '18 Companion}: The 2018 Web Conference
Companion, April 23--27, 2018, Lyon, France}. ACM, April 2018.
\begin{quote} {\bf Abstract:} We present JSExplain, a reference
interpreter for JavaScript that closely follows the specification and that
produces execution traces. These traces may be interactively investigated in
a browser, with an interface that displays not only the code and the state of
the interpreter, but also the code and the state of the interpreted program.
Conditional breakpoints may be expressed with respect to both the interpreter
and the interpreted program. In that respect, JSExplain is a double-debugger
for the specification of JavaScript. \end{quote}

\bibitem[DBLP:conf/cade/SantosGMN17]{DBLP:conf/cade/SantosGMN17}
Jos{\'{e}}~Fragoso Santos, Philippa Gardner, Petar Maksimovic, and Daiva
Naudziuniene.
Towards logic-based verification of {JavaScript} programs.
In Leonardo de~Moura, editor, {\em \textbf{CADE 2017}: 26th
International Conference on Automated Deduction}, volume 10395 of {\em
Lecture Notes in Computer Science}, pages 8--25. Springer, August 2017.

\bibitem[DongolJRA2018]{DongolJRA2018}
Brijesh Dongol, Radha Jagadeesan, James Riely, and Alasdair Armstrong.
On abstraction and compositionality for weak-memory linearisability.
In Isil Dillig and Jens Palsberg, editors, {\em Verification, Model
Checking, and Abstract Interpretation - 19th International Conference,
{VMCAI} 2018, Los Angeles, CA, USA, January 7-9, 2018, Proceedings}, LNCS,
pages 183--204. Springer, 2018.
\begin{quote} {\bf Abstract:} Linearisability is the de facto
standard correctness condition for concurrent objects. Classical
linearisability assumes that the effect of a method is captured entirely by
the allowed sequences of calls and returns. This assumption is inadequate in
the presence of relaxed memory models, where happens-before relations are
also of importance. In this paper, we develop hb-linearisability for relaxed
memory models by extending the classical notion with happens-before
information. We con- sider two variants: Real time hb-linearisability, which
adopts the classical view that time runs on a single global clock, and causal
hb-linearisability, which eschews real-time and is appropriate for systems
without a global clock. For both variants, we prove abstraction (so that
programmers can reason about a client program using the sequential speci
cation of an object rather than its more complex concurrent implementation)
and composition (so that reasoning about independent objects can be conducted
in isolation). \end{quote}

\bibitem[FragosoSantos2018JaVerT]{FragosoSantos2018JaVerT}
Jos{\'{e}} {Fragoso Santos}, Petar Maksimovi\'{c}, Daiva
Naud\v{z}i\={u}nien\.{e}, Thomas Wood, and Philippa Gardner.
{JaVerT: JavaScript verification toolchain}.
{\em {PACMPL}}, 2(\textbf{POPL}):50:1--50:33, 2018.
\begin{quote} {\bf Abstract:} The dynamic nature of JavaScript and
its complex semantics make it a difficult target for logic-based
verification. We introduce JaVerT, a semi-automatic JavaScript Verification
Toolchain, based on separation logic and aimed at the specialist developer
wanting rich, mechanically verified specifications of critical JavaScript
code. To specify JavaScript programs, we design abstractions that capture its
key heap structures (for example, prototype chains and function closures),
allowing the developer to write clear and succinct specifications with
minimal knowledge of the JavaScript internals. To verify JavaScript programs,
we develop JaVerT, a verification pipeline consisting of: JS-2-JSIL, a
well-tested compiler from JavaScript to JSIL, an intermediate goto language
capturing the fundamental dynamic features of JavaScript; JSIL Verify, a
semi-automatic verification tool based on a sound JSIL separation logic; and
verified axiomatic specifications of the JavaScript internal functions. Using
JaVerT, we verify functional correctness properties of: data-structure
libraries (key-value map, priority queue) written in an object-oriented
style; operations on data structures such as binary search trees (BSTs) and
lists; examples illustrating function closures; and test cases from the
official ECMAScript test suite. The verification times suggest that reasoning
about larger, more complex code using JaVerT is feasible. \end{quote}

\bibitem[Gardner2017Verified]{Gardner2017Verified}
Philippa Gardner.
Verified trustworthy software systems.
{\em \textbf{Philosophical Transactions of the Royal Society of
London A}: Mathematical, Physical and Engineering Sciences}, 375(2104),
September 2017.
\begin{quote} {\bf Abstract:} Modern society is faced with a
fundamental problem: the reliability of complex, evolving software systems on
which society critically depends cannot be guaranteed by the established,
non-mathematical computer engineering techniques such as informal prose
specification and ad hoc testing. The situation is worsening: modern
companies are moving fast, leaving little time for code analysis and testing;
the behaviour of concurrent and distributed programs cannot be adequately
assessed using traditional testing methods; users of mobile applications
often neglect to apply software fixes; and malicious users increasingly
exploit even simple programming errors, causing major security disruptions.
Building trustworthy, reliable software is becoming harder and harder to
achieve, while new business and cybersecurity challenges make it of
escalating critical importance \end{quote}

\bibitem[Joannou2017Tags]{Joannou2017Tags}
Alexandre Joannou, Jonathan Woodruff, Robert Kovacsics, Simon~W. Moore, Alex
Bradbury, Hongyan Xia, Robert N.~M. Watson, David Chisnall, Michael Roe,
Brooks Davis, Edward Napierala, John Baldwin, Khilan Gudka, Peter~G. Neumann,
Alfredo Mazzinghi, Alex Richardson, Stacey Son, and A.~Theodore Markettos.
Efficient tagged memory.
In {\em \textbf{ICCD 2017}: IEEE 35th International Conference on
Computer Design}, November 2017.
\begin{quote} {\bf Abstract:} We characterize the cache behavior of
an in-memory tag table and demonstrate that an optimized implementation can
typically achieve a near-zero memory traffic overhead. Both industry and
academia have repeatedly demonstrated tagged memory as a key mechanism to
enable enforcement of power- ful security invariants, including capabilities,
pointer integrity, watchpoints, and information-flow tracking. A single-bit
tag shadowspace is the most commonly proposed requirement, as one bit is the
minimum metadata needed to distinguish between an untyped data word and any
number of new hardware- enforced types. We survey various tag shadowspace
approaches and identify their common requirements and positive features of
their implementations. To avoid non-standard memory widths, we identify the
most practical implementation for tag storage to be an in-memory table
managed next to the DRAM controller. We characterize the caching performance
of such a tag table and demonstrate a DRAM traffic overhead below 5\% for the
vast majority of applications. We identify spatial locality on a page scale
as the primary factor that enables surprisingly high table cache-ability. We
then demonstrate tag-table compression for a set of common applications. A
hierarchical structure with elegantly simple optimizations reduces DRAM
traffic overhead to below 1% for most applications. These insights and
optimizations pave the way for commercial applications making use of
single-bit tags stored in commodity memory. \end{quote}

\bibitem[SvendsenEtAl2018]{SvendsenEtAl2018}
Kasper Svendsen, Jean Pichon-Pharabod, Marko Doko, Ori Lahav, and Viktor
Vafeiadis.
A separation logic for a promising semantics.
In {\em \textbf{{ESOP 2018}}}, 2018.

\bibitem[UCAM-CL-TR-907]{UCAM-CL-TR-907}
Robert N.~M. Watson, Peter~G. Neumann, Jonathan Woodruff, Michael Roe, Jonathan
Anderson, John Baldwin, David Chisnall, Brooks Davis, Alexandre Joannou, Ben
Laurie, Simon~W. Moore, Steven~J. Murdoch, Robert Norton, Stacey Son, and
Hongyan Xia.
{Capability Hardware Enhanced RISC Instructions: CHERI
Instruction-Set Architecture (Version 6)}.
Technical Report UCAM-CL-TR-907, University of Cambridge, Computer
Laboratory, April 2017.

\bibitem[Watt:2018:MVW:3176245.3167082]{Watt:2018:MVW:3176245.3167082}
Conrad Watt.
Mechanising and verifying the {WebAssembly} specification.
In {\em \textbf{CPP 2018}: Proceedings of the 7th ACM SIGPLAN
International Conference on Certified Programs and Proofs}, CPP 2018, pages
53--65, New York, NY, USA, 2018. ACM.
\begin{quote} {\bf Abstract:} WebAssembly is a new low-level language
currently being implemented in all major web browsers. It is designed to
become the universal compilation target for the web, obsoleting existing
solutions in this area, such as asm.js and Native Client. The WebAssembly
working group has incorporated formal techniques into the development of the
language, but their efforts so far have focussed on pen and paper formal
specification. We present a mechanised Isabelle specification for the
WebAssembly language, together with a verified executable interpreter and
type checker. Moreover, we present a fully mechanised proof of the soundness
of the WebAssembly type system, and detail how our work on this proof has
exposed several issues with the official WebAssembly specification,
influencing its development. Finally, we give a brief account of our efforts
in performing differential fuzzing of our interpreter against industry
implementations. \end{quote}

\bibitem[YALLOP2017]{YALLOP2017}
Jeremy Yallop, David Sheets, and Anil Madhavapeddy.
A modular foreign function interface.
{\em \textbf{Science of Computer Programming}}, April 2017.
\begin{quote} {\bf Abstract:} Abstract foreign function interfaces
are typically organised monolithically, tying together the specification of
each foreign function with the mechanism used to make the function available
in the host language. This leads to inflexible systems, where switching from
one binding mechanism to another (say from dynamic binding to static code
generation) often requires changing tools and rewriting large portions of
code. We show that ML-style module systems support exactly the kind of
abstraction needed to separate these two aspects of a foreign function
binding, leading to declarative foreign function bindings that support
switching between a wide variety of binding mechanisms -- static and dynamic,
synchronous and asynchronous, etc. -- with no changes to the function
specifications. Note. This is a revised and expanded version of an earlier
paper, Declarative Foreign Function Binding Through Generic Programming. This
paper brings a greater focus on modularity, and adds new sections on error
handling, and on the practicality of the approach we describe. \end{quote}

\bibitem[armv8-mca]{armv8-mca}
Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, and
Peter Sewell.
{Simplifying ARM Concurrency: Multicopy-atomic Axiomatic and
Operational Models for ARMv8}.
In {\em \textbf{POPL 2018}}, pages 19:1--19:29, January 2018.
\begin{quote} {\bf 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. \end{quote}

\bibitem[gomes-oopsla2017]{gomes-oopsla2017}
Victor B.~F. Gomes, Martin Kleppmann, Dominic~P. Mulligan, and Alastair~R.
Beresford.
Verifying strong eventual consistency in distributed systems.
In {\em \textbf{OOPSLA 2017}: Proceedings of the {ACM} {SIGPLAN}
International Conference on Object-Oriented Programming, Systems, Languages,
and Applications ({OOPSLA})}, pages 109:1--109:28, October 2017.
Distinguished Paper award.
\begin{quote} {\bf Abstract:} Data replication is used in distributed
systems to maintain up-to-date copies of shared data across multiple
computers in a network. However, despite decades of research, algorithms for
achieving consistency in replicated systems are still poorly understood.
Indeed, many published algorithms have later been shown to be incorrect, even
some that were accompanied by supposed mechanised proofs of correctness. In
this work, we focus on the correctness of Conflict-free Replicated Data Types
(CRDTs), a class of algorithm that provides strong eventual consistency
guarantees for replicated data. We develop a modular and reusable framework
in the Isabelle/HOL interactive proof assistant for verifying the correctness
of CRDT algorithms. We avoid correctness issues that have dogged previous
mechanised proofs in this area by including a network model in our
formalisation, and proving that our theorems hold in all possible network
behaviours. Our axiomatic network model is a standard abstraction that
accurately reflects the behaviour of real-world computer networks. Moreover,
we identify an abstract convergence theorem, a property of order relations,
which provides a formal definition of strong eventual consistency. We then
obtain the first machine-checked correctness theorems for three concrete
CRDTs: the Replicated Growable Array, the Observed-Remove Set, and an
Increment-Decrement Counter. We find that our framework is highly reusable,
developing proofs of correctness for the latter two CRDTs in a few hours and
with relatively little CRDT-specific code. \end{quote}

\bibitem[kell:some:2017]{kell:some:2017}
Stephen Kell.
Some were meant for {C}: the endurance of an unmanageable language.
In {\em \textbf{Onward! 2017}: Proceedings of the 2017 ACM
International Symposium on New Ideas, New Paradigms, and Reflections on
Programming \& Software}, Onward! 2017, New York, NY, USA, October 2017. ACM.
\begin{quote} {\bf Abstract:} The C language leads a double life: as
an application programming language of yesteryear, perpetuated by
circumstance, and as a systems programming language which remains a weapon of
choice decades after its creation. This essay is a C programmer's reaction to
the call to abandon ship. It questions several properties commonly held to
define the experience of using C; these include unsafety, undefined
behaviour, and the motivation of performance. It argues all these are in fact
inessential; rather, it traces C's ultimate strength to a communicative
design which does not fit easily within the usual conception of ``a
programming language'', but can be seen as a counterpoint to so-called
``managed languages''. This communicativity is what facilitates the essential
aspect of system-building: creating parts which interact with other, remote
parts---being ``alongside'' not ``within''. \end{quote}

\bibitem[matache-aplas2017]{matache-aplas2017}
Cristina Matache, Victor B.~F. Gomes, and Dominic~P. Mulligan.
Programming and proving with classical types.
In {\em \textbf{APLAS 2017}: Proceedings of the 15th {Asian}
Symposium on Programming Languages and Systems}, November 2017.
\begin{quote} {\bf Abstract:} The propositions-as-types
correspondence is ordinarily presented as linking the metatheory of typed
$\lambda $-calculi and the proof theory of intuitionistic logic. Griffin
observed that this correspondence could be extended to classical logic
through the use of control operators. This observation set off a flurry of
further research, leading to the development of Parigot's $\lambda \mu
$-calculus. In this work, we use the $\lambda \mu $-calculus as the
foundation for a system of proof terms for classical first-order logic. In
particular, we define an extended call-by-value $\lambda \mu $-calculus with
a type system in correspondence with full classical logic. We extend the
language with polymorphic types, add a host of data types in `direct style',
and prove several metatheoretical properties. All of our proofs and
definitions are mechanised in Isabelle/HOL, and we automatically obtain an
interpreter for a system of proof terms cum programming language---called
$\mu $ML---using Isabelle's code generation mechanism. Atop our proof terms,
we build a prototype LCF-style interactive theorem prover---called $\mu
$TP---for classical first-order logic, capable of synthesising $\mu $ML
programs from completed tactic-driven proofs. We present example closed $\mu
$ML programs with classical tautologies for types, including some
inexpressible as closed programs in the original $\lambda \mu $-calculus, and
some example tactic-driven $\mu $TP proofs of classical tautologies.
\end{quote}

\end{thebibliography}
Exploitation Route Please see above
Sectors Aerospace, Defence and Marine,Digital/Communication/Information Technologies (including Software),Electronics,Security and Diplomacy

URL http://www.cl.cam.ac.uk/users/pes20/rems
 
Description Clarification of the behaviour of multiprocessors, programming languages, and security protocols
First Year Of Impact 2014
Sector Digital/Communication/Information Technologies (including Software),Electronics
Impact Types Economic

 
Title Research data supporting "Dynamically Diagnosing Type Errors in Unsafe Code" 
Description Buildable source code of the libcrunch system and related codebases, within a Debian 8.5 (Jessie) distribution, packaged as a VirtualBox virtual machine image. 
Type Of Material Database/Collection of data 
Year Produced 2017 
Provided To Others? Yes