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.