Compilers that Preserve and Enforce Invariants and Proofs

保留并强制执行不变量和证明的编译器

• 批准号: RGPIN-2019-04207
• 负责人: Bowman, William
• 金额: $ 2.4万
• 依托单位: 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=749781
• 关键词: Compilers; Preserve; Enforce; Invariants; Proofs

The goal of this program is to make software more reliable by designing new software development tools that provide guarantees about the machine code used to implement all programs. We rely on software to control everything from spacecraft to pacemakers. This means even simple software errors, such as mistaking a number in imperial units for a number in metric, cause millions of dollars in damages and cost lives. The field of high-assurance software seeks to prevent software errors, but the process is costly and time consuming. This research program will simplify high-assurance software development by creating new tools that automatically rule out whole classes of errors in machine code. Machine code is usually generated from programming languages that simplify software development by hiding the details of how computers execute 0s and 1s. For example, we think about numbers in decimal, the digit 0--9, while computers represent numbers as sequences of 0 and 1 such as "101" (the number "5"). A compiler is a program generates machine code, e.g., translates "5" into "101". Languages often provide tools for reasoning about invariants---properties of a program that must always be true for the program to be correct. For example, some languages can prevent a program from using the imperial unit "5 ft" when a metric unit "5 m" is expected (which would have prevented the Mars Climate Orbiter disaster and saved $300 million). In these languages, the compiler checks that the invariant holds before trying to generate machine code. A few languages, such as so-called dependently typed languages, allow the programmer to encode program invariants and proofs of correctness. Writing invariants and proofs requires extra work at first, but allows the programmer to prove that their program is safe, secure, and correct. This is necessary since, in general, we cannot automatically check arbitrary invariants, but we can check programmer provided proofs. Unfortunately, compilers for dependently typed languages do not preserve all the invariants programmers can express. So for example, while "5 ft" and "5 m" are different, the compiler will translate both to "101", allowing errors like "5 ft + 5 m = 10" even in a "proven correct" program. This research program will design and develop new compilers that translate dependently typed programs into machine code while preserving invariants and proofs. By making compilers preserve more of what a programmer is thinking, we improve the reliability of all programs. In the short-term, this research can reduce the cost of high-assurance software, such as the software running in cars and medical devices, by providing tools to automatically rule out classes of errors. In the long-term, this work can reduce the cost and improve the performance of a broad range of software, from games to scientific computations, by allowing developers to better communicate with the compiler as it generates efficient machine code.

该计划的目标是通过设计新的软件开发工具来提高软件的可靠性，这些工具为用于实现所有程序的机器代码提供保证。我们依靠软件来控制从航天器到起搏器的一切。这意味着即使是简单的软件错误，例如将英制单位的数字误认为公制单位的数字，也会造成数百万美元的损失和生命损失。高可靠性软件领域致力于防止软件错误，但该过程成本高昂且耗时。该研究计划将通过创建自动排除机器代码中所有类别错误的新工具来简化高保证软件开发。机器代码通常由编程语言生成，这些编程语言通过隐藏计算机如何执行 0 和 1 的细节来简化软件开发。例如，我们认为十进制数字是数字 0--9，而计算机将数字表示为 0 和 1 的序列，例如“101”（数字“5”）。编译器是生成机器代码的程序，例如将“5”翻译为“101”。语言通常提供用于推理不变量的工具——程序的属性必须始终为真，程序才能正确。例如，某些语言可以阻止程序在预期使用公制单位“5 m”时使用英制单位“5 ft”（这可以防止火星气候轨道器灾难并节省 3 亿美元）。在这些语言中，编译器在尝试生成机器代码之前会检查不变量是否成立。一些语言，例如所谓的依赖类型语言，允许程序员对程序不变量和正确性证明进行编码。编写不变量和证明一开始需要额外的工作，但允许程序员证明他们的程序是安全的、可靠的和正确的。这是必要的，因为一般来说，我们不能自动检查任意不变量，但我们可以检查程序员提供的证明。不幸的是，依赖类型语言的编译器不能保留程序员可以表达的所有不变量。例如，虽然“5 ft”和“5 m”不同，但编译器会将两者转换为“101”，即使在“已证明正确”的程序中也允许出现“5 ft + 5 m = 10”之类的错误。该研究计划将设计和开发新的编译器，将依赖类型的程序转换为机器代码，同时保留不变量和证明。通过让编译器更多地保留程序员的想法，我们提高了所有程序的可靠性。从短期来看，这项研究可以通过提供自动排除错误类别的工具来降低高保证软件（例如在汽车和医疗设备中运行的软件）的成本。从长远来看，这项工作可以降低成本并提高从游戏到科学计算等各种软件的性能，因为它允许开发人员在编译器生成高效的机器代码时更好地与编译器进行通信。