research-article

Probabilistic relational verification for cryptographic implementations

Authors:

Cédric Fournet,

Benjamin Grégoire,

Pierre-Yves Strub,

Santiago Zanella-BéguelinAuthors Info & Claims

POPL '14: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

Pages 193 - 205

https://doi.org/10.1145/2535838.2535847

Published: 08 January 2014 Publication History

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.

Supplementary Material

MP4 File (d1_right_t9.mp4)

Download
248.34 MB

References

[1]

M. Abadi and C. Fournet. Private authentication. Theor. Comput. Sci., 322(3):427--476, 2004.

Digital Library

[2]

M. Aizatulin, A. D. Gordon, and J. Jürjens. Computational verification of C protocol implementations by symbolic execution. In CCS 2012, pages 712--723. ACM, 2012.

Digital Library

[3]

J. B. Almeida, M. Barbosa, G. Barthe, and F. Dupressoir. Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations. In CCS 2013. ACM, 2013. Also appears as Cryptology ePrint Archive, Report 2013/316.

Digital Library

[4]

A. W. Appel and D. A. McAllester. An indexed model of recursive types for foundational proof-carrying code. ACM Trans. Program. Lang. Syst., 23(5):657--683, 2001.

Digital Library

[5]

M. Arapinis, T. Chothia, E. Ritter, and M. Ryan. Analysing unlinkability and anonymity using the applied Pi calculus. In CSF 2010, pages 107--121. IEEE Computer Society, 2010.

Digital Library

[6]

P. Audebaud and C. Paulin-Mohring. Proofs of randomized algorithms in Coq. Sci. Comput. Program., 74(8):568--589, 2009.

Digital Library

[7]

G. Barthe, B. Grégoire, and S. Zanella-Béguelin. Formal certification of code-based cryptographic proofs. In POPL 2009, pages 90--101. ACM, 2009.

Digital Library

[8]

G. Barthe, B. Grégoire, S. Heraud, and S. Zanella-Béguelin. Computer-aided security proofs for the working cryptographer. In CRYPTO 2011, volume 6841 of Lecture Notes in Computer Science, pages 71--90. Springer, 2011.

Digital Library

[9]

G. Barthe, B. Grégoire, Y. Lakhnech, and S. Zanella-Béguelin. Beyond provable security. Verifiable IND-CCA security of OAEP. In CT-RSA 2011, volume 6558 of Lecture Notes in Computer Science, pages 180--196. Springer, 2011.

Digital Library

[10]

G. Barthe, B. Köpf, F. Olmedo, and S. Zanella Béguelin. Probabilisticrelational reasoning for differential privacy. In POPL 2012, pages 97--110. ACM, 2012.

Digital Library

[11]

N. Benton. Simple relational correctness proofs for static analyses and program transformations. In POPL 2004, pages 14--25. ACM, 2004.

Digital Library

[12]

K. Bhargavan, C. Fournet, and A. D. Gordon. Modular verification of security protocol code by typing. In POPL 2010, pages 445--456. ACM, 2010.

Digital Library

[13]

K. Bhargavan, C. Fournet, M. Kohlweiss, A. Pironti, and P.-Y. Strub. Implementing TLS with verified cryptographic security. In S&P 2013, pages 445--459. IEEE Computer Society, 2013.

Digital Library

[14]

B. Blanchet. Security protocol verification: Symbolic and computational models. In POST 2012, volume 7215 of Lecture Notes in Computer Science, pages 3--29. Springer, 2012.

Digital Library

[15]

{15} J. Borgström, A. D. Gordon, M. Greenberg, J. Margetson, and J. V. Gael. Measure transformer semantics for bayesian machine learning. In ESOP 2011, volume 6602 of Lecture Notes in Computer Science, pages 77--96. Springer, 2011.

Digital Library

[16]

D. Cadé and B. Blanchet. From computationally-proved protocol specifications to implementations. In ARES 2012, pages 65--74. IEEE Computer Society, 2012.

Digital Library

[17]

R. Chadha, L. Cruz-Filipe, P. Mateus, and A. Sernadas. Reasoning about probabilistic sequential programs. Theor. Comput. Sci., 379(1--2):142--165, 2007.

Digital Library

[18]

S. Chaudhuri, S. Gulwani, and R. Lublinerman. Continuity and robustness of programs. Commun. ACM, 55(8):107--115, 2012.

Digital Library

[19]

T. Chothia and V. Smirnov. A traceability attack against e-passports. In FC 2010, volume 6052 of Lecture Notes in Computer Science, pages 20--34. Springer, 2010.

Digital Library

[20]

M. R. Clarkson and F. B. Schneider. Hyperproperties. J. of Comput. Sec., 18(6):1157--1210, 2010.

Digital Library

[21]

L. M. de Moura and N. Bjørner. Z3: An efficient SMT solver. In TACAS 2008, volume 4963 of Lecture Notes in Computer Science, pages 337--340. Springer, 2008.

Digital Library

[22]

F. Dupressoir, A. D. Gordon, J. Jürjens, and D. A. Naumann. Guiding a general-purpose C verifier to prove cryptographic protocols. In CSF 2011, pages 3--17. IEEE Computer Society, 2011.

Digital Library

[23]

Y. A. Feldman and D. Harel. A probabilistic dynamic logic. J. Comput. Syst. Sci., 28(2):193--215, 1984.

[24]

C. Fournet, M. Kohlweiss, and P.-Y. Strub. Modular code-based cryptographic verification. In CCS 2011, pages 341--350. ACM, 2011.

Digital Library

[25]

J. A. Goguen and J. Meseguer. Security policies and security models. In S&P 1982, pages 11--20. IEEE Computer Society, 1982.

[26]

G. Gonthier, A. Mahboubi, and E. Tassi. A small scale reflection extension for the Coq system. Technical Report RR-6455, INRIA, 2008.

[27]

J. Hurd, A. McIver, and C. Morgan. Probabilistic guarded commands mechanized in HOL. Theor. Comput. Sci., 346(1):96--112, 2005.

Digital Library

[28]

{28} B. Jonsson, W. Yi, and K. G. Larsen. Probabilistic extensions of process algebras. In Handbook of Process Algebra, pages 685--710. Elsevier, 2001.

[29]

O. Kiselyov and C.-c. Shan. Embedded probabilistic programming. In DSL 2009, volume 5658 of Lecture Notes in Computer Science, pages 360--384. Springer, 2009.

Digital Library

[30]

D. Kozen. A probabilistic PDL. J. Comput. Syst. Sci., 30(2):162--178, 1985.

[31]

R. Küsters, T. Truderung, and J. Graf. A framework for the cryptographic verification of Java-like programs. In CSF 2012, pages 198--212. IEEE Computer Society, 2012.

Digital Library

[32]

J. McCarthy. Towards a mathematical science of computation. In IFIP Congress, pages 21--28, 1962.

[33]

A. McIver and C. Morgan. Abstraction, Refinement, and Proof for Probabilistic Systems. Monographs in Computer Science. Springer, 2005.

Digital Library

[34]

A. Nanevski, G. Morrisett, A. Shinnar, P. Govereau, and L. Birkedal. Ynot: dependent types for imperative programs. In ICFP 2008, pages 229--240. ACM, 2008.

Digital Library

[35]

S. Park, F. Pfenning, and S. Thrun. A probabilistic language based upon sampling functions. In POPL 2005, pages 171--182. ACM, 2005.

Digital Library

[36]

T. P. Pedersen. Non-interactive and information-theoretic secure verifiable secret sharing. In CRYPTO '91, volume 576 of Lecture Notes in Computer Science, pages 129--140. Springer, 1991.

Digital Library

[37]

N. Ramsey and A. Pfeffer. Stochastic lambda calculus and monads of probability distributions. In POPL 2002, pages 154--165. ACM, 2002.

Digital Library

[38]

J. H. Reif. Logics for probabilistic programming (extended abstract). In STOC 1980, pages 8--13. ACM, 1980.

Digital Library

[39]

B. Reus and N. Charlton. A guide to program logics for higher-order store, 2012. Unpublished manuscript.

[40]

A. Rial and G. Danezis. Privacy-preserving smart metering. In WPES 2011, pages 49--60. ACM, 2011.

Digital Library

[41]

A. Sabelfeld and A. C. Myers. Language-based information-flow security. IEEE Journal on Selected Areas in Communications, 21(1):5--19, 2003.

Digital Library

[42]

G. Stewart, A. Banerjee, and A. Nanevski. Dependent types for enforcement of information flow and erasure policies in heterogeneous data structures. In PPDP 2013, pages 145--156. ACM, 2013.

Digital Library

[43]

P.-Y. Strub, N. Swamy, C. Fournet, and J. Chen. Self-certification: Bootstrapping certified typecheckers in F* with Coq. In POPL 2012, pages 571--584. ACM, 2012.

Digital Library

[44]

K. Svendsen, L. Birkedal, and A. Nanevski. Partiality, state and dependent types. In TLCA 2011, pages 198--212. Springer, 2011.

Digital Library

[45]

N. Swamy, J. Chen, C. Fournet, P.-Y. Strub, K. Bhargavan, and J. Yang. Secure distributed programming with value-dependent types. In ICFP 2011, pages 266--278. ACM, 2011.

Digital Library

[46]

N. Swamy, J. Weinberger, C. Schlesinger, J. Chen, and B. Livshits. Verifying higher-order programs with the Dijkstra monad. In PLDI 2013, pages 387--398. ACM, 2013.

Digital Library

Cited By

Vasilenko EVazou NBarthe G(2024)OBRA: Oracle-Based, Relational, Algorithmic Type VerificationProgramming Languages and Systems10.1007/978-981-97-8943-6_14(283-302)Online publication date: 23-Oct-2024
https://dl.acm.org/doi/10.1007/978-981-97-8943-6_14
G GKizhakkethottam J(2023)A Study on Formal Verification of Smart Contracts in Distributed Ledger Technology2023 IEEE International Conference on Recent Advances in Systems Science and Engineering (RASSE)10.1109/RASSE60029.2023.10363616(1-9)Online publication date: 8-Nov-2023
https://doi.org/10.1109/RASSE60029.2023.10363616
Baelde DKoutsos ALallemand J(2023)A Higher-Order Indistinguishability Logic for Cryptographic Reasoning2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1109/LICS56636.2023.10175781(1-13)Online publication date: 26-Jun-2023
https://doi.org/10.1109/LICS56636.2023.10175781
Show More Cited By

Index Terms

Probabilistic relational verification for cryptographic implementations

Recommendations

Probabilistic relational verification for cryptographic implementations
POPL '14

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 ...
Higher-order probabilistic adversarial computations: categorical semantics and program logics

Adversarial computations are a widely studied class of computations where resource-bounded probabilistic adversaries have access to oracles, i.e., probabilistic procedures with private state. These computations arise routinely in several domains, ...
CoqQ: Foundational Verification of Quantum Programs

CoqQ is a framework for reasoning about quantum programs in the Coq proof assistant. Its main components are: a deeply embedded quantum programming language, in which classic quantum algorithms are easily expressed, and an expressive program logic for ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '14: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 2014

702 pages

ISBN:9781450325448

DOI:10.1145/2535838

General Chair:
Suresh Jagannathan
Purdue University, USA
,
Program Chair:
Peter Sewell
University of Cambridge, UK

ACM SIGPLAN Notices Volume 49, Issue 1
POPL '14
January 2014
661 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2578855
Editor:
Mark W. Bailey
Hamilton College, Clinton, NY
Issue’s Table of Contents

Copyright © 2014 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

In-Cooperation

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 08 January 2014

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

POPL '14

Sponsor:

SIGPLAN

POPL '14: The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 22 - 24, 2014

California, San Diego, USA

Acceptance Rates

POPL '14 Paper Acceptance Rate 51 of 220 submissions, 23%;

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

65
Total Citations
View Citations
615
Total Downloads

Downloads (Last 12 months)27
Downloads (Last 6 weeks)2

Reflects downloads up to 16 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Vasilenko EVazou NBarthe G(2024)OBRA: Oracle-Based, Relational, Algorithmic Type VerificationProgramming Languages and Systems10.1007/978-981-97-8943-6_14(283-302)Online publication date: 23-Oct-2024
https://dl.acm.org/doi/10.1007/978-981-97-8943-6_14
G GKizhakkethottam J(2023)A Study on Formal Verification of Smart Contracts in Distributed Ledger Technology2023 IEEE International Conference on Recent Advances in Systems Science and Engineering (RASSE)10.1109/RASSE60029.2023.10363616(1-9)Online publication date: 8-Nov-2023
https://doi.org/10.1109/RASSE60029.2023.10363616
Baelde DKoutsos ALallemand J(2023)A Higher-Order Indistinguishability Logic for Cryptographic Reasoning2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1109/LICS56636.2023.10175781(1-13)Online publication date: 26-Jun-2023
https://doi.org/10.1109/LICS56636.2023.10175781
de Amorim P(2023)A Higher-Order Language for Markov Kernels and Linear OperatorsFoundations of Software Science and Computation Structures10.1007/978-3-031-30829-1_5(89-112)Online publication date: 21-Apr-2023
https://doi.org/10.1007/978-3-031-30829-1_5
Vasilenko EVazou NBarthe G(2022)Safe couplings: coupled refinement typesProceedings of the ACM on Programming Languages10.1145/35476436:ICFP(596-624)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547643
Ho SProtzenko JBichhawat ABhargavan K(2022)Noise: A Library of Verified High-Performance Secure Channel Protocol Implementations2022 IEEE Symposium on Security and Privacy (SP)10.1109/SP46214.2022.9833621(107-124)Online publication date: May-2022
https://doi.org/10.1109/SP46214.2022.9833621
Dupressoir FKohbrok KOechsner S(2022)Bringing State-Separating Proofs to EasyCrypt A Security Proof for Cryptobox2022 IEEE 35th Computer Security Foundations Symposium (CSF)10.1109/CSF54842.2022.9919671(227-242)Online publication date: Aug-2022
https://doi.org/10.1109/CSF54842.2022.9919671
Bhargavan KBichhawat ADo QHosseyni PKüsters RSchmitz GWürtele TKim YKim JVigna GShi E(2021)An In-Depth Symbolic Security Analysis of the ACME StandardProceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security10.1145/3460120.3484588(2601-2617)Online publication date: 12-Nov-2021
https://dl.acm.org/doi/10.1145/3460120.3484588
Bhargavan KBichhawat ADo QHosseyni PKüsters RSchmitz GWürtele T(2021)$\text{DY}^{\star}$: A Modular Symbolic Verification Framework for Executable Cryptographic Protocol Code2021 IEEE European Symposium on Security and Privacy (EuroS&P)10.1109/EuroSP51992.2021.00042(523-542)Online publication date: Sep-2021
https://doi.org/10.1109/EuroSP51992.2021.00042
QU WGABOARDI MGARG D(2021)Relational cost analysis in a functional-imperative settingJournal of Functional Programming10.1017/S095679682100007131Online publication date: 2-Nov-2021
https://doi.org/10.1017/S0956796821000071
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents