Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (extended version)

TL;DR

Hyper Hoare Logic generalizes Hoare logic by lifting pre- and postconditions to hyper-assertions over sets of extended states, enabling reasoning about arbitrary hyperproperties that relate multiple program executions. It supports both over- and underapproximate reasoning, capturing hypersafety and the existence of executions, and can express properties beyond $k$-safety, including generalized non-interference in nondeterministic settings. The framework provides formal semantics, soundness, completeness, and compositionality results, with mechanized proofs in Isabelle/HOL and a mechanized artifact available. This unifies proving and disproving of complex program hyperproperties within a single logic, offering a robust foundation for verification and bug discovery across a broad class of properties.

Abstract

Hoare logics are proof systems that allow one to formally establish properties of computer programs. Traditional Hoare logics prove properties of individual program executions (such as functional correctness). Hoare logic has been generalized to prove also properties of multiple executions of a program (so-called hyperproperties, such as determinism or non-interference). These program logics prove the absence of (bad combinations of) executions. On the other hand, program logics similar to Hoare logic have been proposed to disprove program properties (e.g., Incorrectness Logic), by proving the existence of (bad combinations of) executions. All of these logics have in common that they specify program properties using assertions over a fixed number of states, for instance, a single pre- and post-state for functional properties or pairs of pre- and post-states for non-interference. In this paper, we present Hyper Hoare Logic, a generalization of Hoare logic that lifts assertions to properties of arbitrary sets of states. The resulting logic is simple yet expressive: its judgments can express arbitrary program hyperproperties, a particular class of hyperproperties over the set of terminating executions of a program (including properties of individual program executions). By allowing assertions to reason about sets of states, Hyper Hoare Logic can reason about both the absence and the existence of (combinations of) executions, and, thereby, supports both proving and disproving program (hyper-)properties within the same logic, including (hyper-)properties that no existing Hoare logic can express. We prove that Hyper Hoare Logic is sound and complete, and demonstrate that it captures important proof principles naturally. All our technical results have been proved in Isabelle/HOL.

Figures (1)

• Figure 1: (Non-exhaustive) overview of Hoare logics, classified in two dimensions: The type of properties a logic can establish, and the number of program executions these properties can relate (column "$\mathbf{\infty}$" subsumes an unbounded and an infinite number of executions). We explain the distinction between backward and forward underapproximate properties in App. \ref{['subsec:liveness']}. App. \ref{['app:unbounded']} gives examples of (hypersafety and set) properties for an unbounded number of executions. $\forall^* \exists^*$- and $\exists^* \forall^*$-hyperproperties are discussed in Sect. \ref{['sec:hyper-triples']}. A green checkmark indicates that a property is handled by our Hyper Hoare Logic for the programming language defined in Sect. \ref{['subsec:language']}, and $\varnothing$ indicates that no other Hoare logic supports it. The acronyms refer to the following. CHL: Cartesian Hoare Logic CHL16, HL: Hoare Logic HoareLogicFloydLogic, IL: Incorrectness Logic IncorrectnessLogic or Reverse Hoare Logic ReverseHL, InSec: Insecurity Logic InsecurityLogic, OL: Outcome Logic OutcomeLogic, RHL: Relational Hoare Logic Benton04, RHLE RHLE, MHRM next700RHL, BiKAT BiKat.

Theorems & Definitions (6)

• Definition 1
• Definition 2
• Definition 3
• Definition 4
• Lemma 1
• Definition 5