Logical Relations for Program Verification

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

In an economy as relentlessly digital as the modern worldwide one, inwhich everything from toasters to interpersonal communications toglobal financial services are computerised, the need for formallyverified software cannot be overestimated. Formal verification usesmathematical techniques to prove that programs actually perform thecomputations they are intended to perform (e.g., that text editorsreally do save files when a SAVE command is issued or that automaticpilots really do correctly execute flight plans) and also avoidperforming unintended ones (e.g., leaking credit card details orlaunching nuclear weapons without authorisation). Since programmersmake 15 to 50 errors per 1000 lines of code, and since repairing themaccounts for some 80% of project expenses, the ever-increasing sizeand sophistication of programs makes formal verification increasinglycritical to modern software development.Mathematical reasoning lies at the core of all formal verification,and so is crucial for building truly secure and reliable software.One of the key techniques for formally verifying properties ofsoftware systems uses logical relations. Logical relations provide ameans of deriving properties of a software system directly from thesystem itself; as a result, they can be used to prove importantproperties of programs, programming languages, and languageimplementations. Logical relations have been developed for corefragments of many modern programming languages and verificationsystems. They are currently extended to richer programming languagesand properties by constructing plausible variants of the definitionsof logical relations for appropriate core fragments and checking thatthe mathematical theory goes through. But as languages and propertiesto be proved have become increasingly sophisticated and expressive,this ad hoc approach has become both difficult and unsustainable. Ithas also led to an enormous constellation of complicated andnon-reusable logical relations that "work" for particular languagefeatures, rather than their principled and transferrable developmentfrom fundamental principles. In short, logical relations havestruggled to keep pace with developments in programming languages,with the obvious consequences for security and reliability of softwaresystems.We aim to revolutionise the landscape of logical relations byproviding framework for their development and use that is principled,conceptually simple, reusable, and uniform (rather than ad hoc). Ourframework will be capable of both describing the wide array of logicalrelations already used in existing applications and prescribing newlogical relations for future ones. It will be based on themathematical concept of comprehension for a fibration, which has not previously been identified as a key ingredient inthe construction of logical relations. Our use of it thusdistinguishes our framework from all other treatments of logicalrelations in the literature. Comprehension allows explicit representation of logical properties oflanguages within those languages themselves. This means that ourframework will be implementable, so we will produce a logic forderiving consequences of logical relations and a prototypeimplementation of that logic in a modern interactive theoremprover. This will allow users to experiment with our framework, andallow their experiences with it to feed back into itsfoundations. We will also apply our new framework for logicalrelations to cutting-edge problems that are the focus of activeresearch and for which there is presently no consensus on the wayforward. Successful application of our framework will show that it cansolve problems that are the focus of active research, aswell as open up unanticipated new research directions. Conversely, thepractical applications we pursue will raise challenges that prompt usto further refine its foundations