一句话：提出首个针对同一程序多次执行任意超属性的演绎验证技术，并实现工具 Hypra。
超属性刻画程序多次执行之间的关系，可表达确定性、非干扰等正确性与安全性性质。已有超属性程序逻辑强大，但自动化落后：多数演绎验证工具仅支持安全性质，难以推理执行存在性；其他工具虽支持广义非干扰等更灵活超属性，却受限于程序与证明结构。本文提出针对同一程序多次执行任意超属性的首个演绎验证技术，自动化生成 Hyper Hoare Logic 的验证条件。关键思想是将任意超属性及证明规则编码到标准中间验证语言中：在中间程序状态中显式表示原程序的状态集合，再借助现有基于 SMT 的验证器完成验证。作者实现 Hypra，并实验表明其能可靠验证复杂超属性。
Hyperproperties relate multiple executions of a program and are useful to express common correctness properties (such as determinism) and security properties (such as non-interference). While there are a number of powerful program logics for the deductive verification of hyperproperties, their automation falls behind. Most existing deductive verification tools are limited to safety properties, but cannot reason about the existence of executions, for instance, to prove the violation of a safety property. Others support more flexible hyperproperties such as generalized non-interference, but have limitations in terms of the programs and proof structures they support. In this paper, we present the first deductive verification technique for arbitrary hyperproperties over multiple executions of the same program. Our technique automates the generation of verification conditions for Hyper Hoare Logic. Our key insight is that arbitrary hyperproperties and the corresponding proof rules can be encoded into a standard intermediate verification language by representing sets of states of the input program explicitly in the states of the intermediate program. Verification is then automated using an existing SMT-based verifier for the intermediate language. We implement our technique in a tool called Hypra and demonstrate that it can reliably verify complex hyperproperties.
@article{DardinierL024,
title = {Hypra: A Deductive Program Verifier for Hyper Hoare Logic},
author = {Thibault Dardinier and Anqi Li and Peter Müller},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA2},
year = {2024},
doi = {10.1145/3689756}
}