Checking Satisfiability of Hyperproperties using First-Order Logic

TL;DR

This paper introduces FOLHyper, a tool that translates HyperLTL hyperproperties into first-order logic to leverage FOL solvers for satisfiability checking, aiding security and information-flow analysis.

Contribution

FOLHyper is the first tool to reduce HyperLTL satisfiability to FOL, enabling analysis beyond the decidable fragment and improving unsatisfiability proofs.

Findings

FOLHyper effectively proves unsatisfiability of hyperproperties.

It extends analysis capabilities beyond the decidable HyperLTL fragment.

FOLHyper complements existing bounded satisfiability approaches.

Abstract

Hyperproperties are system properties that relate multiple execution traces and occur, e.g., when specifying security and information-flow properties. Checking if a hyperproperty is satisfiable has many important applications, such as testing if some security property is contradictory, or analyzing implications and equivalences between information-flow policies. In this paper, we present FOLHyper, a tool that can automatically check satisfiability of hyperproperties specified in the temporal logic HyperLTL. FOLHyper reduces the problem to an equisatisfiable first-order logic (FOL) formula, which allows us to leverage FOL solvers for the analysis of hyperproperties. As such, FOLHyper is applicable to many formulas beyond the decidable $\exists^*\forall^*$ fragment of HyperLTL. Our experiments show that FOLHyper is particularly useful for proving that a formula is unsatisfiable, and complements existing bounded approaches to satisfiability.