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