Notes on relational program verification

Relational-program-verification.md

Relational Verification

Beckert, B. and M. Ulbrich. (2018) "Trends in Relational Program Verification." In I. Schaefer and P. Muller (Eds.), Principled Software Development: Essays Dedicated to Arnd Poetzsch-Heffter on the Occasion of His 60th Birthday. Springer, pp. 41-58.

Relational verification verifies relational properties that relate different programs.

To verify relational properties, one must (in principle) compare several runs of the same program.

Some examples of relational properties:

• Two programs are equivalent if they terminate in equivalent states when started from equivalent inputs.

• If any two runs of a program that start with different values of an input x result in an equivalent output state, then x does not interfere with the output (i.e., the program does not reveal any information about the input value of x).

Relational program verification is somewhat easier, because you can rely on the original program as a specification: you can say the original behavior is the expected behavior except for certain intended changes. (Note that this directly exhibits one standard use of relational verification: to verify that there are no regressions.)

The complexity of traditional functional verification grows with the size of the program. The complexity of relational verification grows with the size of the difference between the programs compared. So, if the programs are similar, the difference can be small, and thus what you end up verifying can be less complex.

Section: Basic Notions and Definitions

We are working with a set Progs of programs, and a given state space S which has a special state err to indicate that a program has failed an assertion. The value of a variable x at a state s in S is denoted as s(x).

For any given program P in Progs, the semantics of that program is a relation run.P, which is a subset of S x S. I will denote a particular pair (s, s') from run.P like this: run.P(s, s'). Intuitively, this represents that the program P, when started in state s, may terminate in state s'.

If the programming language is deterministic, then run.P is a partial function (any starting state s in S can be mapped to only one output state s' in S). If the language is nondeterministic, then it's a regular relation (any starting state s can be mapped to more than one output state s').

A functional safety property F is basically the set of all program runs that count as "correct behavior" for the program, i.e. all pairs (s, s') where it is correct for the program to end in s' if it starts in s. So formally, F is just a subset of S x S.

We say that a program P satisfies F iff, for all s and s', run.P(s, s') implies that (s, s') is in F. That is to say, all program runs of P is a subset of F.

Example. Here's a property: a program increments x by 1 if x starts with a positive value. We don't need to say anything about what happens when the program doesn't start with a positive value of x. We can formalize the property like this:

{(s, s') | if s(x) > 0 then s'(x) = s(x) + 1}

In other words, it is the set of all program runs that start with s(x) as a positive number, and end with s'(x) being one more.

Note that, in order to evaluate if a program satisfies a functional safety property F, we have to check each program run separately, to figure out if it belongs in F. So for the above property, we'd have to check that this holds good for every (s, s') run. If so, then we could say that the program satisfies this F.

By contrast, a relational property puts program runs into relation. In order to check whether two programs P1 and P2 satsify a relational property, we have to look at each P1 program run in the context of all P2 program runs, and vice versa.

A relational safety property R is basically the set of all combinations of the two programs' runs that are allowed to "co-exist." So formally, R is a subset of (S x S) x (S x S). That is to say, it's a relation on state pairs (i.e., a relation on program runs).

We say that two programs P1 and P2 in Progs satisfy R iff for all states s1, s1', s2, s2': run.P(s1, s1') and run.P(s2, s2') implies that ((s1, s1'), (s2, s2')) is in R.

Example. A common relational property is program equivalence. We can define this by saying that two programs are equivalent if, when started in equivalent states, they end in equivalent states. We don't need to make a restriction on what happens when the programs don't start in equivalent states.

{ ((s1, s1'), (s2, s2')) | if s1 = s2 then s1' = s2' }

In other words, it is the set of all pairs of program runs that, when started from equivalent s1 and s2, end in equivalent s1' and s2'.

To check this for programs P1 and P2, we'd need to check every ((s1, s1'), (s2, s2')) combination. In other words, we'd need to check every pair of parallel program runs that start with equivalent states, and see if they end up in equivalent states. If so, then we can conclude that P1 and P2 satisfy the above property.

Example. Noninterference. This can be expressed by saying that any input variable h does not interfere with an output variable l:

{ ((s1, s1'), (s2, s2')) | if s1(l) = s2(l) then s1'(l) = s2'(l) }

To check this for programs P1 and P2, we again need to check every ((s1, s1'), (s2, s2')) combination. In other words, we need to check that for every pair of parallel program runs that start with an equilavent l, they end up with an equivalent l. Keep in mind that the program runs are of the same program. So, if this holds for every possible pair of parallel program runs, then we know that whenever the programs start with the same l, nothing can affect the output of l. No other way of running the program that starts with the same l can end up with a different l.

Note that relational properties allow 2 dimensions of variation:

• You can compare how the same program behaves with different initial states.
• You can compare how different programs behave with the same initial state.
• You can combine those two as well.

Properties designed for the case where P1 and P2 are the same program are called "single-program relational properties," or "2-properties." These are a special case of relational program verification.

Relational properties are stronger and more expressive than functional properties, and every functional property can be expressed as a relational property but not vice versa. In particular, take any relational property F, and then let R be F x F. Then that property R will be satisfied by a program P (where P1 and P2 are the same program P) iff F is satisfied by P.

For instance, take the property of incrementing x above:

{(s, s') | if s(x) > 0 then s'(x) = s(x) + 1}

To convert this to F x F we get this:

{((s1, s1'), (s2, s2')) | if s1(x) > 0 and s2(x) > 0 then s1'(x) = s1(x) + 1 and s2'(x) = s2(x) + 1 }

If P1 = P2, i.e., if P1 = P2 = P, then this property will be satisfied precisely whenever P satisfies F (it won't be possible for P to satisfy the s1/s1' clause but not the s2/s2' clause, since P is one and the same program).

Note that the definition above of a relational property is restricted to binary relations, i.e., relations between two programs P1 and P2. There are other interesting properties that can only be verified by checking three or more program runs. The above definition of relational safety properties would need to be generalized to handle those kinds of properties.

Example. Suppose we want to check that a program picks a particular option consistently. For instance, say we have a set X that is broken up into two overlapping subsets X1 and X2. Suppose next that there is some element x in the intersection of X1 and X2, and that the program P picks x from X1, and it also picks x from X2. So it's choice is consistent across X1 and X2. But what about when it's presented with X? We need to check that P picks x in that case too. So, we actually need to compare 3 runs of the program to check that it picks consistently.

Properties such as consistency that can only be defined by comparison of three transitions are called 3-properties. In fact, we can extend the notion to any k (a natural number), to get k-properties.

But, k-properties still don't cover all interesting properties. There are certain existential properties that are liveness properties that can't be expressed as k-properties (k-safety properties).

Example. If we want to express that a program terminates from all initial states, we can't do that as a k-property. If we want to express that whenever P1 terminates when started in initial state s, P2 also terminates when started in s, we need to say this:

for all s, s1' in S with run.P1(s, s1'), there is an s2' in S with run.P2(s, s2')

[TO DO: check the original paper on defining liveness to see how this definition fits]

This property is called mutual or relational termination, and it has to be a k-liveness property, rather than a k-safety property.

Clarkson et al (2008) introduce a taxonomy of relational properties that include both k-safety and k-liveness properties. They of course also take traces as the basic semantics for a program run rather than start/end pairs as we are here.

For relational verification, we need one more concept: coupling properties. A coupling property is (or rather defines?) a relation on states, which holds for corresponding states during the execution of two or more related programs.

The notion is basically that state a, b, c from P1 get coupled with state p, q, r in P2, and so we can say which states in the two programs correspond to each other during execution (e.g., a in P1 corresponds to p in P2).

If two programs run in lockstep (i.e., have identical traces), then you can just use the identity relation to couple the states.

If a coupling property holds throughout program execution, then we say that the property is coupling invariant. Typically, such invariants only need to hold at certain synchronization points, rather than at every state.

A coupling predicate is a formula that expresses the coupling property. Some coupling properties are inductive, so that we can prove by induction on the length of the traces that the property holds throughout the execution. These are a powerful tool for verifying relational properties.

Section: Application Scenarios

There are a variety of different applications that relational verification techniques are used.

(1) Single-program properties.

This kind of property relates different runs of the same program to different outputs. Typically, these properties are "symmetric" (see below).

Case: non-interference and information-flow properties.

Secure information flow requires that the public output of a program does not depend on secret inputs. So, one should not be able to see a difference in the public output, if one uses different public inputs. An attacker should not be able to learn secret input by observing the public input, purely based on the public input they enter. If this holds, then we say the program is non-interferent.

How do we express non-interference? We have to relate different runs of the program to each other, and say that, for any two runs starting in states that differ only in their secret parts, the public outputs should be the same.

Joshi and Leino (2000) and Amtoft and Banerjee (2004) were the first to give semantic definitions of information flow based on relational properties like this. There have been, of course, various other ways to talk about information flow (e.g., language-based analyses, type systems, and so on), but here the focus is on descriptions of non-interference using relational properties.

Case: symmetry properties.

This is a general idea. A symmetry property is one where, if two initial states are symmetric (i.e., similar in some specified way), then they lead to appropriately symmetric final states.

Symmetry properties are often used to make it easier to prove functional properties. Suppose I want to prove that a program P satisfies a functional property F that is compatible with a symmetry property S. I can do so like this:

1. Show that P has the symmetry property S.
2. Show that P satisfies F for a small subset X of states.
3. Show that X reaches all states via S.

The trick here is using S to show that a small subset of states X lead to all other states. If we can show this, then we only need to prove that P satisfies F for that small subset of states X. We don't have to prove it for all states.

Example. Permutation-invariance. Suppose that the states of a program are arrays (vectors) of some particular length n. We say that a program P is permutation-invariant if it produces the same output for input x and a permutation p(x).

I don't quite understand the concrete property described by the authors here. They seem to assume that there is a symmetry relation, call it Sym.n, and then they say the property is expressed like this:

{((s1, s1'), (s2, s2')) | if s1 = p(s2) for some p in Sym.n, then s1' = s2' }

I presume that Sym.n is the set of permutation-invariant program runs. I don't understand why we say "for some p in Sym.n" though. It seems like we should say "for all ps in Sym.n" in order to show that every permutation doesn't change the output.

In any case, let's pretend that I understand this, and that I'm right that Sym.n is the set of permutation-invariant program runs.

If that's right, then this can help prove further functional properties. Suppose we want to prove that a program P satisfies a functional property F. Well, we only need to prove that P satisfies this for the sorted input arrays. The sorted input arrays are like a canonical set of inputs. If we've proved that P satisfies S, and then we prove that P satisfies F for sorted array inputs, we may conclude that P satisfies F for all array inputs, because S tells us that program runs are permutation-invariant, so we'll get the same results when we run the program with permutations of the sorted inputs.

(2) Multi-program properties.

These properties compare the observable behavior of two or more programs. Often, the properties express some sort of (strong or weak) equivalence.

Interestingly, Beckert et al (2015) have shown that the verification of a multi-program proprety can be reduced to the verification of a single-program property. The claim here is that there is a way to combine the various programs under test into a single program that has all of the behaviors of the different programs. Then, we can just verify that one, combined program. This may be inefficient, but it is possible, and it shows that whether we compare multiple programs against each other or whether we compare one program that can do all those things against itself, it doesn't matter. It comes to the same thing.

Case: regression verification.

Regression testing is a common way to try and detect unintended regressions when programs are updated. Godlin and Strichman (2013) coined the term "regression verification" to describe a similar technique, but using relational verification. The idea is that you check the original program and the updated program for equivalence.

The most basic form of this equivalence property says: the two programs terminate in the same final states when started from the same initial states.

However, for more sophisticated scenarios, we might want to check that the two programs are equivalent only for those initial states that are not affected by the update. We call this conditional equivalence.

Alternatively (or in addition to), we might want to check that the final states of the two programs differ in a formally specified way. Here, we can express exactly how the update is meant to alter the program's behavior. We call this relational equivalence.

The authors note that one can use regression verification to prove information-flow properties: you can check that the updated program does not leak more secrets than the original. This is a two-program 4-property.

Case: translation validation.

This is the usual TV (translation validation) thing. We want to prove that a program translation is "correct," and so we prove that the original and the translated programs are equivalent in some way (e.g., the translation did not introduce new behaviors). This is used to validate compiler transformations, for instance.

Case: contextual equivalence.

This kind of property is called "contextual equivalence" by Murawski et al (2015) and "backward compatibility" by Welsch and Poetzsch-Heffter (2014). This is a relational property of sub-programs. It says that two sub-programs P1 and P2 behave equivalently when included in any possible larger program context.

This is useful if, say, you want to refactor a library that is used by lots of other programs. It sure would be nice to know that your refactor leaves the library operating the same, so that you don't break the code of all those other people that use your library (are you listening AWS? You should do this...)

Case: refinement.

Another relational property is refinement, which holds when one program refines another.

The authors claim that refinement is not a relational safety property, since it cannot be expressed using only universal quantification.

The authors point out that for non-deterministic programs, we can just use simple equivalence (i.e., F is a list of equivalent program runs): given all s1, s1', s2, s2' states, if the more concrete program runs from s1 to s1' and the more abstract program runs from s2 to s2', then the pair of those two program runs is listed in F.

But, for non-deterministic programs, this won't do, because the abstract program usually allows multiple possible states. So, the property must be stated like this: given a program run of the more concrete program from s1 to s1', there exists a program run of the more abstract program from s2 to s2', where that pair of program runs is listed in F.

The key point here appears to be that you have to use an existential quantifier to express this property. Hence, it fails to qualify as a relational safety property, because the latter must be expressed only with universal quantifiers.

Section: Verification of Relational Properties

To verify relational properties, researchers have taken traditional working verification techniques, and lifted them (employed them or enhanced them?) to address relational questions. In this regard, the authors note that one can observe two trends (that can both be at work in relational verification):

(1) Reduce relational properties to functional safety properties that can be verified with off-the-shelf verification tools.

(2) Explot similarities between intermediate states in compared program runs. This is done out of a practical need, because it is just too painful to compare each and every program run. Instead, identify some points where the programs are "synchronized," and then you only have to look at the sub-parts that are relevant after that.

Case: Reduction to functional verification.

Some created specialized logics to deal with relational properties. Benton (2004) introduced a theory of relational Hoare calculus, and Yang (2007) introduced a relational separation logic that lets you reason about two heaps instead of one.

Barthe et al (2011) introduced the notion of a "product program" that can help reduce relational verification to functional verification. To construct a product program, first make sure the two programs cannot interfere with each other (so rename variables for instance). Then, join them together into a product program P that operates on both program's variables simultaneousy. So, syntactically, the product program makes calls that operates on both sets of variables, and semantically, the product program operates on a product state space S x S which has this property:

if run.P1(s1, s1') and run.P2(s2, s2')
then run.P((s1, s2), (s1', s2')) or run.P((s1, s2), err)

In other words, the pairing of the two program state spaces must preserve their individual program runs. If P1 runs to s1' when started from s1 and P2 runs to s2' when started from s2, then the product program P better run to (s1', s2') when started from (s1, s2), or else fail an assertion. In other words, the product program should end up in the same states that P1 and P2 would end up in if they were run separately (or fail an assertion).

Why do we allow the product program to fail an assertion? The authors say it is so that we can combine programs more "liberally," in the sense that we can add assumptions about intermediate states or synchronization with assertions in the code of P. (I don't understand the sense of the authors' word "liberally" here...perhaps it simply means that it allows us to add further assertions and assumptions into the program and so prove more refined things about the programs).

Once we have a product program, we can then just use regular old functional verification to prove what we want. The reason is because this holds:

|= {A}P{B}  implies  |= {A}P1 ~ P2{B}

In other words, if we just prove {A}P{B} about our product program P, that implies that the pre and post conditions hold for P1 and P2 as they stand in the relevant relation. So, this makes it easy to use our regular functional tools to derive relational results.

The main question though is how to construct the product program.

One easy way to do it is just rename variables and append the second to the first: P1; P2. This makes a valid product program (i.e., one that satisfies the above implication). The authors note that if we do this, then in fact the word "implies" above turns into an "iff."

Barthe et al (2004) and Darvas et al (2005) basically do this. They use "self-composition" to prove non-interference: take a program P and compose it with itself, then you have a product program of which you can prove a 2-property like non-interference.

However, Terauchi and Aiken (2005) show that there are problems with this kind of simple self-composition.

The authors illustrate with the case of a simple program that has a while-loop that operates on a single variable. It turns out that in order to use simple sequential composition, one must find the strongest possible loop invariant to make it work. And loop invariants are really hard to find, so one should wonder about the practicality of the sequential self-composition technique in the presence of loops.

One way around the problem just discussed is to exploit similarities between program runs.

For instance, think about using a different execution policy. Rather than execute the programs one after the other (in sequence), execute them alternatingly: first execute one iteration of the loop in P1, then one in P2, and so on. Then, after each iteration, x1 = x2 holds. This is a strong enough coupling invariant to complete the proof inductively.

What we try to do when we exploit similarities between program runs is identify locations in both programs that are coupling points, i.e., they are points where the two programs correspond when they both reach them. Pairs of such locations are called synchronization points.

With sequential composition, you have to construct full-program predicates M and N for P1 and P2 respectively, and then you prove that the conjunction of the precondition, M, and N implies the postcondition. So, you prove the whole dang program runs at once.

With synchronization points, you do the same kind of thing, but only up to the next synchronization point. Then, you prove all the synchronization chunks, and put them together inductively to prove a property about the whole program.

The trick here is to find the "precondition" for each synchronization chunk. This "precondition" is just the coupling predicate for that synchronization point.

(There are nice diagrams/figures on pp. 12-13 that illustrate this stuff visually.)

What are good identification points? One piece of advice is: use the same places that you would in functional verification. For instance, at the heads of loops (the entry point of the loop).

There's an example in Fig. 2 on p. 13 of the paper that illustrates different ways to synchronize loops. Fig. 2a: you can just do it sequentially (no synchronization), that is, just do one after the other completes. Fig. 2b: you can do them in lock step, but this requires that both loops have the same number of iterations and it requires that both are proven to satisfy the loop pre/postconditions after each step. Fig. 2c: do the two in lock step, but allow one or the other not to happen in each step, if it fails its loop pre/postcondition, which lets the loops go a different number of times.

The authors mentions work by Elenbogen et al (2015) and Hawblitzel et al (2013) that formulates relational properties that also entail mutual termination.

Using synchronization points requires that the two programs sort of move forward from synchronization point to synchronization point in lock step. Many program pairs simply don't work this way, so one can devise even more elaborate synchronization schemes to help.

Note, of course, that the non-synchonized proof technique that uses predicates that extend over the whole length of the program, well this one can prove properties of programs that don't move through synchronization points in lock step. But of course those are difficult, so as a compromise, it is sometimes better to come up with more elaborate synchronization schemes.

For instance, maybe one program's loop needs to be unwound a certain number of times before it "synchronizes" with the other program's loop. Hence, we really need a richer relation between the two program's synchronization points. It can't be a 1:1 relationship, but rather a many-to-many relationship.

To actually weave together a product program like this, you need some transformation rules that tells your product-program-builder how to take pieces from each program and put them together. But, this can be done. See Eilers et al (2018) and Banerjee et al (2016).

The authors do claim that there seems to be high potential here for automation. For things like regression verification, it seems like often it would be enough to just specify relationally how, say, the action on the variable x has changed, and then assume that the rest has stayed the same. Felsing et al (2014) have shown ways to automatically infer relational coupling predicates for relational verification of non-trivial programs.

Important References noted by the paper

• Benton, N. (2004) "Simple relational correctness proofs for static analyses and program transformations." In: Jones ND, Leroy X (eds) Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Lan- guages, POPL 2004, Venice, Italy, January 14-16, 2004, ACM, pp 14–25. Benton presents a relational Hoare calculus for deductively proving relational properties of programs.

• Joshi, R. and K. Leino. (2000) "A semantic approach to secure information flow." Sci Comput Program 37(1-3):113–138; Amtoft, T. and A. Banerjee. (2004) "Information flow analysis in logical form." In: Gi- acobazzi R (ed) Static Analysis, 11th International Symposium, SAS 2004, Verona, Italy, August 26-28, 2004, Proceedings, Springer, Lecture Notes in Com- puter Science, vol 3148, pp 100–115. These two papers were among the first to define non-interference with relational properties rather than, say, type systems.

• Godlin, B. and O. Strichman. (2013) "Regression verification: proving the equivalence of similar programs." Softw Test, Verif Reliab 23(3):241–258. This paper introduced the term "regression verification."

• Murawski AS, Ramsay SJ, Tzevelekos N (2015) Game semantic analysis of equiv- alence in IMJ. In: Finkbeiner B, Pu G, Zhang L (eds) Automated Technology for Verification and Analysis - 13th International Symposium, ATVA 2015, Shang- hai, China, October 12-15, 2015, Proceedings, Springer, Lecture Notes in Com- puter Science, vol 9364, pp 411–428; Welsch, Y. and A. Poetzsch-Heffter. (2014) "A fully abstract trace-based semantics for reasoning about backward compatibility of class libraries." Sci Comput Program 92:129–161. These two papers were among the first to describe a similar idea. The first calls it "contextual equivalence," and the second calls it "backward compatility." They are roughly the same thing though.

• Yang, H. (2007) "Relational separation logic." Theor Comput Sci 375(1-3):308–334. Yang presents a separation logic that lets you reason about relational properties over two heaps.

• Barthe, G., J. Crespo, and C. Kunz. (2011) "Relational verification using product programs." In: Butler MJ, Schulte W (eds) FM 2011: Formal Methods - 17th Inter- national Symposium on Formal Methods, Limerick, Ireland, June 20-24, 2011. Proceedings, Springer, Lecture Notes in Computer Science, vol 6664, pp 200– 214. This is the paper that introduced product programs.

• Barthe, G., P. D'Argenio, and T. Rezk. (2004) "Secure information flow by self-composition." In: 17th IEEE Computer Security Foundations Workshop, (CSFW-17 2004), 28-30 June 2004, Pacific Grove, CA, USA, IEEE Computer Society, pp 100–114; Darvas, A. R. Hahnle, and D. Sands. (2005) "A theorem proving approach to analysis of secure information flow." In: Hutter D, Ullmann M (eds) Security in Pervasive Com- puting, Second International Conference, SPC 2005, Boppard, Germany, April 6-8, 2005, Proceedings, Springer, Lecture Notes in Computer Science, vol 3450, pp 193–209. These two papers were among the first to describe the technique of self-composition.

• Terauchi, T. and A. Aiken. (2005) "Secure information flow as a safety problem." In: Hankin C, Siveroni I (eds) Static Analysis, 12th International Symposium, SAS 2005, London, UK, September 7-9, 2005, Proceedings, Springer, Lecture Notes in Computer Science, vol 3672, pp 352–367. This paper describes some of the problems that arise for simple sequential self-composition.

• Elenbogen, D., S. Katz, and O. Strichman. (2015) "Proving mutual termination." Formal Methods in System Design 47(2):204–229; This paper formulates some relational properties that entail mutual termination (e.g., by doing loops in lock step).

• Hawblitzel, C., M. Kawaguchi, S. Lahiri, and H. Rebelo. (2013) "Towards modularly comparing programs using automated theorem provers." In: Bonacina MP (ed) Au- tomated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings, Springer, Lecture Notes in Computer Science, vol 7898, pp 282–299; Eilers, M., P. Muller, and S. Hitz. (2018) "Modular product programs." In: Ahmed A (ed) Programming Languages and Systems - 27th European Symposium on Program- ming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Springer, Lecture Notes in Computer Science, vol 10801, pp 502–529; Banerjee, A., D. Naumann, and M. Nikouei. (2016) "Relational logic with framing and hypotheses." In: Lal A, Akshay S, Saurabh S, Sen S (eds) 36th IARCS An- nual Conference on Foundations of Software Technology and Theoretical Com- puter Science, FSTTCS 2016, December 13-15, 2016, Chennai, India, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, LIPIcs, vol 65, pp 11:1–11:16. These papers describe ways to build product programs with more sophisticated weaving techniques.

• Felsing, D., S. Grebing, V. Klebanov, P. Rummer, and M. Ulbrich (2014). "Automating regression verification." In: Crnkovic I, Chechik M, Gru ̈nbacher P (eds) ACM/IEEE International Conference on Automated Software Engineering, ASE ’14, Vasteras, Sweden - September 15 - 19, 2014, ACM, pp 349–360. The authors describe how to automatically infer relational coupling predicates.