SAFER - Secure Foundations: Verified Systems Software Above Full-Scale Integrated Semantics
Lead Research Organisation:
University of Cambridge
Department Name: Computer Science and Technology
Abstract
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
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
People |
ORCID iD |
| Peter Sewell (Principal Investigator) |