The TAU Programming Languages and Systems Seminar - Inferring Phase Invariants from Phase Sketches

ABSTRACT:

Infinite state systems such as distributed protocols are challenging to verify using interactive theorem provers or automatic verification tools.  Of these techniques, deductive verification is highly expressive but requires the user to annotate the system with inductive invariants.  Finding inductive invariants is challenging, even for experts, who must often go through many iterations before successfully proving safety.  Thus, to further increase automation, one might hope to instead automatically infer the necessary invariants, but existing invariant inference techniques are unreliable and opaque. Inference may diverge or run for so long as to be useless; furthermore, feedback to the user tends to be all-or-nothing, either finding a full invariant to prove safety or reporting that no invariant could be found.  In such cases, the user is left to tweak the system using trial and error with little guidance until inference manages to succeed, or to try directly annotating the system with invariants until safety is proved.

This paper proposes user-guided invariant inference based on phase invariants, an automaton structure that captures the different logical phases of the protocol.

The automaton's states are labeled with assertions that hold in that phase, while edges between phases correspond to atomic transitions of the protocol.  The user conveys their intuition by specifying a phase sketch, which is a partially labeled (or completely unlabeled) automaton, from which a full labeling is inferred automatically.  The sketch with its additional structure provides guidance to the inference procedure about how to find an invariant than would otherwise be available; as a result, the user obtains more reliable and transparent results.

We demonstrate the utility of this approach by analyzing several distributed protocols from the literature using phase invariant based inference.  Our results show that the additional structure from phase sketches can accelerate the process of inferring an invariant to prove safety.  Crucially, guidance from a phase invariant is essential to achieve successful inference in some cases, where an invariant is automatically found based on a phase invariant but unguided techniques fail.  We find that phase sketches are pleasantly well matched to the intuitive reasoning routinely used by domain experts to understand why distributed protocols are correct, so that providing a phase sketch reuses this existing intuition.