Beyond 2-Safety: Asymmetric Product Programs for Relational Program Verification
Beyond 2-Safety: Asymmetric Product Programs for Relational Program Verification
复制标题
超越2-安全性：用于关系程序验证的非对称产品程序
DOI：
10.1007/978-3-642-35722-0_3
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
César Kunz
中科院分区：
文献类型：
--
作者：
G. Barthe;Juan Manuel Crespo;César Kunz
关系Hoare逻辑是Hoare逻辑的概括，允许对两个程序的执行或同一程序的两个执行进行推理。它可以用来验证程序是否稳健或（信息流）安全，并且两个程序在观察方面相当。产品计划提供了一种将关系判断验证验证的方法，以验证（标准）Hoare判断，并开放将标准验证工具应用于关系属性的可能性。但是，针对确定性和结构化程序定义了先前的产品计划概念。此外，这些概念是对称的，不能应用于诸如改进之类的属性，这些属性是不对称的，并且涉及第一个程序的痕迹上的通用量化以及第二个程序痕迹的存在量化。
Relational Hoare Logic is a generalization of Hoare logic that allows reasoning about executions of two programs, or two executions of the same program. It can be used to verify that a program is robust or (information flow) secure, and that two programs are observationally equivalent. Product programs provide a means to reduce verification of relational judgments to the verification of a (standard) Hoare judgment, and open the possibility of applying standard verification tools to relational properties. However, previous notions of product programs are defined for deterministic and structured programs. Moreover, these notions are symmetric, and cannot be applied to properties such as refinement, which are asymmetric and involve universal quantification on the traces of the first program and existential quantification on the traces of the second program.