Abstract
We analyse and exploit implementation features in OpenSSL version 0.9.8g which permit an attack against ECDH-based functionality. The attack, although more general, can recover the entire (static) private key from an associated SSL server via 633 adaptive queries when the NIST curve P-256 is used. One can view it as a software-oriented analogue of the bug attack concept due to Biham et al. and, consequently, as the first bug attack to be successfully applied against a real-world system. In addition to the attack and a posteriori countermeasures, we show that formal verification, while rarely used at present, is a viable means of detecting the features which the attack hinges on. Based on the security implications of the attack and the extra justification posed by the possibility of intentionally incorrect implementations in collaborative software development, we conclude that applying and extending the coverage of formal verification to augment existing test strategies for OpenSSL-like software should be deemed a worthwhile, long-term challenge.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Antipa, A., Brown, D.R.L., Menezes, A., Struik, R., Vanstone, S.A.: Validation of Elliptic Curve Public Keys. In: Desmedt, Y.G. (ed.) PKC 2003. LNCS, vol. 2567, pp. 211–223. Springer, Heidelberg (2002)
Barbosa, M.: CACE Deliverable D5.2: formal specification language definitions and security policy extensions (2009), http://www.cace-project.eu
Barbosa, M., Moss, A., Page, D.: Constructive and destructive use of compilers in elliptic curve cryptography. J. Cryptology 22(2), 259–281 (2009)
Biham, E., Carmeli, Y., Shamir, A.: Bug Attacks. In: Wagner, D. (ed.) CRYPTO 2008. LNCS, vol. 5157, pp. 221–240. Springer, Heidelberg (2008)
Ciet, M., Joye, M.: Elliptic curve cryptosystems in the presence of permanent and transient faults. Designs, Codes and Cryptography 36(1), 33–43 (2005)
Conchon, S., Contejean, E., Kanig, J.: Ergo : a theorem prover for polymorphic first-order logic modulo theories (2006), http://ergo.lri.fr/papers/ergo.ps
Coron, J.-S.: Resistance against Differential Power Analysis for Elliptic Curve Cryptosystems. In: Koç, Ç.K., Paar, C. (eds.) CHES 1999. LNCS, vol. 1717, pp. 292–302. Springer, Heidelberg (1999)
Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365–473 (2005)
Filliâtre, J.-C., Marché, C.: Multi-Prover Verification of C Programs. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 15–29. Springer, Heidelberg (2004)
Filliâtre, J.-C., Marché, C.: The Why/Krakatoa/Caduceus Platform for Deductive Program Verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 173–177. Springer, Heidelberg (2007)
Herley, C.: So long, and no thanks for the externalities: The rational rejection of security advice by users. In: New Security Paradigms Workshop (NSPW), pp. 133–144 (2009)
Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM 12, 576–580 (1969)
Montgomery, P.L.: Speeding the Pollard and elliptic curve methods of factorization. Math. Comp. 48(177), 243–264 (1987)
Nguyen, P.Q.: Can We Trust Cryptographic Software? Cryptographic Flaws in GNU Privacy Guard v1.2.3. In: Cachin, C., Camenisch, J.L. (eds.) EUROCRYPT 2004. LNCS, vol. 3027, pp. 555–570. Springer, Heidelberg (2004)
Paterson, K.G., Yau, A.K.L.: Cryptography in Theory and Practice: The Case of Encryption in IPsec. In: Vaudenay, S. (ed.) EUROCRYPT 2006. LNCS, vol. 4004, pp. 12–29. Springer, Heidelberg (2006)
Reimann, H.: BN_nist_mod_384 gives wrong answers. openssl-dev mailing list #1593 (2007), http://marc.info/?t=119271238800004
Solinas, J.A.: Generalized Mersenne numbers. Technical Report CORR 99-39, Centre for Applied Cryptographic Research (CACR), University of Waterloo (1999), http://www.cacr.math.uwaterloo.ca/techreports/1999/corr99-39.pdf
The Coq Development Team. The Coq Proof Assistant Reference Manual – Version V8.2 (2008), http://coq.inria.fr
Vieira, B., Barbosa, M., Sousa Pinto, J., Filliatre, J.-C.: A deductive verification platform for cryptographic software. In: International Workshop on Foundations and Techniques for Open Source Software Certification, OpenCert (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Brumley, B.B., Barbosa, M., Page, D., Vercauteren, F. (2012). Practical Realisation and Elimination of an ECC-Related Software Bug Attack. In: Dunkelman, O. (eds) Topics in Cryptology – CT-RSA 2012. CT-RSA 2012. Lecture Notes in Computer Science, vol 7178. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-27954-6_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-27954-6_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-27953-9
Online ISBN: 978-3-642-27954-6
eBook Packages: Computer ScienceComputer Science (R0)