We introduce a novel logic for the specification of context-free hyperproperties, which capture, e.g., the flow of information in security-critical recursive systems. Intuitively, the logic extends visibly pushdown automata by quantification over traces, just like HyperLTL, the most important logic for regular hyperproperties, extends LTL by quantification over traces. Using a game-based approach, we show that model-checking is decidable for formulas with a single quantifier alternation, provided the stack height of the visibly pushdown automaton only depends on the traces bound to the variables of the first quantifier block. A single quantifier alternation suffices to express many information-flow properties studied in the literature. Complementarily, we show that model-checking is undecidable for formulas with a single quantifier alternation, if the stack behavior of the visibly pushdown automaton may depend on the second quantifier block. This also implies that model-checking is undecidable for almost all fragments with more than one quantifier alternation.

翻译：我们提出了一种用于指定上下文自由超性质的新逻辑，该类性质能够捕获诸如安全关键递归系统中的信息流等行为。直观而言，该逻辑通过迹量化扩展了可见下推自动机，正如正则超性质最重要的逻辑HyperLTL通过迹量化扩展了LTL。基于博弈方法，我们证明：对于仅包含单一量词交替的公式，若能见下推自动机的栈高度仅依赖于绑定到第一个量词块变量的迹，则模型检测是可判定的。单一量词交替足以表达文献中研究的诸多信息流性质。作为补充，我们证明：若能见下推自动机的栈行为可能依赖于第二个量词块，则包含单一量词交替的公式的模型检测是不可判定的。这一结果也意味着几乎所有包含多于一个量词交替的子句的模型检测均不可判定。