Probabilistic Relational Verification for Cryptographic Implementations

In the form of tools like EasyCrypt, relational program logics have been used for mechanizing formal proofs of various cryptographic constructions. With an eye towards scaling these successes towards end-to-end security proofs for implementations of distributed systems, we present rF*, a new extension of F*, a general-purpose higher-order stateful programming language with a verification system based on refinement types.

The distinguishing feature of rF* is a new probabilistic, relational Hoare logic, formalized in Coq—the first such logic for a higher-order, stateful language. We prove the soundness of this logic against a new denotational semantics for rF*, in contrast to prior operational formalizations of F*. Through careful language design, we adapt the F* typechecker to generate both classic and relational verification conditions, and to automatically discharge their proofs using an SMT solver. Thus, we are able to benefit from the existing features of F*, including, for example, its abstraction facilities that support modular reasoning about program fragments. We evaluate rF* experimentally by programming a series of cryptographic constructions and protocols, and by verifying their security properties, ranging from information flow to unlinkability, integrity, and privacy.