Yu-Fang Chen
ABSTRACT
This paper presents results on formal verification of high-speed cryptographic software. We consider speed-record-setting hand-optimized assembly software for Curve25519 elliptic-curve key exchange presented by Bernstein et al. at CHES 2011. Two versions for different microarchitectures are available. We successfully verify the core part of the computation, and reproduce detection of a bug in a previously published edition. An SMT solver supporting array and bit-vector theories is used to establish almost all properties. Remaining properties are verified in a proof assistant with simple rewrite tactics. We also exploit the compositionality of Hoare logic to address the scalability issue. Essential differences between both versions of the software are discussed from a formal-verification perspective.
- R. Affeldt. On construction of a library of formally verified low-level arithmetic functions. Innovations in Systems and Software Engineering, 9(2):59--77, 2013. https://staff.aist.go.jp/reynald.affeldt/documents/arilib-affeldt.pdf. Google Scholar
Digital Library
- R. Affeldt and N. Marti. An approach to formal verification of arithmetic functions in assembly. In M. Okada and I. Satoh, editors, Advances in Computer Science -- ASIAN 2006, volume 4435 of Lecture Notes in Computer Science, pages 346--360. Springer-Verlag Berlin Heidelberg, 2007. https://staff.aist.go.jp/reynald.affeldt/documents/affeldt-asian2006.pdf. Google ScholarDigital Library
- R. Affeldt, D. Nowak, and K. Yamada. Certifying assembly with formal security proofs: The case of BBS. Science of Computer Programming, 77(10--11):1058{1074, 2012. http://www.sciencedirect.com/science/article/pii/S0167642311001493. Google ScholarDigital Library
- J. B. Almeida, M. Barbosa, G. Barthe, and F. Dupressoir. Certified computer-aided cryptography: effcient provably secure machine code from high-level implementations. In V. Gligor and M. Yung, editors, Proceedings of the 2013 ACM SIGSAC conference on Computer & communications security, pages 1217--1230. ACM New York, 2013. http://eprint.iacr.org/2013/316/. Google ScholarDigital Library
- B. Alpern, M. N. Wegman, and F. K. Zadeck. Detecting equality of variables in programs. In ACM Symposium on Principles of Programming Languages -- (POPL 1988), pages 1--11. ACM Press, 1988. http://courses.cs.washington.edu/courses/cse501/04wi/papers/alpern-popl88.pdf. Google ScholarDigital Library
- R. Avanzi, H. Cohen, C. Doche, G. Frey, T. Lange, K. Nguyen, and F. Vercauteren. Handbook of Elliptic and Hyperelliptic Curve Cryptography. Chapman & Hall/CRC, 2006. Google ScholarDigital Library
- E.-I. Bartzia. Formalisation des courbes elliptiques en coq. Master's thesis, Universite de Vincennes-Saint Denis { Paris VIII, 2011. http://pierre-yves.strub.nu/research/ec/.Google Scholar
- A. G. Bayrak, F. Regazzoni, D. Novo, and P. Ienne. Sleuth: Automated verification of software power analysis countermeasures. In G. Bertoni and J.-S. Coron, editors, Cryptographic Hardware and Embedded Systems -- CHES 2013, volume 8086 of Lecture Notes in Computer Science, pages 293--310. Springer-Verlag Berlin Heidelberg, 2013. Google ScholarDigital Library
- D. J. Bernstein. qhasm: tools to help write high-speed software. http://cr.yp.to/qhasm.html.Google Scholar
- D. J. Bernstein. Supercop: System for unified performance evaluation related to cryptographic operations and primitives. http://bench.cr.yp.to/supercop.html. Published as part of ECRYPT II VAMPIRE Lab.Google Scholar
- D. J. Bernstein. Curve25519: new Diffie-Hellman speed records. In M. Yung, Y. Dodis, A. Kiayias, and T. Malkin, editors, Public Key Cryptography -- PKC 2006, volume 3958 of Lecture Notes in Computer Science, pages 207{228. Springer-Verlag Berlin Heidelberg, 2006. http://cr.yp.to/papers.html#curve25519. Google ScholarDigital Library
- D. J. Bernstein. Batch binary Edwards. In S. Halevi, editor, Advances in Cryptology -- CRYPTO 2009, volume 5677 of Lecture Notes in Computer Science, pages 317--336. Springer-Verlag Berlin Heidelberg, 2009. http://cr.yp.to/papers.html#bbe. Google ScholarDigital Library
- D. J. Bernstein, N. Duif, T. Lange, P. Schwabe, and B.-Y. Yang. High-speed high-security signatures. In B. Preneel and T. Takagi, editors, Cryptographic Hardware and Embedded Systems -- CHES 2011, volume 6917 of Lecture Notes in Computer Science, pages 124--142. Springer-Verlag Berlin Heidelberg, 2011. see also full version {14}. Google ScholarDigital Library
- D. J. Bernstein, N. Duif, T. Lange, P. Schwabe, and B.-Y. Yang. High-speed high-security signatures. Journal of Cryptographic Engineering, 2(2):77--89, 2012. http://cryptojedi.org/papers/#ed25519, see also short version {13}.Google ScholarCross Ref
- D. J. Bernstein and T. L. (editors). eBACS: ECRYPT Benchmarking of Cryptographic Systems. http://bench.cr.yp.to (accessed May 17, 2014).Google Scholar
- D. J. Bernstein and T. L. (editors). Explicit-formulas database. http://www.hyperelliptic.org/EFD/ (accessed May 17, 2014).Google Scholar
- D. J. Bernstein, W. Janssen, T. Lange, and P. Schwabe. TweetNaCl: A crypto library in 100 tweets, 2013. http://cryptojedi.org/papers/#tweetnacl.Google Scholar
- D. J. Bernstein, T. Lange, and P. Schwabe. The security impact of a new cryptographic library. In A. Hevia and G. Neven, editors, Progress in Cryptology -- LATINCRYPT 2012, volume 7533 of Lecture Notes in Computer Science, pages 159--176.Springer-Verlag Berlin Heidelberg, 2012. http://cryptojedi.org/papers/#coolnacl. Google ScholarDigital Library
- Y. Bertot and P. Cast--eran. Interactive Theorem Proving and Program Development Coq'Art: The Calculus of Inductive Constructions. EATCS. Springer, 2004. Google ScholarDigital Library
- K. Bhargavan, A. Delignat-Lavaud, C. Fournet, M. Kohlweiss, A. Pironti, P.-Y. Strub, and S. Zanella-Beguelin. miTLS: A verified reference TLS implementation, 2014. http://www.mitls.org/wsgi/home.Google Scholar
- K. Bhargavan, C. Fournet, M. Kohlweiss, A. Pironti, and P.-Y. Strub. Implementing TLS with verified cryptographic security. In IEEE Symposium on Security and Privacy 2013, pages 445--459, 2013. full version: http://www.mitls.org/downloads/miTLS-report.pdf. Google ScholarDigital Library
- B. B. Brumley, M. Barbosa, D. Page, and F. Vercauteren. Practical realisation and elimination of an ECC-related software bug attack. In O. Dunkelman, editor, Topics in Cryptology -- CT-RSA 2012, volume 7178 of Lecture Notes in Computer Science, pages 171--186. Springer-Verlag Berlin Heidelberg, 2012. http://eprint.iacr.org/2011/633. Google ScholarDigital Library
- R. Brummayer and A. Biere. Boolector: An effcient SMT solver for bit-vectors and arrays. In S. Kowalewski and A. Philippou, editors, Tools and Algorithms for the Construction and Analysis of Systems -- (TACAS 2009), volume 5505 of Lecture Notes in Computer Science, pages 174--177. Springer-Verlag Berlin Heidelberg, 2009. http://fmv.jku.at/papers/BrummayerBiere-TACAS09.pdf. Google ScholarDigital Library
- C. Costello, H. Hisil, and B. Smith. Faster compact diffie--hellman: Endomorphisms on the x-line. In P. Q. Nguyen and E. Oswald, editors, Advances in Cryptology -- EUROCRYPT 2014, volume 8441 of Lecture Notes in Computer Science, pages 183--200. Springer-Verlag Berlin Heidelberg, 2014. http://eprint.iacr.org/2013/692/.Google Scholar
- M. D. Ernst, J. H. Perkins, P. J. Guo, S. McCamant, C. Pacheco, M. S. Tschantz, and C. Xiao. The daikon system for dynamic detection of likely invariants. Sci. Comput. Program., 69(1{3):35{45, 2007. http://pgbovine.net/publications/ daikon-invariant-detector_SCP-2007.pdf. Google ScholarDigital Library
- M. Gordon. CryptVer project. http://www.cl.cam.ac.uk/~mjcg/proposals/CryptVer/.Google Scholar
- D. Hankerson, A. Menezes, and S. A. Vanstone. Guide to Elliptic Curve Cryptography. Springer-Verlag New York, 2004. Google ScholarDigital Library
- C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576--580, 1969. http://www.spatial.maine.edu/~worboys/processes/hoare/20axiomatic.pdf. Google ScholarDigital Library
- P. Longa and F. Sica. Four-dimensional Gallant-Lambert-Vanstone scalar multiplication. In X. Wang and K. Sako, editors, Advances in Cryptology -- ASIACRYPT 2012, volume 7658 of Lecture Notes in Computer Science, pages 718{739. Springer-Verlag Berlin Heidelberg, 2012. https://eprint.iacr.org/2011/608. Google ScholarDigital Library
- D. Molnar, M. Piotrowski, D. Schultz, and D. Wagner. The program counter security model: Automatic detection and removal of control-flow side channel attacks. In D. H. Won and S. Kim, editors, Information Security and Cryptology -- ICISC 2005, volume 3935 of Lecture Notes in Computer Science, pages 156--168. Springer-Verlag Berlin Heidelberg, 2005. Full version at http://eprint.iacr.org/2005/368/. Google ScholarDigital Library
- P. L. Montgomery. Speeding the Pollard and elliptic curve methods of factorization. Mathematics ofComputation, 48(177):243--264, 1987. http://www.ams.org/journals/mcom/1987--48--177/S0025--5718--1987-0866113--7/S0025--5718--1987-0866113--7.pdf.Google ScholarCross Ref
- M. O. Myreen and M. J. C. Gordon. Hoare logic for realistically modelled machine code. In O. Grumberg and M. Huth, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 4424 of Lecture Notes in Computer Science, pages 568--582. Springer-Verlag Berlin Heidelberg, 2007. http: //www.cl.cam.ac.uk/~mom22/mc-hoare-logic.pdf. Google ScholarDigital Library
- T. Oliveira, J. Lopez, D. F. Aranha, and F. Rodrguez-Henrquez. Lambda coordinates for binary elliptic curves. In G. Bertoni and J.-S. Coron, editors, Cryptographic Hardware and Embedded Systems -- CHES 2013, volume 8086 of Lecture Notes in Computer Science, pages 311--330. Springer-Verlag Berlin Heidelberg, 2013. http: //eprint.iacr.org/2013/131/20130611:205154. Google ScholarDigital Library
- S. Ragan. Bugcrowd launches funding drive to audit popenssl. News article on CSO, 2014. http://www.csoonline.com/article/2145020/security-industry/ bugcrowd-launches-funding-drive-to-audit-openssl. html (accessed May 17, 2014).Google Scholar
- B. K. Rosen, M. N. Wegman, and F. K. Zadeck. Global value numbers and redundant computations. In ACM Symposium on Principles of Programming Languages -- (POPL 1988), pages 12--27. ACM Press, 1988. http://www.cs.wustl.edu/~cytron/cs531/ Resources/Papers/valnum.pdf. Google ScholarDigital Library
- L. Thery and G. Hanrot. Primality proving with elliptic curves. In K. Schneider and J. Brandt, editors, Theorem Proving in Higher Order Logics, volume 4732 of Lecture Notes in Computer Science, pages 319--333. Springer-Verlag Berlin Heidelberg, 2007. http://hal.inria.fr/docs/00/14/06/58/PDF/paper.pdf. Google ScholarDigital Library
- K. White and M. Green. IsTrueCryptAuditedYet? http://istruecryptauditedyet.com/ (accessed May 17, 2014).Google Scholar
Index Terms
- Verifying Curve25519 Software
Recommendations
Inductive Completeness of Logics of Programs
We propose a new approach to delineating logics of programs, based directly on inductive definition of program semantics. The ingredients are elementary and well-known, but their fusion yields a simple yet powerful approach, surprisingly overlooked for ...
Completeness and decidability of converse PDL in the constructive type theory of Coq
CPP 2018: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and ProofsThe completeness proofs for Propositional Dynamic Logic (PDL) in the literature are non-constructive and usually presented in an informal manner. We obtain a formal and constructive completeness proof for Converse PDL by recasting a completeness proof ...
Comments