REMS: Rigorous Engineering for Mainstream Systems

计算机系统对现代社会至关重要，从嵌入式设备和移动电话到互联网服务，但传统的计算机工程无法产生可靠和安全的系统，正如我们从影响各地行业和消费者的源源不断的错误和安全漏洞中看到的那样。行业依赖非正式的描述规范和特殊测试，但当今系统的复杂性和规模使得仅使用这些方法排除错误实际上是不可能的(即使主要供应商中可能有70%的开发人员致力于测试)，而敌意利用往往会将错误转变为主要的安全问题，并带来巨大的经济和社会成本。使问题雪上加霜的是，构建真实系统所围绕的整个行业的抽象，包括多处理器硬件和软件之间的体系结构接口，以及C和C++等编程语言，定义不明确，导致歧义和错误。这是一个长期存在的问题，促使人们对数学上严格的替代方案进行广泛研究。到目前为止，用严格的技术解决主流的广泛部署的系统是不切实际的。相反，学术研究集中在适度规模的安全关键系统和理想化系统的学术验证上。一方面，实际工业工程和系统研究与语义、验证和基础方面的理论研究之间存在着严重的脱节。然而，现在，我们拥有的新方法，加上务实地强调使用最有效的数学严格模型，最终使解决工业规模的系统成为可能-而不这样做的商业和社会成本正在变得越来越大。现在是时候对主流系统进行严格的工程设计，统一实践和理论。REMS将一支领先的理论和系统研究人员团队与关键的行业合作伙伴聚集在一起，建立一个新的综合体。我们将为构建更健壮和安全的计算机系统建立真正的工程数学：应用于构建全面主流计算机系统的严格数学模型、验证技术和工程工具，包括当今广泛使用的关键基础设施(多处理器、编程语言和操作系统)。我们将把这一点与新的编程语言和验证支持结合起来，为未来的系统建设提供支持。通过发展我们最近与处理器供应商和语言标准机构的合作，我们将解决将这些技术广泛使用所需的技术、工程和社会挑战，使整个计算机工程得到根本改善。

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.