Proving hypersafety compositionally

Hypersafety properties of arity 𝑛 are program properties that relate 𝑛 traces of a program (or, more generally, traces of 𝑛 programs). Classic examples include determinism, idempotence, and associativity. A number of relational program logics have been introduced to target this class of properties. Their aim is to construct simpler proofs by capitalizing on structural similarities between the 𝑛 related programs. We propose unexplored, complementary proof principles that establish hyper-triples (i.e. hypersafety judgments) as a unifying compositional building block for proofs, and we use them to develop a Logic for Hyper-triple Composition (LHC), which supports forms of proof compositionality that were not achievable in previous relational logics. We prove LHC sound and apply it to a number of challenging examples.

Many properties of interest about programs are properties not of individual program traces but rather of multiple program traces. For example, stipulating a bound on mean response time over all executions of a program cannot be specified as a property of individual traces, because the acceptability of delays in a trace depends on the magnitude of delays in all other traces. Clarkson and Schneider [2008] formally studied this class of properties, coining the term hyperproperties. In this paper, we focus on the verification problem of a class of generalized hyperproperties, which we will refer to as 𝑛-safety properties: these are safety hyperproperties (i.e. only concerned with partial correctness) that govern 𝑛 executions of potentially different programs. More formally, these 𝑛-safety properties have the form ∀(𝑠 1 , 𝑠 ′ 1 ) ∈ 𝑡 1 . . . ∀(𝑠 𝑛 , 𝑠 ′ 𝑛 ) ∈ 𝑡 𝑛 . 𝜑 (𝑠 1 , 𝑠 ′ 1 , . . . , 𝑠 𝑛 , 𝑠 ′ 𝑛 ), where 𝑡 denotes the set of input/output states of the traces of 𝑡. Examples of such properties are 1 commutativity (𝑛 = 2), associativity (𝑛 = 4), determinism (𝑛 = 2), noninterference (𝑛 = 2) and transitivity (𝑛 = 3). Input-output equivalences between two programs can also be proved as 2-safety properties (e.g. a compiler optimization preserves I/O behaviour).

One approach to proving 𝑛-safety properties is to obtain from 𝑡 a precise mathematical characterization 𝑅 of its functionality 𝑡 -i.e. 𝑡's strongest postcondition-and then prove using this mathematical characterization that the desired 𝑛-safety property 𝜑 is satisfied. This approach has a major drawback, however: functional correctness is in general a much stronger-thus more difficult to prove-property of 𝑡 than what proving 𝜑 requires.

Thus, the trend in research on this problem has been instead towards reasoning directly about 𝑛-safety, through a number of so-called relational program logics, e.g. [Barthe et al. 2016;Benton 2004;Sousa and Dillig 2016;Yang 2007]. These logics move away from the traditional Hoaretriple judgment and introduce 𝑛-ary relational Hoare-style judgments, which we will refer to as hyper-triples. In our syntax, a hyper-triple (of arity 𝑛) is a judgment of the form

For example, determinism of 𝑡 can be expressed as ⊢ vars 1 = vars 2 [1: 𝑡, 2: 𝑡] vars 1 = vars 2 , which asserts that 1 Intuitively, for instance, associativity f(𝑎, f(𝑏, 𝑐)) = f(f(𝑎, 𝑏), 𝑐) compares 4 runs of f.