Every time you use a banking app, send an encrypted message, or log into a government portal, the operating system underneath is running code that may contain undetected bugs—and those bugs are open doors for attackers. SAFER aims to close those doors by building the first complete, mathematically rigorous models of how real computer architectures actually behave when running systems software like operating systems and hypervisors. Current industry practice relies on testing and debugging, which cannot check every possible execution path in these immensely complex systems. Formal verification—using machine-checked mathematical proof—can guarantee correctness, but until now it has been unable to handle the full scale and subtlety of real-world hardware. SAFER will integrate recent advances in instruction-set semantics, concurrency models, and reasoning methods into a unified mathematical foundation, then build practical analysis and verification tools on top of it. If successful, the project could transform how critical infrastructure software is developed, making it possible to prove that the code running everything from energy grids to cloud servers is free of exploitable flaws—not just likely to be, but mathematically certain.
View original technical description
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
Plain English summaries and category classifications on this site are generated by AI and may not perfectly reflect the original research.
Is something wrong? Let us know