Proofware: establishing trustworthy computing through programming with proofs

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

Software systems are an integral part of our infrastructure and our society more and more depends on them: Software monitors medical devices, manages our financial assets, and controls power plants. But as consumers take more and more advantage of online services, they are also becoming more concerned about whether their personal information, such as financial and medical records, are kept safe. If computing is to become truly ubiquitous, we will have to make software systems and services sufficiently trustworthy that people do not worry about its fallibility or unreliability the way they do today. Proof-carrying architectures for trustworthy computing advocate establishing trust by verifying compliance of the software with a formal safety policy. However, existing programming environments are inadequate to track and verify complex safety properties about programs. This is a major obstacle for this paradigm to become mainstream. The Proofware project aims to change the way we develop and implement software systems by extending a general purpose programming language with the ability to directly represent, generate, and manipulate proof certificates. The objectives are: Design a foundation for certifying programs based on dependent types, build a proof-of-concept programming environment where proofs are seamlessly integrated into programs, and evaluate its effectiveness in two main areas, certified meta-programming and meta-reasoning. Our goal is twofold: 1) to make it routine work for the programmer to specify and mechanically verify complex behavioral properties of their programs and ensure that these properties are preserved during compilation. 2) to make it common practice to communicate, exchange, and verify proofs to establish trust and guarantee reliability and safety of software systems and services.