Visualizing Game-Based Certificates for Hyperproperty Verification
Raven Beutner, Bernd Finkbeiner, Angelina Göbl
TL;DR
The paper addresses certifying hyperproperty satisfaction for HyperLTL properties by introducing a game-based framework where verification of a formula of the form $\forall^*\exists^*$. $\psi$ is cast as a two-player game between universal and existential quantifiers. A strategy for the $\exists$-player serves as a Skolem-like witness mapping from universally quantified traces to existential traces, enabling explainable certificates. HyGaViz is introduced as a browser-based tool that synthesizes such strategies from requested finite-state transition systems and a HyperLTL formula, and then allows interactive exploration by taking the role of the $\forall$-player; the backend uses spot to translate HyperLTL to DPAs and oink to synthesize strategies, with a Cytoscape.js frontend for visualization, marking a first step toward trustworthy certificates for alternating hyperproperties.
Abstract
Hyperproperties relate multiple executions of a system and are commonly used to specify security and information-flow policies. While many verification approaches for hyperproperties exist, providing a convincing certificate that the system satisfies a given property is still a major challenge. In this paper, we propose strategies as a suitable form of certificate for hyperproperties specified in a fragment of the temporal logic HyperLTL. Concretely, we interpret the verification of a HyperLTL property as a game between universal and existential quantification, allowing us to leverage strategies for the existential quantifiers as certificates. We present HyGaViz, a browser-based visualization tool that lets users interactively explore an (automatically synthesized) witness strategy by taking control over universally quantified executions.