Probabilistic relational verification for cryptographic implementations. (English) Zbl 1284.68380
Proceedings of the 41st ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’14, San Diego, CA, USA, January 22–24, 2014. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-2544-8). 193-205 (2014).
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 03B70 | Logic in computer science |
| 68N18 | Functional programming and lambda calculus |
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 94A60 | Cryptography |
References:
| [1] | M. Abadi and C. Fournet. Private authentication. Theor. Comput. Sci., 322(3):427-476, 2004. 10.1016/j.tcs.2003.12.023 · Zbl 1071.68006 |
| [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. 10.1145/2382196.2382271 |
| [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. 10.1145/2508859.2516652 |
| [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. 10.1145/504709.504712 |
| [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. 10.1109/CSF.2010.15 |
| [6] | P. Audebaud and C. Paulin-Mohring. Proofs of randomized algorithms in Coq. Sci. Comput. Program., 74(8):568-589, 2009. 10.1016/j.scico.2007.09.002 · Zbl 1178.68667 |
| [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. 10.1145/1480881.1480894 · Zbl 1315.68081 |
| [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. · Zbl 1287.94048 |
| [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. · Zbl 1284.94052 |
| [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. 10.1145/2103656.2103670 · Zbl 1321.68182 |
| [11] | N. Benton. Simple relational correctness proofs for static analyses and program transformations. In POPL 2004, pages 14-25. ACM, 2004. 10.1145/964001.964003 · Zbl 1325.68057 |
| [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. 10.1145/1706299.1706350 · Zbl 1312.68052 |
| [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. 10.1109/SP.2013.37 |
| [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. 10.1007/978-3-642-28641-4_2 · Zbl 1297.68072 |
| [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. · Zbl 1326.68217 |
| [16] | D. Cadé and B. Blanchet. From computationally-proved protocol specifications to implementations. In ARES 2012, pages 65-74. IEEE Computer Society, 2012. 10.1109/ARES.2012.63 |
| [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. 10.1016/j.tcs.2007.02.040 · Zbl 1121.68028 |
| [18] | S. Chaudhuri, S. Gulwani, and R. Lublinerman. Continuity and robustness of programs. Commun. ACM, 55(8):107-115, 2012. 10.1145/2240236.2240262 |
| [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. 10.1007/978-3-642-14577-3_5 |
| [20] | M. R. Clarkson and F. B. Schneider. Hyperproperties. J. of Comput. Sec., 18(6):1157-1210, 2010. |
| [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. |
| [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. 10.1109/CSF.2011.8 |
| [23] | Y. A. Feldman and D. Harel. A probabilistic dynamic logic. J. Comput. Syst. Sci., 28(2):193-215, 1984. · Zbl 0537.68036 |
| [24] | C. Fournet, M. Kohlweiss, and P.-Y. Strub. Modular code-based cryptographic verification. In CCS 2011, pages 341-350. ACM, 2011. 10.1145/2046707.2046746 |
| [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. 10.1016/j.tcs.2005.08.005 · Zbl 1080.68063 |
| [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. · Zbl 1062.68081 |
| [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. 10.1007/978-3-642-03034-5_17 |
| [30] | D. Kozen. A probabilistic PDL. J. Comput. Syst. Sci., 30(2):162-178, 1985. · Zbl 0575.03013 |
| [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. 10.1109/CSF.2012.9 |
| [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. · Zbl 1069.68039 |
| [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. 10.1145/1411204.1411237 · Zbl 1323.68142 |
| [35] | S. Park, F. Pfenning, and S. Thrun. A probabilistic language based upon sampling functions. In POPL 2005, pages 171-182. ACM, 2005. 10.1145/1040305.1040320 · Zbl 1369.68083 |
| [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. · Zbl 0763.94015 |
| [37] | N. Ramsey and A. Pfeffer. Stochastic lambda calculus and monads of probability distributions. In POPL 2002, pages 154-165. ACM, 2002. 10.1145/503272.503288 · Zbl 1323.68150 |
| [38] | J. H. Reif. Logics for probabilistic programming (extended abstract). In STOC 1980, pages 8-13. ACM, 1980. 10.1145/800141.804647 |
| [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. 10.1145/2046556.2046564 |
| [41] | A. Sabelfeld and A. C. Myers. Language-based information-flow security. IEEE Journal on Selected Areas in Communications, 21(1):5-19, 2003. 10.1109/JSAC.2002.806121 |
| [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. 10.1145/2505879.2505895 |
| [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. 10.1145/2103656.2103723 · Zbl 1321.68205 |
| [44] | K. Svendsen, L. Birkedal, and A. Nanevski. Partiality, state and dependent types. In TLCA 2011, pages 198-212. Springer, 2011. · Zbl 1331.03020 |
| [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. 10.1145/2034773.2034811 · Zbl 1323.68229 |
| [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. 10.1145/2491956.2491978 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
