Hyperproperties relate multiple executions of a program and are commonly used to specify security and information-flow policies. Most existing work has focused on the verification of $k$-safety properties, i.e., properties that state that all $k$-tuples of execution traces satisfy a given property. In this paper, we study the automated verification of richer properties that combine universal and existential quantification over executions. Concretely, we consider $\forall^k\exists^l$ properties, which state that for all $k$ executions, there exist $l$ executions that, together, satisfy a property. This captures important non-$k$-safety requirements, including hyperliveness properties such as generalized non-interference, opacity, refinement, and robustness. We design an automated constraint-based algorithm for the verification of $\forall^k\exists^l$ properties. Our algorithm leverages a sound-and-complete program logic and a (parameterized) strongest postcondition computation. We implement our algorithm in a tool called ForEx and report on encouraging experimental results.

翻译：超属性关联程序的多次执行，常用于指定安全与信息流策略。现有研究主要关注$k$-安全性属性的验证，即所有$k$元执行迹均满足给定属性的断言。本文研究对结合执行全称量化与存在量化的更丰富属性的自动化验证。具体而言，我们考虑$\forall^k\exists^l$属性，该类属性断言：对于任意$k$条执行，均存在$l$条执行使得其整体满足某属性。这涵盖了重要的非$k$-安全性需求，包括广义非干扰性、不透明性、精化与鲁棒性等超活性性质。我们设计了一种基于约束的自动化验证算法，用于检验$\forall^k\exists^l$属性。该算法利用完备可靠的程序逻辑与（参数化）最强后置条件计算。我们在名为ForEx的工具中实现了该算法，并报告了鼓舞人心的实验结果。