SAFER - Secure Foundations: Verified Systems Software Above Full-Scale Integrated Semantics

我们的计算基础设施是现代社会的基础，但它从根本上存在缺陷：可利用的错误使我们所有人在从个人到民族国家的各个层面上不断面临恶意攻击的风险。行业测试和调试开发无法检查这些极其复杂的系统的所有执行路径，因此无法确保没有错误。这对于系统软件尤其重要：操作系统和管理程序使用底层硬件体系结构机制（虚拟内存等）来保护正在运行的程序免受彼此的攻击，因为这些系统中的缺陷会让攻击扩散。这个长期存在的问题促使了对形式化验证和分析的研究，因为机器检查的证明可以提供正确性和安全性的高度保证，但研究落后于主流工程，无法处理真实架构和系统代码的微妙和规模。最近的工作已经在几个方向上朝着这个方向迈出了一大步：我们现在有了全面的指令集语义，用户和系统并发性的许多方面的模型，以及复杂的推理方法——但是我们仍然没有一个集成的数学定义，用于任何主流架构的系统代码的允许行为，或者上面的证明和分析工具。我们现在面临的高层次挑战，以及SAFER的目标，是整合和扩展那些不同的进步，以产生真实世界架构的可用的全尺寸数学模型；开发以上可用于实际系统软件的分析和验证技术；并使这些技术能够在工业中得到更广泛的应用，用数学规范、方法和保证补充现有的实践。最终，这是建立一个更加健壮和安全的计算基础设施的唯一途径，真正使我们更安全，免受对我们的数据和系统的恶意攻击

Our computing infrastructure is fundamental to modern society, but it is fundamentally flawed: exploitable errors expose all of us to continual risk of malicious attack, at every level from the individual to the nation-state. Industry test-and-debug development cannot check all execution paths of these incredibly complex systems, and hence cannot ensure the absence of bugs. This is especially important for systems software: the operating systems and hypervisors that use the underlying hardware-architecture mechanisms (virtual memory, etc.) to protect running programs from each other, as flaws in these let attacks spread. This long-standing problem has prompted research in formal verification and analysis, as machine-checked proof _can_ provide high assurance of correctness and security, but research has lagged behind mainstream engineering, unable to handle the subtleties and scale of real architectures and systems code. Recent work has taken big steps towards this in several directions: we now have full-scale instruction-set semantics, models for many aspects of user and systems concurrency, and sophisticated reasoning methods - but we still do not have an integrated mathematical definition of the allowed behaviour of systems code for any mainstream architecture, or proof and analysis tools above it. The high-level challenge that we now face, and that SAFER targets, is to integrate and extend those disparate advances to produce usable full-scale mathematical models of real-world architectures; to develop analysis and verification techniques above them that can be used in practice for real-world systems software; and to enable transfer of these techniques into more widespread use in industry, complementing existing practice with mathematical specifications, methods, and assurance. Ultimately, this is the only way to establish a substantially more robust and secure computing infrastructure, to truly make us safer from malicious attack on our data and systems