Beluga: Building Trustworthy Software Systems through Programming Proofs

Beluga：通过编程证明构建值得信赖的软件系统

• 批准号: RGPIN-2017-03895
• 负责人: Pientka, Brigitte
• 金额: $ 1.68万
• 依托单位: McGill University
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2019
• 资助国家: 加拿大
• 起止时间: 2019-01-01 至 2020-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=679162
• 关键词: Beluga; Building; Trustworthy; Software; Systems

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

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