SHF: Small: Relational Parametricity for Program Verification

SHF：小：程序验证的关系参数

• 批准号: 1420175
• 负责人: Patricia Johann
• 金额: $ 37.71万
• 依托单位: Appalachian State University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2014
• 资助国家: 美国
• 起止时间: 2014-09-15 至 2018-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1420175&HistoricalAwards=false
• 关键词: SHF; Small; Relational; Parametricity; Program

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.

标题：SHF：小：计划验证的关系参数目前估计每年5000亿美元，而且随着软件变得越来越无关紧要，该数字可能会实际上显着增长。软件的一个关键方面是，它是正确的，即，该软件可以执行预期并且没有出错。即使是iPod和手机等日常设备的故障，也令人不安和令人沮丧，但是软件泄漏了信用卡详细信息或投票记录，导致飞机崩溃，无授权发射核武器或损害全球金融部门的核武器可能会导致前所未有的前所未有的，并且明显不可接受的全球不认真。程序的尺寸和成熟的程序使得正式的验证方法使用数学技术来确保程序实际执行其旨在执行和不执行意外的计算，这对于构建真正安全和可靠的软件而言越来越重要。这项研究的更广泛的影响是使得开发更好，更广泛的正式程序验证方法，从而有助于确保即使是大型且复杂的软件系统也是正确的。相关参数是正式验证软件系统属性的关键技术。关系参数基于的逻辑关系提供了一种直接从系统本身证明软件系统属性的方法。到目前为止，已经为许多现代编程语言和验证系统的核心碎片开发了逻辑关系。但是，这是通过庞大的复杂和不可解决的逻辑关系的巨大星座来实现的，而不是通过从基本原则中吸引其统一的构造和可转让的发展。这项研究旨在通过为逻辑关系的建设提供一个公理框架来改善当前的最新框架。该框架是原则上的，在概念上是简单，全面，统一和预测的。这项研究的智力优点在于它的论述和使用类别理论（“纤维”）的基本结构来解决构建逻辑关系的重要技术问题，并概念化复杂设置中的关系参数。它还在于该研究将引起的新颖和统一的参数表述，以及将新框架应用于特定的最新计算问题。为了确保其吸收，将提供对新框架的逻辑和工具支持。尽管该工具将允许用户尝试该框架，但实际经验的反馈将进一步加强新的参数基础。