Document Open Access Logo

Practical Formal Methods for Real World Cryptography (Invited Talk)

Authors Karthikeyan Bhargavan, Prasad Naldurg

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2019.1.pdf
  • Filesize: 0.9 MB
  • 12 pages

Document Identifiers

Author Details

Karthikeyan Bhargavan
  • Inria, Paris, France
Prasad Naldurg
  • Inria, Paris, France

Cite As Get BibTex

Karthikeyan Bhargavan and Prasad Naldurg. Practical Formal Methods for Real World Cryptography (Invited Talk). In 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 150, pp. 1:1-1:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.FSTTCS.2019.1

Abstract

Cryptographic algorithms, protocols, and applications are difficult to implement correctly, and errors and vulnerabilities in their code can remain undiscovered for long periods before they are exploited. Even highly-regarded cryptographic libraries suffer from bugs like buffer overruns, incorrect numerical computations, and timing side-channels, which can lead to the exposure of sensitive data and long-term secrets. We describe a tool chain and framework based on the F* programming language to formally specify, verify and compile high-performance cryptographic software that is secure by design. This tool chain has been used to build a verified cryptographic library called HACL*, and provably secure implementations of sophisticated secure communication protocols like Signal and TLS. We describe these case studies and conclude with ongoing work on using our framework to build verified implementations of privacy preserving machine learning software.

Subject Classification

ACM Subject Classification
  • Security and privacy → Formal security models
  • Security and privacy → Logic and verification
Keywords
  • Formal verification
  • Applied cryptography
  • Security protocols
  • Machine learning

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Signal. URL: https://signal.org/docs/.
  2. ChaCha20 and Poly1305 for IETF Protocols. IETF RFC 7539, 2015. Google Scholar
  3. Elliptic Curves for Security. IETF RFC 7748, 2016. Google Scholar
  4. Edwards-Curve Digital Signature Algorithm (EdDSA) . IETF RFC 8032, 2017. Google Scholar
  5. Martín Abadi, Ashish Agarwal, Paul Barham, Eugene Brevdo, Zhifeng Chen, Craig Citro, Greg S. Corrado, Andy Davis, Jeffrey Dean, Matthieu Devin, Sanjay Ghemawat, Ian Goodfellow, Andrew Harp, Geoffrey Irving, Michael Isard, Yangqing Jia, Rafal Jozefowicz, Lukasz Kaiser, Manjunath Kudlur, Josh Levenberg, Dan Mané, Rajat Monga, Sherry Moore, Derek Murray, Chris Olah, Mike Schuster, Jonathon Shlens, Benoit Steiner, Ilya Sutskever, Kunal Talwar, Paul Tucker, Vincent Vanhoucke, Vijay Vasudevan, Fernanda Viégas, Oriol Vinyals, Pete Warden, Martin Wattenberg, Martin Wicke, Yuan Yu, and Xiaoqiang Zheng. TensorFlow: Large-scale machine learning on heterogeneous systems, 2015. Software available from tensorflow.org. URL: http://tensorflow.org/.
  6. José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Arthur Blot, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Hugo Pacheco, Benedikt Schmidt, and Pierre-Yves Strub. Jasmin: High-Assurance and High-Speed Cryptography. In ACM SIGSAC Conference on Computer and Communications Security (CCS), pages 1807-1823, 2017. Google Scholar
  7. Andrew W Appel. Verification of a cryptographic primitive: SHA-256. ACM Transactions on Programming Languages and Systems (TOPLAS), 37(2):7, 2015. Google Scholar
  8. Daniel J Bernstein, Tanja Lange, and Peter Schwabe. The security impact of a new cryptographic library. In International Conference on Cryptology and Information Security in Latin America (LATINCRYPT), pages 159-176. Springer, 2012. Google Scholar
  9. Benjamin Beurdouche, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, and Jean Karim Zinzindohoue. A Messy State of the Union: Taming the Composite State Machines of TLS. In IEEE Symposium on Security and Privacy, pages 535-552, 2015. Google Scholar
  10. Karthikeyan Bhargavan, Bruno Blanchet, and Nadim Kobeissi. Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate. In IEEE Symposium on Security and Privacy, pages 483-503, 2017. Google Scholar
  11. Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, Cédric Fournet, Chris Hawblitzel, Catalin Hritcu, Samin Ishtiaq, Markulf Kohlweiss, Rustan Leino, Jay Lorch, Kenji Maillard, Jianyang Pang, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella-Béguelin, and Jean-Karim Zinzindohoué. Everest: Towards a Verified, Drop-in Replacement of HTTPS. In Summit on Advances in Programming Languages (SNAPL), 2017. Google Scholar
  12. Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Jianyang Pan, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy, Santiago Zanella-Béguelin, and Jean Karim Zinzindohoué. Implementing and Proving the TLS 1.3 Record Layer. In Proceedings of the IEEE Symposium on Security and Privacy, 2017. Google Scholar
  13. Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Alfredo Pironti, and Pierre-Yves Strub. Triple Handshakes and Cookie Cutters: Breaking and Fixing Authentication over TLS. In IEEE Symposium on Security and Privacy, pages 98-113, 2014. Google Scholar
  14. Bruno Blanchet. Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif. Foundations and Trends in Privacy and Security, 1(1-2):1-135, October 2016. Google Scholar
  15. Barry Bond, Chris Hawblitzel, Manos Kapritsos, K. Rustan M. Leino, Jacob R. Lorch, Bryan Parno, Ashay Rane, Srinath Setty, and Laure Thompson. Vale: Verifying High-Performance Cryptographic Assembly Code. In USENIX Security Symposium, 2017. Google Scholar
  16. Dan Boneh, Eu-Jin Goh, and Kobbi Nissim. Evaluating 2-DNF Formulas on Ciphertexts. In Theory of Cryptography Conference (TCC), pages 325-341, 2005. Google Scholar
  17. Dan Boneh, Amit Sahai, and Brent Waters. Functional Encryption: Definitions and Challenges. In Theory of Cryptography Conference (TCC), pages 253-273, 2011. Google Scholar
  18. Raphael Bost, Raluca Ada Popa, Stephen Tu, and Shafi Goldwasser. Machine Learning Classification over Encrypted Data. In Network and Distributed System Security Symposium (NDSS), 2015. Google Scholar
  19. Billy B Brumley, Manuel Barbosa, Dan Page, and Frederik Vercauteren. Practical realisation and elimination of an ECC-related software bug attack. In Topics in Cryptology (CT-RSA), pages 171-186. Springer, 2012. Google Scholar
  20. Yu-Fang Chen, Chang-Hong Hsu, Hsin-Hung Lin, Peter Schwabe, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang, and Shang-Yi Yang. Verifying Curve25519 Software. In ACM SIGSAC Conference on Computer and Communications Security (CCS), pages 299-309, 2014. Google Scholar
  21. Katriel Cohn-Gordon, Cas J. F. Cremers, and Luke Garratt. On Post-compromise Security. In IEEE Computer Security Foundations Symposium (CSF), pages 164-178, 2016. Google Scholar
  22. Ivan Damgård, Martin Geisler, and Mikkel Krøigaard. Efficient and Secure Comparison for On-Line Auctions. In Josef Pieprzyk, Hossein Ghodosi, and Ed Dawson, editors, Information Security and Privacy, 2007. Google Scholar
  23. Ivan Damgard, Martin Geisler, and Mikkel Kroigard. A Correction to "Efficient and Secure Comparison for On-Line Auctions". Int. J. Appl. Cryptol., 1(4), August 2008. Google Scholar
  24. Jason A. Donenfeld. WireGuard: Next Generation Kernel Network Tunnel. In Network and Distributed System Security Symposium (NDSS), 2017. Google Scholar
  25. Cynthia Dwork. Differential Privacy. In International Conference on Automata, Languages and Programming (ICALP) - Volume Part II, 2006. Google Scholar
  26. A. Erbsen, J. Philipoom, J. Gross, R. Sloan, and A. Chlipala. Simple High-Level Code for Cryptographic Arithmetic - With Proofs, Without Compromises. In IEEE Symposium on Security and Privacy, 2019. Google Scholar
  27. Craig Gentry. A Fully Homomorphic Encryption Scheme. PhD thesis, Stanford University, Stanford, USA, 2009. Google Scholar
  28. Craig Gentry and Shai Halevi. Implementing Gentry’s Fully-homomorphic Encryption Scheme. In Advances in Cryptology (EUROCRYPT), pages 129-148, 2011. Google Scholar
  29. Shafi Goldwasser and Silvio Micali. Probabilistic Encryption & How to Play Mental Poker Keeping Secret All Partial Information. In ACM Symposium on Theory of Computing (STOC), 1982. Google Scholar
  30. Trinabh Gupta, Henrique Fingler, Lorenzo Alvisi, and Michael Walfish. Pretzel: Email Encryption and Provider-supplied Functions Are Compatible. In Conference of the ACM Special Interest Group on Data Communication (SIGCOMM), pages 169-182, 2017. Google Scholar
  31. Andreas Haas, Andreas Rossberg, Derek L. Schuff, Ben L. Titzer, Michael Holman, Dan Gohman, Luke Wagner, Alon Zakai, and JF Bastien. Bringing the Web Up to Speed with WebAssembly. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 185-200, 2017. Google Scholar
  32. Chiraag Juvekar, Vinod Vaikuntanathan, and Anantha Chandrakasan. GAZELLE: A low latency framework for secure neural network inference. In USENIX Security Symposium, pages 1651-1669, 2018. Google Scholar
  33. Nadim Kobeissi, Karthikeyan Bhargavan, and Bruno Blanchet. Automated verification for secure messaging protocols and their implementations: A symbolic and computational approach. In IEEE European Symposium on Security and Privacy (EuroSP), pages 435-450, 2017. Google Scholar
  34. Eleftheria Makri, Dragos Rotaru, Nigel P. Smart, and Frederik Vercauteren. EPIC: Efficient Private Image Classification (or: Learning from the Masters). Topics in Cryptology (CT-RSA), 2019. Google Scholar
  35. Moxie Marlinspike and Trevor Perrin. The X3DH Key Agreement Protocol, 2016. URL: https://signal.org/docs/specifications/x3dh/.
  36. Pascal Paillier. Public-key cryptosystems based on composite degree residuosity classes. In International Conference on the Theory and Applications of Cryptographic Techniques, pages 223-238, 1999. Google Scholar
  37. Pascal Paillier. Public-Key Cryptosystems Based on Composite Degree Residuosity Classes. In Advances in Cryptology (EUROCRYPT), pages 223-238, 1999. Google Scholar
  38. Trevor Perrin and Moxie Marlinspike. The Double Ratchet Algorithm, 2016. URL: https://signal.org/docs/specifications/doubleratchet/.
  39. Andy Polyakov, Ming-Hsien Tsai, Bow-Yaw Wang, and Bo-Yin Yang. Verifying Arithmetic Assembly Programs in Cryptographic Primitives. In Conference on Concurrency Theory (CONCUR), 2018. Google Scholar
  40. Jonathan Protzenko, Benjamin Beurdouche, Denis Merigoux, and Karthikeyan Bhargavan. Formally Verified Cryptographic Web Applications in WebAssembly. In IEEE Symposium on Security and Privacy, pages 1256-1274, 2019. Google Scholar
  41. Jonathan Protzenko, Jean-Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Catalin Hritcu, Karthikeyan Bhargavan, Cédric Fournet, and Nikhil Swamy. Verified Low-Level Programming Embedded in F*. PACMPL, 1(ICFP):17:1-17:29, September 2017. Google Scholar
  42. E. Rescorla. The Transport Layer Security (TLS) Protocol Version 1.3, 208. IETF RFC 8446. Google Scholar
  43. Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoue, and Santiago Zanella-Béguelin. Dependent Types and Multi-Monadic Effects in F*. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 256-270, 2016. Google Scholar
  44. National Institute of Standards US Department of Commerce and Technology (NIST). Federal Information Processing Standards Publication 180-4: Secure hash standard (SHS), 2012. Google Scholar
  45. Sameer Wagh, Divya Gupta, and Nishanth Chandran. SecureNN: Efficient and Private Neural Network Training. In Privacy Enhancing Technologies Symposium. (PETS 2019), 2019. Google Scholar
  46. Jean Karim Zinzindohoue, Evmorfia-Iro Bartzia, and Karthikeyan Bhargavan. A Verified Extensible Library of Elliptic Curves. In IEEE Computer Security Foundations Symposium (CSF), pages 296-309, 2016. Google Scholar
  47. Jean-Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan Protzenko, and Benjamin Beurdouche. HACL*: A verified modern cryptographic library. In ACM SIGSAC Conference on Computer and Communications Security (CCS), pages 1789-1806, 2017. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact