Probabilistic relational verification for cryptographic implementations

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 relational 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 relational Hoare logic for a higher-order, stateful, probabilistic language. 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 its abstraction facilities for 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. Moreover, we validate the design of RF? by formalizing in Coq a core probabilistic λ-calculus and a relational refinement type system and proving the soundness of the latter against a denotational semantics of the probabilistic λ-calculus.