Gilles Barthe
Skip Abstract Section
Skip Supplemental Material SectionAbstract
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.
Supplemental Material
- M. Abadi and C. Fournet. Private authentication. Theor. Comput. Sci., 322(3):427--476, 2004. Google Scholar
Digital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- P. Audebaud and C. Paulin-Mohring. Proofs of randomized algorithms in Coq. Sci. Comput. Program., 74(8):568--589, 2009. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- N. Benton. Simple relational correctness proofs for static analyses and program transformations. In POPL 2004, pages 14--25. ACM, 2004. Google ScholarDigital Library
- K. Bhargavan, C. Fournet, and A. D. Gordon. Modular verification of security protocol code by typing. In POPL 2010, pages 445--456. ACM, 2010. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- {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. Google ScholarDigital Library
- D. Cadé and B. Blanchet. From computationally-proved protocol specifications to implementations. In ARES 2012, pages 65--74. IEEE Computer Society, 2012. Google ScholarDigital Library
- R. Chadha, L. Cruz-Filipe, P. Mateus, and A. Sernadas. Reasoning about probabilistic sequential programs. Theor. Comput. Sci., 379(1--2):142--165, 2007. Google ScholarDigital Library
- S. Chaudhuri, S. Gulwani, and R. Lublinerman. Continuity and robustness of programs. Commun. ACM, 55(8):107--115, 2012. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- M. R. Clarkson and F. B. Schneider. Hyperproperties. J. of Comput. Sec., 18(6):1157--1210, 2010. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Y. A. Feldman and D. Harel. A probabilistic dynamic logic. J. Comput. Syst. Sci., 28(2):193--215, 1984.Google ScholarCross Ref
- C. Fournet, M. Kohlweiss, and P.-Y. Strub. Modular code-based cryptographic verification. In CCS 2011, pages 341--350. ACM, 2011. Google ScholarDigital Library
- J. A. Goguen and J. Meseguer. Security policies and security models. In S&P 1982, pages 11--20. IEEE Computer Society, 1982.Google Scholar
- G. Gonthier, A. Mahboubi, and E. Tassi. A small scale reflection extension for the Coq system. Technical Report RR-6455, INRIA, 2008.Google Scholar
- J. Hurd, A. McIver, and C. Morgan. Probabilistic guarded commands mechanized in HOL. Theor. Comput. Sci., 346(1):96--112, 2005. Google ScholarDigital Library
- {28} B. Jonsson, W. Yi, and K. G. Larsen. Probabilistic extensions of process algebras. In Handbook of Process Algebra, pages 685--710. Elsevier, 2001.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- D. Kozen. A probabilistic PDL. J. Comput. Syst. Sci., 30(2):162--178, 1985.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- J. McCarthy. Towards a mathematical science of computation. In IFIP Congress, pages 21--28, 1962.Google Scholar
- A. McIver and C. Morgan. Abstraction, Refinement, and Proof for Probabilistic Systems. Monographs in Computer Science. Springer, 2005. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- S. Park, F. Pfenning, and S. Thrun. A probabilistic language based upon sampling functions. In POPL 2005, pages 171--182. ACM, 2005. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- N. Ramsey and A. Pfeffer. Stochastic lambda calculus and monads of probability distributions. In POPL 2002, pages 154--165. ACM, 2002. Google ScholarDigital Library
- J. H. Reif. Logics for probabilistic programming (extended abstract). In STOC 1980, pages 8--13. ACM, 1980. Google ScholarDigital Library
- B. Reus and N. Charlton. A guide to program logics for higher-order store, 2012. Unpublished manuscript.Google Scholar
- A. Rial and G. Danezis. Privacy-preserving smart metering. In WPES 2011, pages 49--60. ACM, 2011. Google ScholarDigital Library
- A. Sabelfeld and A. C. Myers. Language-based information-flow security. IEEE Journal on Selected Areas in Communications, 21(1):5--19, 2003. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- K. Svendsen, L. Birkedal, and A. Nanevski. Partiality, state and dependent types. In TLCA 2011, pages 198--212. Springer, 2011. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
Index Terms
- Probabilistic relational verification for cryptographic implementations
Recommendations
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, ...
Formal verification of higher-order probabilistic programs: reasoning about approximation, convergence, Bayesian inference, and optimization
Probabilistic programming provides a convenient lingua franca for writing succinct and rigorous descriptions of probabilistic models and inference tasks. Several probabilistic programming languages, including Anglican, Church or Hakaru, derive their ...
Probabilistic relational verification for cryptographic implementations
POPL '14: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming LanguagesRelational 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 ...
Comments