RHLE: Modular Deductive Verification of Relational $\forall\exists$ Properties

Relational program logics are used to prove that a desired relationship holds between the execution of multiple programs. Existing relational program logics have focused on verifying that all runs of a collection of programs do not fall outside a desired set of behaviors. Several important relational properties, including refinement and noninterference, do not fit into this category, as they require the existence of specific desirable executions. This paper presents RHLE, a logic for verifying a class of relational properties which we term $\forall\exists$ properties. $\forall\exists$ properties assert that for all executions of a collection of programs, there exist executions of another set of programs exhibiting some intended behavior. Importantly, RHLE can reason modularly about programs which make library calls, ensuring that $\forall\exists$ properties are preserved when the programs are linked with any valid implementation of the library. To achieve this, we develop a novel form of function specification that requires the existence of certain behaviors in valid implementations. We have built a tool based on RHLE which we use to verify a diverse set of relational properties drawn from the literature, including refinement and generalized noninterference.