Logical Relations for Program Verification

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

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