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

点击翻译按钮获取中文摘要

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