Beluga: Building Trustworthy Software Systems through Programming Proofs

软件系统是我们基础设施不可或缺的一部分，我们越来越依赖它们：软件管理我们的金融资产，协助驾驶我们的汽车，并在电子投票中发挥核心作用。与此同时，安全漏洞和计算错误可能导致我们的基础设施大规模中断和服务中的安全关键故障。因此，确保软件系统更值得信赖和可靠不仅对计算行业的持续成功至关重要，而且对我们的经济和整个社会都至关重要。 在过去十年中，我们通过验证软件组件是否符合正式的安全策略，并消除可能导致编译器和操作系统中的安全漏洞和计算错误的软件“错误”，在构建可信赖的计算基础设施方面取得了重大进展。然而，验证的成本仍然过高，我们往往集中在建立只有浅的顺序程序的安全保证。我的研究的目标是开发一个类型理论的基础，用于验证顺序，分布式和反应式程序的深层属性，为常见和重复出现的概念提供抽象和原语，并使机械化模块化，更容易维护和重用。这可能会对机械化的工作和成本产生重大影响：通过分解和抽象低级别的官僚细节，它减少了原型化正式系统及其元理论的时间，并避免了操纵低级别操作的错误。更重要的是，它可以对自动验证产生重大影响。 具体地说，我们计划解决三个主要的研究挑战：1）扩展现有的类型理论基础，以便能够验证有关顺序程序的深层属性，例如完全抽象，这表明两个组件在任何有效的程序上下文中都是不可区分的。2)开发一个基础，以建立有关旨在连续运行的程序的属性，即分布式和反应式系统。3)设计和开发工具，尽可能多地自动进行证明，使程序员能够指定和自动验证程序的复杂属性，因为手工编写证明很快就会让程序员不知所措。 我的长期目标是降低验证的成本，使通信、交换和验证证明成为常见的做法，以确保软件的可靠性和安全性。这对于构建值得信赖和可靠的计算基础设施至关重要。

Software systems are an integral part of our infrastructure and we are increasingly dependent on them: Software manages our financial assets, assists in driving our cars, and plays a central role in electronic voting. At the same time, security vulnerabilities and computing errors can lead to massive disruptions of our infrastructure and safety-critical failures in services. Thus, ensuring that software systems are more trustworthy and reliable is not only essential to the continued success of the computing industry, but to our economy and society at large. Over the past decade we have made significant progress towards building a trustworthy computing infrastructure by verifying compliance of software components with a formal safety policy and eliminating software "bugs" that can lead to security vulnerabilities and computing errors in compilers and operating systems. However, the cost of verification remains exorbitantly high and we often concentrate on establishing only shallow safety guarantees about sequential programs. The objective of my research is to develop a type-theoretic foundation for verifying deep properties about sequential, distributed, and reactive programs that provides abstractions and primitives for common and recurring concepts and makes mechanizations modular, and easier to maintain and reuse. This can have a major impact on the effort and cost of mechanization: By factoring and abstracting over low-level bureaucratic details, it reduces the time to prototype formal systems and their meta-theory, and avoids errors in manipulating low-level operations. More importantly, it can make a substantial difference to automatic verification. Concretely, we plan to address three major research challenges: 1) Extend the existing type-theoretical foundation to be able to verify deep properties about sequential programs such as full abstraction, which states that two components are indistinguishable in any valid program context. 2) Develop a foundation to establish properties about programs that are intended to run continuously, i.e. distributed and reactive systems. 3) Design and develop tools that automatically discharge as many proofs as possible to make it routine work for programmers to specify and automatically verify complex properties of their programs, as writing out proofs by hand can quickly become overwhelming to programmers. My long-term goal is to bring down the cost of verification and make it common practice to communicate, exchange, and verify proofs to ensure that software is reliable and safe. This is essential to building a trustworthy and reliable computing infrastructure.