Compilers that Preserve and Enforce Invariants and Proofs

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

• 批准号: RGPIN-2019-04207
• 负责人: Bowman, William
• 金额: $ 2.4万
• 依托单位: 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=737482
• 关键词: 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”这样的错误。本研究计划将设计和开发新的编译器，将依赖类型的程序转换为机器代码，同时保留不变式和证明。通过使编译器保留更多程序员的想法，我们提高了所有程序的可靠性。在短期内，这项研究可以通过提供自动排除错误类别的工具来降低高保证软件的成本，例如在汽车和医疗设备中运行的软件。从长远来看，这项工作可以降低成本，提高从游戏到科学计算的各种软件的性能，允许开发人员在编译器生成有效的机器代码时更好地与编译器进行通信。