Deductive Verification Across the Stack

最新进展与文献综述 软件渗透到现代社会的方方面面，确保其可靠性对个人安全、数据安全、生产力和商业利润至关重要。然而，软件可靠性仍然是一个巨大的挑战。现代软件项目的规模、复杂性和并发性不断增加，使得传统的基于测试的方法无法有效地消除所有关键错误，这些错误只有在非常特定和罕见的情况下才会出现。 学术研究提供了一个诱人的替代方案：形式验证可以提供经过数学验证的保证，即执行特定代码的所有方法都将按预期执行。通过让程序员提供规范及其实现的代码，可以捕捉到意图的概念。然而，适用于现代软件的验证技术成本极高：所采用的数学形式是复杂和困难的，使用这些技术手动构建证明是一项仅由专家完成的耗时的任务。 目标、方法和HQP 我的长期研究目标是将形式验证的力量应用到实用工具中，专家软件开发人员可以使用这些工具来保证他们代码的正确性。这些将是演绎验证工具，需要低和可预测的代码注释程度(程序员意图的规范)，并将逐步数学证明的构造或拒绝委托给建立在高度自动化的逻辑工具(如SMT解算器)上的工具堆栈。开发的工具将提供深层语义性质的早期反馈，在软件部署之前暴露概念性错误和意外场景。 实现这一愿景需要解决一系列复杂的技术和实际研究挑战。我提出了四个相辅相成的目标，旨在实现对广泛类别的编程任务的验证，特别是针对系统编程。这些目标是：1.开发用于更简单的规范和验证的能力类型系统，2.用于补充部分程序规范的静态分析技术，3.分解验证问题以针对多个自动求解器，以及4.用程序分析技术理解有问题的求解器行为。我计划培养两名博士生和两名硕士生，每个人都以这些目标中的一个为目标，并辅之以本科项目。 影响 每个目标都有可能显著提高当前程序验证的最先进水平。我们的工作成果将通过与行业专家的合作进行评估，我们还将从他们那里获得关于他们日常遇到的代价高昂的实际问题的宝贵指导。我将引导这些努力，以最大限度地影响学术验证社区，以及从事关键系统软件工作的工业从业者。

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.