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.