José Bacelar Almeida
ABSTRACT
Jasmin is a framework for developing high-speed and high-assurance cryptographic software. The framework is structured around the Jasmin programming language and its compiler. The language is designed for enhancing portability of programs and for simplifying verification tasks. The compiler is designed to achieve predictability and efficiency of the output code (currently limited to x64 platforms), and is formally verified in the Coq proof assistant. Using the supercop framework, we evaluate the Jasmin compiler on representative cryptographic routines and conclude that the code generated by the compiler is as efficient as fast, hand-crafted, implementations. Moreover, the framework includes highly automated tools for proving memory safety and constant-time security (for protecting against cache-based timing attacks). We also demonstrate the effectiveness of the verification tools on a large set of cryptographic routines.
Supplemental Material
- Nadhem J. AlFardan and Kenneth G. Paterson 2013. Lucky Thirteen: Breaking the TLS and DTLS Record Protocols IEEE Symposium on Security and Privacy, SP 2013. IEEE Computer Society, 526--540.Google Scholar
- José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, and Franc cois Dupressoir 2013. Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations. In ACM CCS 13, Ahmad-Reza Sadeghi, Virgil D. Gligor, and Moti Yung (Eds.). ACM Press, 1217--1230.Google Scholar
- José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, and Franc cois Dupressoir. 2016. Verifiable Side-Channel Security of Cryptographic Implementations: Constant-Time MEE-CBC FSE 2016 (LNCS), Thomas Peyrin (Ed.), Vol. Vol. 9783. Springer, Heidelberg, 163--184. https://doi.org/10.1007/978-3-662-52993-5_9Google Scholar
- Jose Carlos Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Franc cois Dupressoir, and Michael Emmi 2016. Verifying Constant-time Implementations. In 25th USENIX Security Symposium (USENIX Security 16). USENIX Association, Austin, TX. https://www.usenix.org/conference/usenixsecurity16/technical-sessions/presentation/almeidaGoogle Scholar
- Andrew W. Appel. 2015. Verification of a Cryptographic Primitive: SHA-256. ACM Trans. Program. Lang. Syst. Vol. 37, 2 (2015), 7:1--7:31. https://doi.org/10.1145/2701415Google ScholarDigital Library
- Andrew W Appel, Robert Dockins, Aquinas Hobor, Lennart Beringer, Josiah Dodds, Gordon Stewart, Sandrine Blazy, and Xavier Leroy. 2014. Program logics for certified compilers. Cambridge University Press.Google ScholarDigital Library
- Michael Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino. 2005. Boogie: A Modular Reusable Verifier for Object-Oriented Programs Formal Methods for Components and Objects, 4th International Symposium, FMCO 2005, Amsterdam, The Netherlands, November 1--4, 2005, Revised Lectures (Lecture Notes in Computer Science), Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem P. de Roever (Eds.), Vol. Vol. 4111. Springer, 364--387. https://doi.org/10.1007/11804192_17Google Scholar
- Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Daniel Luna, and David Pichardie. 2014. System-level Non-interference for Constant-time Cryptography ACM CCS 14, Gail-Joon Ahn, Moti Yung, and Ninghui Li (Eds.). ACM Press, 1267--1279.Google Scholar
- Evmorfia-Iro Bartzia and Pierre-Yves Strub 2014. A Formal Library for Elliptic Curves in the Coq Proof Assistant Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14--17, 2014. Proceedings (Lecture Notes in Computer Science), Gerwin Klein and Ruben Gamboa (Eds.), Vol. Vol. 8558. Springer, 77--92. https://doi.org/10.1007/978-3-319-08970-6_6Google Scholar
- Lennart Beringer, Adam Petcher, Katherine Q. Ye, and Andrew W. Appel 2015. Verified Correctness and Security of OpenSSL HMAC 24th USENIX Security Symposium, USENIX Security 15, Washington, D.C., USA, August 12--14, 2015., Jaeyeon Jung and Thorsten Holz (Eds.). USENIX Association, 207--221. https://www.usenix.org/conference/usenixsecurity15/technical-sessions/presentation/beringerGoogle Scholar
- Dan Bernstein. Writing high-speed software. (????). http://cr.yp.to/qhasm.htmlGoogle Scholar
- Daniel J. Bernstein. 2005. Cache-timing attacks on AES. (2005). shownotehttp://cr.yp.to/antiforgery/cachetiming-20050414.pdf.Google Scholar
- Daniel J. Bernstein. 2006. Curve25519: New Diffie-Hellman Speed Records PKC 2006 (LNCS), Moti Yung, Yevgeniy Dodis, Aggelos Kiayias, and Tal Malkin (Eds.), Vol. Vol. 3958. Springer, Heidelberg, 207--228.Google Scholar
- Daniel J. Bernstein, Niels Duif, Tanja Lange, Peter Schwabe, and Bo-Yin Yang 2011. High-Speed High-Security Signatures. In CHES 2011 (LNCS), Bart Preneel and Tsuyoshi Takagi (Eds.), Vol. Vol. 6917. Springer, Heidelberg, 124--142. Google ScholarCross Ref
- Dan Berstein and Peter Schwabe 2015. gfverif: fast and easy verification of finite-field arithmetic. (2015). http://gfverif.cryptojedi.org/Google Scholar
- Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Catalin Hritcu, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Peng Wang, Santiago Zanella Béguelin, and Jean Karim Zinzindohoué. 2017. Verified Low-Level Programming Embedded in F. CoRR Vol. abs/1703.00053 (2017). http://arxiv.org/abs/1703.00053Google Scholar
- Barry Bond, Chris Hawblitzel, Manos Kapritsos, K. Rustan M. Leino, Jacob R. Lorch, Bryan Parno, Ashay Rane, Srinath Setty, and Laure Thompson 2017. Vale: Verifying High-Performance Cryptographic Assembly Code 26th USENIX Security Symposium (USENIX Security 17). USENIX Association, Vancouver, BC. https://www.usenix.org/conference/usenixsecurity17/technical-sessions/presentation/bondGoogle Scholar
- Billy Bob Brumley, Manuel Barbosa, Dan Page, and Frederik Vercauteren 2012. Practical Realisation and Elimination of an ECC-Related Software Bug Attack CT-RSA 2012 (LNCS), Orr Dunkelman (Ed.), Vol. Vol. 7178. Springer, Heidelberg, 171--186.Google Scholar
- Yu-Fang Chen, Chang-Hong Hsu, Hsin-Hung Lin, Peter Schwabe, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang, and Shang-Yi Yang. 2014. Verifying Curve25519 Software. In ACM CCS 14, Gail-Joon Ahn, Moti Yung, and Ninghui Li (Eds.). ACM Press, 299--309. Google ScholarDigital Library
- Leonardo Mendoncca de Moura and Nikolaj Bjørner 2008. Z3: An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings (Lecture Notes in Computer Science), C. R. Ramakrishnan and Jakob Rehof (Eds.), Vol. Vol. 4963. Springer, 337--340. https://doi.org/10.1007/978-3-540-78800-3_24Google ScholarCross Ref
- Vijay D'Silva, Mathias Payer, and Dawn Xiaodong Song. 2015. The Correctness-Security Gap in Compiler Optimization 2015 IEEE Symposium on Security and Privacy Workshops, SPW 2015, San Jose, CA, USA, May 21--22, 2015. IEEE Computer Society, 73--87. https://doi.org/10.1109/SPW.2015.33Google Scholar
- Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, and Adam Chlipala 2017. Systematic Synthesis of Elliptic Curve Cryptography Implementations. (2017). https://people.csail.mit.edu/jgross/personal-website/papers/2017-fiat-crypto-pldi-draft.pdfGoogle Scholar
- Shay Gueron and Vlad Krasnov 2013. The fragility of AES-GCM authentication algorithm. Cryptology ePrint Archive, Report 2013/157. (2013). http://eprint.iacr.org/2013/157.Google Scholar
- Darrel Hankerson, Alfred Menezes, and Scott Vanstone. 2004. Guide to elliptic curve cryptography. (2004).Google Scholar
- Jacques-Henri Jourdan, François Pottier, and Xavier Leroy. 2012. Validating LR(1) Parsers. In European Symposium on Programming (ESOP). Springer, 397--416.Google ScholarDigital Library
- Thierry Kaufmann, Hervé Pelletier, Serge Vaudenay, and Karine Villegas 2016. When Constant-Time Source Yields Variable-Time Binary: Exploiting Curve25519-donna Built with MSVC 2015. In Cryptology and Network Security - 15th International Conference, CANS 2016, Milan, Italy, November 14--16, 2016, Proceedings (Lecture Notes in Computer Science), Sara Foresti and Giuseppe Persiano (Eds.), Vol. Vol. 10052. 573--582. https://doi.org/10.1007/978-3-319-48965-0_36Google Scholar
- K. Rustan M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Selected Papers (Lecture Notes in Computer Science), Edmund M. Clarke and Andrei Voronkov (Eds.), Vol. Vol. 6355. Springer, 348--370. https://doi.org/10.1007/978--3--642--17511--4_20Google Scholar
- Xavier Leroy. 2006. Formal certification of a compiler back-end, or: programming a compiler with a proof assistant 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006. ACM, 42--54.Google Scholar
- George C. Necula. Translation validation for an optimizing compiler. ACM sigplan notices (2000), Vol. Vol. 35. ACM, 83--94. Google ScholarDigital Library
- Aina Niemetz, Mathias Preiner, and Armin Biere 2014 (published 2015). Boolector 2.0 system description. Journal on Satisfiability, Boolean Modeling and Computation Vol. 9 (2014 (published 2015)), 53--58.Google Scholar
- Adam Petcher and Greg Morrisett 2015. The Foundational Cryptography Framework. In Principles of Security and Trust - 4th International Conference, POST 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings (Lecture Notes in Computer Science), Riccardo Focardi and Andrew C. Myers (Eds.), Vol. Vol. 9036. Springer, 53--72. https://doi.org/10.1007/978-3-662-46666-7_4Google ScholarDigital Library
- Massimiliano Poletto and Vivek Sarkar 1999. Linear scan register allocation. Vol. 21, 5 (1999), 895--913.Google ScholarDigital Library
- Bruno Rodrigues, Fernando Magno Quint ao Pereira, and Diego F. Aranha. 2016. Sparse representation of implicit flows with applications to side-channel detection Proceedings of the 25th International Conference on Compiler Construction, CC 2016, Barcelona, Spain, March 12--18, 2016, Ayal Zaks and Manuel V. Hermenegildo (Eds.). ACM, 110--120. https://doi.org/10.1145/2892208.2892230Google Scholar
- Katherine Ye, Matthew Green, Naphat Sanguansin, Lennart Beringer, Adam Petcher, and Andrew W. Appel 2017. Verified correctness and security of mbedTLS HMAC-DRBG ACM CCS 2017.Google Scholar
- Jean Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan Protzenko, and Benjamin Beurdouche. 2017. HACL*: A Verified Modern Cryptographic Library. IACR Cryptology ePrint Archive Vol. 2017 (2017), 536. http://eprint.iacr.org/2017/536Google Scholar
- Jean Karim Zinzindohoué, Evmorfia-Iro Bartzia, and Karthikeyan Bhargavan 2016. A Verified Extensible Library of Elliptic Curves. IEEE 29th Computer Security Foundations Symposium, CSF 2016, Lisbon, Portugal, June 27 - July 1, 2016. IEEE Computer Society, 296--309. https://doi.org/10.1109/CSF.2016.28Google ScholarCross Ref
Index Terms
- Jasmin: High-Assurance and High-Speed Cryptography
Recommendations
A formally verified sequentializer for lustre-like concurrent synchronous data-flow programs
ICSE-C '17: Proceedings of the 39th International Conference on Software Engineering CompanionSynchronous data-flow languages (SDFL), such as Lustre [1], is a concurrent language that has been widely used in safety-critical systems. Verified compilers for such languages are crucial in generating trustworthy object code. A good approach is to ...
Towards a verified compiler prototype for the synchronous language SIGNAL
SIGNAL belongs to the synchronous languages family which are widely used in the design of safety-critical real-time systems such as avionics, space systems, and nuclear power plants. This paper reports a compiler prototype for SIGNAL. Compared with the ...
Formal verification of control-flow graph flattening
CPP 2016: Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and ProofsCode obfuscation is emerging as a key asset in security by obscurity. It aims at hiding sensitive information in programs so that they become more difficult to understand and reverse engineer. Since the results on the impossibility of perfect and ...
Comments