Deductive Verification Across the Stack

跨堆栈的演绎验证

• 批准号: RGPIN-2020-06072
• 负责人: Summers, Alexander
• 金额: $ 2.91万
• 依托单位: University of British Columbia
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2021
• 资助国家: 加拿大
• 起止时间: 2021-01-01 至 2022-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=741014
• 关键词: Deductive; Verification; Across; 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.

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