SHF: Small: Relational Parametricity for Program Verification

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

Title: SHF: Small: Relational Parametricity for Program VerificationThe software market is currently estimated at $500 billion per year, and this figure is likely to grow significantly in real terms as software becomes ever more ubiquitous. One crucial aspect of software is that it be correct, i.e., that software does what's intended and does not go wrong. Even failures of everyday devices like iPods and mobile phones are inconvenient and frustrating, but software leaking credit card details or voting records, causing an airplane to crash, launching nuclear weapons without authorization, or compromising the global financial sector can lead to unprecedented and clearly unacceptable global uncertainties. The ever-growing size and sophistication of programs makes formal verification methods --- which use mathematical techniques to ensure that programs actually perform the computations they are designed to carry out and do not perform unintended ones --- increasingly critical for building truly secure and reliable software. The broader impact of this research is to make possible the development of better and more widely applicable formal program verification methods, and, thereby, to help ensure that even large and sophisticated software systems are provably correct.Relational parametricity is a key technique for formally verifying properties of software systems. Logical relations, upon which relational parametricity is based, provide a means of proving properties of a software system directly from the system itself. Logical relations have by now been developed for core fragments of many modern programming languages and verification systems. However, this has been accomplished by way of an enormous constellation of complicated and non-reusable logical relations, rather than by appealing to their uniform construction and transferrable development from fundamental principles. This research aims to improve the current state-of-the-art by providing an axiomatic framework for the construction of logical relations. The framework is principled, conceptually simple, comprehensive, uniform, and predictive. The intellectual merit of this research lies in its exposition and use of essential structures from category theory ("fibrations") to address the significant technical problems of constructing logical relations, and conceptualizing relational parametricity in sophisticated settings. It also lies in the novel and uniform formulation of parametricity to which this research will lead, and the application of this new framework to specific state-of-the-art computational problems. To ensure its uptake, a logic and tool support for the new framework will be provided. While the tool will permit users to experiment with the framework, the feedback from their practical experiences will further fortify the new foundations for parametricity.