REMS: Rigorous Engineering for Mainstream Systems

Project

How can we use rigorous maths to improve the quality of mainstream computer systems? REMS (Rigorous Engineering for Mainstream Systems), is a 6-year EPSRC-funded Programme Grant (EP/K008528/1) to do just that, bringing together an exciting combination of researchers in systems (architecture, operating systems, and networks) and in semantics (programming languages, automated reasoning, and verification) at Cambridge, Imperial, and Edinburgh.

We're finally in a position to scale up and apply mathematically rigorous semantics to mainstream systems:

The project is focussed on lightweight rigorous methods, rather than full verification everywhere: precise specification (post hoc and during design) and testing against specifications, with full verification only where that is feasible. The project emphasises building useful (and reusable) semantics and tools. We want to understand how to build accurate full-scale mathematical models of some of the key computational abstractions (processor architectures, programming languages, and concurrent OS interfaces), and how these can be used for new verification research, to build tools that are applicable to real systems, and to enable new systems and programming language research. Supporting all this, we are also working on new specification tools and their foundations.

People

Investigators, at Cambridge: Jon Crowcroft, Mike Gordon, Steve Hand, Simon Moore, Andrew Pitts, Peter Sewell (PI); at Imperial: Philippa Gardner; and at Edinburgh: Ian Stark.

Also involved in the proposal are, at Cambridge: Anil Madhavapeddy, Magnus Myreen, and Robert Watson; together with Mike Dodds (York), Susmit Sarkar (St. Andrews), Scott Owens (Kent), and Brian Campbell (Edinburgh).

The industrial partners include ARM, IBM, Microsoft Research, and the FreeBSD foundation, and academic partners include INRIA (Maranget, Zappa Nardelli), U. Pennsylvania (Pierce, Weirich, Zdancewic), Purdue University (Jagannathan, Vitek), and U. Texas Austin (Hunt).

Project Outline

There are four Tasks:

Context

REMS builds on a range of recent work and current projects spanning theory and practice by the investigators and their colleagues, including:

Summary

Here is the informal summary from the proposal:

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.