Logical Relations for Program Verification

在一个像现代全球经济一样无情的数字化经济中，从烤面包机到人际交流再到全球金融服务，一切都是计算机化的，对经过正式验证的软件的需求怎么估计都不为过。形式验证使用数学技术来证明程序实际上执行了它们打算执行的计算（例如，文本编辑器在发出SAVE命令时确实保存了文件，或者自动飞行员确实正确地执行了飞行计划），并且还避免执行非预期的操作（例如，泄露信用卡信息或未经授权发射核武器）。由于程序员在每1000行代码中会犯15到50个错误，而且修复这些错误占项目费用的80%左右，因此程序的规模和复杂性的不断增加使得形式化验证对现代软件开发越来越重要。数学推理是所有形式化验证的核心，软件系统性质形式化验证的关键技术之一是逻辑关系。逻辑关系提供了直接从软件系统本身推导软件系统属性的方法;因此，它们可以用来证明程序、编程语言和语言实现的重要属性。许多现代编程语言和验证系统的核心部分都建立了逻辑关系。目前，通过为适当的核心片段构建逻辑关系定义的合理变体并检查数学理论是否通过，它们被扩展到更丰富的编程语言和属性。但是，随着语言和有待证明的属性变得越来越复杂和富有表现力，这种临时的方法变得既困难又不可持续。这也导致了一个巨大的复杂和不可重用的逻辑关系的星座，“工作”的特定语言功能，而不是他们的原则和transferable发展的基本原则。简而言之，逻辑关系一直在努力跟上编程语言的发展步伐，这对软件系统的安全性和可靠性产生了明显的影响。我们的目标是通过为逻辑关系的开发和使用提供原则性的、概念简单的、可重用的和统一的（而不是临时的）框架来彻底改变逻辑关系的面貌。我们的框架将能够描述广泛的逻辑关系已经在现有的应用程序和处方新的逻辑关系为未来的。这将是基于数学概念的理解纤维化，这还没有被确定为一个关键组成部分，在建设的逻辑关系。因此，我们对它的使用将我们的框架与文献中所有其他逻辑关系的处理区分开来。理解允许在这些语言本身内明确地表示语言的逻辑属性。这意味着我们的框架将是可实现的，所以我们将产生一个逻辑推导逻辑关系的后果和一个原型实现的逻辑在现代互动theoremprover。这将允许用户尝试我们的框架，并允许他们的经验反馈到它的基础。我们还将把我们新的逻辑关系框架应用于前沿问题，这些问题是积极研究的焦点，目前还没有就前进方向达成共识。该框架的成功应用表明，它不仅可以解决当前研究的热点问题，而且可以开辟新的研究方向。相反，我们追求的实际应用将带来挑战，促使我们进一步完善其基础

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