Beluga: Building Trustworthy Software Systems through Programming Proofs

点击翻译按钮获取中文摘要

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