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. **