Probabilistic Relational Verification for Cryptographic Implementations
- Gilles Barthe ,
- Cédric Fournet ,
- Benjamin Grégoire ,
- Pierre-Yves Strub ,
- Santiago Zanella-Béguelin ,
- Nikhil Swamy
41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014 |
Published by ACM
To appear
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 lambda-calculus and a relational refinement type system and proving the soundness of the latter against a denotational semantics of the probabilistic lambda-calculus.