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

SAFER - 安全基础：高于全面集成语义的经过验证的系统软件

• 批准号: EP/Y035976/1
• 负责人: Peter Sewell
• 金额: $ 269.73万
• 依托单位: University of Cambridge
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2024
• 资助国家: 英国
• 起止时间: 2024 至 无数据
• 项目状态: 未结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FY035976%2F1
• 关键词: SAFER; Secure; Foundations; Verified; Systems

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

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