RHLE: Automatic Verification of $\forall\exists$-Hyperproperties

Specifications of program behavior typically consider single executions of a program, usually requiring that every execution never reaches a bad state (a safety property) or that every execution can eventually produce some good state (a liveness property). Many desirable behaviors, however, including refinement and non-interference, range over multiple executions of a program. These sorts of behaviors are instead expressible as a combination of k-safety and k-liveness hyperproperties. Relational program logics allow for reasoning about the validity of hyperproperties, but, just as Floyd-Hoare logics focus on axiomatic reasoning about safety, existing relational logics have focused on proving k-safety properties. Such relational logics are unfortunately not suitable for verifying more general combinations of k-safety and k-liveness hyperproperties. This paper presents RHLE, a relational program logic for reasoning about a class of such hyperproperties that we term $\forall\exists$-hyperproperties. RHLE forms the basis for an algorithm capable of automatically verifying this class of hyperproperties. We present an implementation of this algorithm which we have used to automatically verify a number of $\forall\exists$-hyperproperties, including refinement and non-interference properties, on a corpus of representative programs.