by Barthe, Gilles, Fournet, Cédric, Grégoire, Benjamin, Strub, Pierre-Yves, Swamy, Nikhil and Zanella-Béguelin, Santiago
Abstract:
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 F* 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 lambda λ calculus.
Reference:
Probabilistic Relational Verification for Cryptographic Implementations (Barthe, Gilles, Fournet, Cédric, Grégoire, Benjamin, Strub, Pierre-Yves, Swamy, Nikhil and Zanella-Béguelin, Santiago), In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Association for Computing Machinery, 2014.
Bibtex Entry:
@inproceedings{10.1145/2535838.2535847,
author = {Barthe, Gilles and Fournet, C\'{e}dric and Gr\'{e}goire, Benjamin and Strub, Pierre-Yves and Swamy, Nikhil and Zanella-B\'{e}guelin, Santiago},
title = {Probabilistic Relational Verification for Cryptographic Implementations},
year = {2014},
isbn = {9781450325448},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/2535838.2535847},
doi = {10.1145/2535838.2535847},
abstract = {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 F* 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 lambda λ calculus.},
booktitle = {Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
pages = {193–205},
numpages = {13},
keywords = {program logics, probabilistic programming},
location = {San Diego, California, USA},
series = {POPL '14}
}