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