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 和手机等日常设备出现故障也会带来不便和令人沮丧，但软件泄露信用卡详细信息或投票记录、导致飞机坠毁、未经授权发射核武器或危及全球金融部门可能会导致前所未有的、明显不可接受的后果。全球不确定性。程序的规模和复杂性不断增长，使得形式验证方法（使用数学技术来确保程序实际执行其设计的计算而不是执行意外的计算）对于构建真正安全和可靠的系统变得越来越重要。可靠的软件。这项研究更广泛的影响是使开发更好、更广泛适用的形式化程序验证方法成为可能，从而帮助确保即使是大型和复杂的软件系统也能被证明是正确的。关系参数性是形式化验证的关键技术软件系统的属性。关系参数性所基于的逻辑关系提供了一种直接从系统本身证明软件系统属性的方法。迄今为止，许多现代编程语言和验证系统的核心片段已经开发出逻辑关系。然而，这是通过大量复杂且不可重用的逻辑关系来实现的，而不是通过从基本原则上诉诸它们的统一构造和可移植发展来实现的。这项研究旨在通过为逻辑关系的构建提供公理化框架来改进当前的最新技术。该框架原则性强、概念简单、全面、统一且具有预测性。这项研究的智力价值在于它对范畴论（“纤维”）的基本结构的阐述和使用，以解决构建逻辑关系以及在复杂环境中概念化关系参数性的重大技术问题。它还在于本研究将导致参数化的新颖且统一的表述，以及将这种新框架应用于特定的最先进的计算问题。为了确保其被采用，将为新框架提供逻辑和工具支持。虽然该工具将允许用户试验该框架，但他们的实践经验的反馈将进一步巩固参数化的新基础。