Deductive Verification Across the Stack

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

Recent Progress and Literature Software pervades all aspects of modern society, and ensuring its reliability is critical for personal safety, data security, productivity and business profits. However, software reliability remains a massive challenge. The increasing scale, complexity and concurrency of modern software projects renders traditional testing-based approaches ineffective for eliminating all critical bugs, which may only arise under very specific and rare circumstances. Academic research offers a tantalising alternative: formal verification can provide mathematically-proven guarantees that all ways to execute a certain piece of code will perform as intended. The notion of what is intended can be captured by having the programmer provide specifications along with their implemented code. Yet verification techniques applicable to modern software come at an extremely high cost: the mathematical formalisms employed are complex and difficult, and manual construction of proofs using these techniques is a time-consuming experts-only task. Objectives, Methodology and HQP My long-term research objective is to bring the power of formal verification to bear in practical tools which expert software developers can use themselves to guarantee the correctness of their code. These will be deductive verification tools, requiring low and predictable degrees of code annotation (specifications of the programmer's intentions), and delegating the construction or rejection of a step-by-step mathematical proof to a tool stack built upon highly-automated logic tools such as SMT solvers. The developed tools will provide early feedback of a deep semantic nature, exposing conceptual mistakes and unintended scenarios before the software is ever deployed. Realising this vision requires solutions to a complex array of technical and practical research challenges. I propose four complementary objectives designed to enable verification for a wide class of programming tasks, targeting systems programming in particular. These objectives are: 1. exploiting capability type systems for simpler specification and verification, 2. static analysis techniques for complementing partial program specifications, 3. decomposing verification problems to target multiple automatic solvers, and 4. understanding problematic solver behaviour with program analysis techniques. I plan for two doctoral students and two Master's students to each target one of these objectives, complemented by undergraduate projects. Impact Each objective has the potential to significantly improve the current state-of-the-art in program verification. The outcomes of our work will be evaluated through collaboration with industry experts, from whom we will also obtain valuable guidance on the costly practical problems they encounter day-to-day. I will steer these efforts to maximise impact both on the academic verification community, and on industrial practioners working on critical systems software of their own.