Logics for Context-free Hyperproperties

TL;DR

This paper introduces a new logic for specifying context-free hyperproperties, extending visibly pushdown automata with trace quantification, and analyzes its decidability for model-checking.

Contribution

It presents a novel logic for context-free hyperproperties, extending visibly pushdown automata, and provides decidability results for model-checking with a single quantifier alternation.

Findings

Model-checking is decidable with a single quantifier alternation under certain stack height constraints.

Model-checking becomes undecidable if the automaton's stack behavior depends on the second quantifier block.

Almost all fragments with more than one quantifier alternation are undecidable.

Abstract

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.