Finding $\forall\exists$ Hyperbugs using Symbolic Execution

TL;DR

This paper introduces an automated symbolic execution-based method to detect violations of complex $orall ightarrow ext{exists}$ hyperproperties in software, addressing challenges posed by their quantifier alternation.

Contribution

It extends symbolic execution techniques to handle trace quantification for verifying $orall ightarrow ext{exists}$ hyperproperties, providing a prototype implementation.

Findings

Successfully detects violations in challenging examples

Extends bug-finding techniques to hyperproperties

Prototype demonstrates effectiveness

Abstract

Many important hyperproperties, such as refinement and generalized non-interference, fall into the class of $\forall\exists$ hyperproperties and require, for each execution trace of a system, the existence of another trace relating to the first one in a certain way. The alternation of quantifiers renders $\forall\exists$ hyperproperties extremely difficult to verify, or even just to test. Indeed, contrary to trace properties, where it suffices to find a single counterexample trace, refuting a $\forall\exists$ hyperproperty requires not only to find a trace, but also a proof that no second trace satisfies the specified relation with the first trace. As a consequence, automated testing of $\forall\exists$ hyperproperties falls out of the scope of existing automated testing tools. In this paper, we present a fully automated approach to detect violations of $\forall\exists$ hyperproperties in software systems. Our approach extends bug-finding techniques based on symbolic execution with support for trace quantification. We provide a prototype implementation of our approach, and demonstrate its effectiveness on a set of challenging examples.