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

软件系统是我们基础架构不可或缺的一部分，我们越来越依赖它们：软件管理我们的金融资产，有助于驾驶汽车，并在电子投票中发挥着核心作用。同时，安全漏洞和计算错误可能会导致我们的基础架构和服务关键性失败的大规模中断。因此，确保软件系统更具值得信赖和可靠性不仅对计算行业的持续成功至关重要，而且对我们的经济和整个社会的持续成功至关重要。但是，验证的成本仍然高昂，我们通常专注于建立有关顺序程序的浅安全保证。我的研究的目的是为验证有关顺序，分布式和反应性程序的深层属性开发一种类型的理论基础，该程序为共同和重复的概念提供了抽象和原始词，并使机械化模块化，并且更易于维护和重复使用。这可能会对机械化的努力和成本产生重大影响：通过在低级官僚细节上考虑和抽象，它减少了原型正式系统及其元理论的时间，并避免了操纵低级操作的错误。更重要的是，它可以对自动验证产生实质性的差异。 2）建立一个基础，以建立旨在连续运行的程序的属性，即分布式和反应性系统。 3）设计和开发工具，这些工具会自动放电尽​​可能多的证据，以使程序员为程序指定和自动验证其程序的复杂属性，因为手工写出证据很快就会对程序员施加压倒性。 ******我的长期目标是降低验证成本，并使沟通，交换和验证证明以确保软件可靠且安全。这对于建立可信赖且可靠的计算基础架构至关重要。 **