Visualizing Game-Based Certificates for Hyperproperty Verification

TL;DR

This paper introduces HyGaViz, a visualization tool that uses game-based strategies as certificates to verify hyperproperties specified in HyperLTL, enhancing interpretability and interaction in system verification.

Contribution

It proposes a novel game-based approach to generate certificates for hyperproperties and develops an interactive visualization tool, HyGaViz, for exploring these strategies.

Findings

Successfully synthesizes witness strategies for hyperproperties.

Enables interactive exploration of verification certificates.

Improves understanding of hyperproperty verification processes.

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.