Deductive Verification Across the Stack

跨堆栈的演绎验证

• 批准号: RGPIN-2020-06072
• 负责人: Summers, Alexander
• 金额: $ 2.91万
• 依托单位: University of British Columbia
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2022
• 资助国家: 加拿大
• 起止时间: 2022-01-01 至 2023-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=749923
• 关键词: 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 Solvers）的工具堆栈中。开发的工具将提供深层语义性质的早期反馈，在软件部署之前，暴露出概念错误和意外情况。意识到这一愿景需要解决各种技术和实践研究挑战的解决方案。我提出了四个完整的对象，旨在验证广泛的编程任务，特别针对系统编程。这些目标是：1。利用功能类型系统以进行简单规格和验证，2。用于综合部分程序规范的静态分析技术，3。将验证问题分解为目标多个自动求解器，以及4。使用程序分析技术了解有问题的求解器行为。我计划为两名博士生和两个硕士的学生指定这些目标之一，该目标是由本科项目完成的。影响每个目标都有可能显着改善程序验证中最新的最新技术。我们的工作结果将通过与行业专家的合作进行评估，我们还将从中获得有关他们日常遇到的昂贵实践问题的宝贵指导。我将引导这些努力，以最大程度地影响学术验证社区以及从事自己的关键系统软件的工业实践者。