nach oben

Journal of Cryptographic Engineering

Erschienen in:

01.09.2016 | Special Section on Proofs 2014

Formally proved security of assembly code against power analysis

A case study on balanced logic

verfasst von: Pablo Rauzy, Sylvain Guilley, Zakaria Najm

Erschienen in: Journal of Cryptographic Engineering | Ausgabe 3/2016

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

In his keynote speech at CHES 2004, Kocher advocated that side-channel attacks were an illustration that formal cryptography was not as secure as it was believed because some assumptions (e.g., no auxiliary information is available during the computation) were not modeled. This failure is caused by formal methods’ focus on models rather than implementations. In this paper, we present formal methods and tools for designing protected code and proving its security against power analysis. These formal methods avoid the discrepancy between the model and the implementation by working on the latter rather than on a high-level model. Indeed, our methods allow us (a) to automatically insert a power balancing countermeasure directly at the assembly level, and to prove the correctness of the induced code transformation; and (b) to prove that the obtained code is balanced with regard to a reasonable leakage model. We also show how to characterize the hardware to use the resources which maximize the relevancy of the model. The tools implementing our methods are then demonstrated in a case study on an 8-bit AVR smartcard for which we generate a provably protected present implementation that reveals to be at least 250 times more resistant to CPA attacks.

Vorheriger Artikel Inversion-free arithmetic on elliptic curves through isomorphisms

Nächster Artikel Physical functions: the common factor of side-channel and fault attacks?

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Nur mit Berechtigung zugänglich

For convenience, we use regular expressions notation.

Intuitively, the proof invokes the Universal Turing Machines equivalence (those that work with only \(\{0,1\}\) as alphabet are as powerful as the others).

Other works consider that a sensitive data must depend on both the secret key and the plaintext (as it is usually admitted in the “only computation leaks” paradigm; see for instance [41, §4.1]). Our definition is broader, in particular it also encompasses the random probing model [24].

These differences are due to the internal architecture of the chip, for which we do not have the specifications.

Notice that present is inherently slow in software (optimized non-bitsliced assembly is reported to run in about 11,000 clock cycles on an Atmel ATtiny 45 device [15]) because it is designed for hardware. Typically, the permutation layer is free in hardware, but requires many bit-level manipulations in software. Nonetheless, we outline that there are contexts where present must be supported, but no hardware accelerator is available.

We insist that the comparison between two security gains is very platform-dependent. The figures we give are only valid on our specific setup. Of course, for different conditions, e.g., lower signal-to-noise ratio, masking might become more secure than DPL.

http://pablo.rauzy.name/sensi/paioli.html.

http://ocaml.org/.

Note that using the maximum correlation point to attack the DPL implementations resulted in the success rate remaining always at \(\approx 1/{16}\) (there are \(2^4\) key guesses in present when targeting the first round, because the substitution boxes are \(4 \times 4\)) in average [at least on the number of traces we had (100,000)] on both on them.

Battistello, A., Giraud, C.: Fault analysis of infective AES computations. In: Fischer, W., Schmidt, J.-M., (Eds.), 2013 Workshop on Fault Diagnosis and Tolerance in Cryptography. Los Alamitos, CA, USA, August 20, 2013, IEEE, pp. 101–107, Santa Barbara, CA, USA (2013)

Bhasin, S., Danger, J.-L., Guilley, S., Zakaria, N.: NICV: normalized inter-class variance for detection of side-channel leakage. In: International symposium on electromagnetic compatibility (EMC ’14 / Tokyo). IEEE, (May 12–16 2014). Session OS09: EM Information Leakage. Hitotsubashi Hall (National Center of Sciences), Chiyoda, Tokyo, Japan (2014)

Bhasin, S., Danger, J.-L., Guilley, S., Zakaria, N.: Side-channel leakage and trace compression using normalized inter-class variance. In: Proceedings of the Third Workshop on Hardware and Architectural Support for Security and Privacy, HASP ’14, pp. 7:1–7:9, ACM, New York, NY, USA (2014)

Biham, E.: A fast new DES Implementation in software. In: Biham, E. (ed.), FSE, volume 1267 of Lecture Notes in Computer Science, pp. 260–272, Springer, Berlin (1997)

Bogdanov, A., Knudsen, L.R., Leander, G., Paar, C., Poschmann, A., Robshaw, M.J. B., Seurin, Y., Vikkelsoe, C.: PRESENT: an ultra-lightweight block cipher. In: CHES, volume 4727 of LNCS, pp. 450–466, Springer, Berlin (September 10–13 2007). Vienna, Austria (2007)

Brier, É., Clavier, C., Olivier, F.: Correlation power analysis with a leakage model. In: CHES, volume 3156 of LNCS, pp. 16–29, Springer, Berlin (August 11–13 2004). Cambridge, MA, USA (2004)

Carlet, C., Faugère, J.-C., Goyet, C., Renault, G.: Analysis of the algebraic side channel attack. J. Cryptogr. Eng. 2(1), 45–62 (2012)CrossRef

Carlet, C., Goubin, L., Prouff, E., Quisquater, M., Rivain, M.: Higher-order masking schemes for S-boxes. In: Canteaut, A. (Ed.), Fast Software Encryption—19th International Workshop, FSE 2012, Washington, DC, USA, March 19–21, 2012. Revised Selected Papers, volume 7549 of Lecture Notes in Computer Science, pp. 366–384, Springer, Berlin (2012)

Chen, C., Eisenbarth, T., Shahverdi, A., Ye, X.: Balanced encoding to mitigate power analysis: a case study. In: CARDIS, Lecture Notes in Computer Science. Springer, Berlin (November 2014). Paris, France (2014)

10.

Chen, Z., Sinha, A., Schaumont, P.: Using virtual secure circuit to protect embedded software from side-channel attacks. IEEE Trans. Comput. 62(1), 124–136 (2013)

11.

Common Criteria Consortium. Common Criteria (aka CC) for Information Technology Security Evaluation (ISO/IEC 15408) (2013). http://www.commoncriteriaportal.org/

12.

Coron, J.-S., Prouff, E., Rivain, M.: Side channel cryptanalysis of a higher order masking scheme. In: Paillier, P., Verbauwhede, I. (Eds.), CHES, volume 4727 of LNCS, pp. 28–44, Springer, Berlin (2007)

13.

Courtois, N., Hulme, D., Mourouzis, T.: Solving circuit optimisation problems in cryptography and cryptanalysis. IACR Cryptology ePrint Archive, 2011:475, 2011. (Also presented in SHARCS 2012, Washington DC, (17–18 March 2012), on page 179)

14.

Doychev, G., Feld, D., Köpf, B., Mauborgne, L., Reineke, J.: CacheAudit: a tool for the static analysis of cache side channels. IACR Cryptol. ePrint Arc. 2013, 253 (2013)

15.

Eisenbarth, T., Gong, Z., Güneysu, T., Heyse, S., Indesteege, S., Kerckhof, S., Koeune, F., Nad, T., Plos, T., Regazzoni, F., Standaert, F.-X., Oldenzeel, L.V.O.: Tot: compact implementation and performance evaluation of block ciphers in attiny devices. In: Mitrokotsa, A., Vaudenay, S. (Eds.), AFRICACRYPT, volume 7374 of Lecture Notes in Computer Science, pp. 172–187, Springer, Berlin (2012)

16.

Eldib, H., Wang, C., Schaumont, P.: Formal verification of software countermeasures against side-channel attacks. ACM Trans. Softw. Eng. Methodol. 24(2), 11:1–11:24 (2014)CrossRef

17.

Guilley, S., Chaudhuri, S., Sauvage, L., Hoogvorst, P., Pacalet, R., Bertoni, G.M.: Security evaluation of WDDL and SecLib countermeasures against power attacks. IEEE Trans. Comput. 57(11), 1482–1497 (2008)MathSciNetCrossRef

18.

Guilley, S., Hoogvorst, P., Mathieu, Y., Pacalet, R.: The “Backend Duplication” method. In: CHES, volume 3659 of LNCS, pp. 383–397. Springer, Berlin, August 29th September 1st, Edinburgh, Scotland, UK (2005)

19.

Guilley, S., Hoogvorst, P., Pacalet, R.: Differential power analysis model and some results. In: Kluwer (Ed.), Proceedings of WCC/CARDIS, pp. 127–142, (Aug 2004), Toulouse, France. (2004). doi:10.1007/1-4020-8147-2_9

20.

Güneysu, T., Moradi, A.: Generic side-channel countermeasures for reconfigurable devices. In:Preneel, B., Takagi, T. (Eds.), CHES, volume 6917 of LNCS, pp. 33–48, Springer, Berlin (2011)

21.

Heuser, A., Rioul, O., Guilley, S.: A theoretical study of kolmogorov-smirnov distinguishers—side-channel analysis vs. differential cryptanalysis. In: Emmanuel P., (Ed.) COSADE, volume 8622 of Lecture Notes in Computer Science, pp. 9–28, Springer, Berlin (2014)

22.

Hoogvorst, P., Danger, J.-L., Duc, G.: Software implementation of dual-rail representation. In: COSADE, (February 24–25 2011). Darmstadt, Germany (2011)

23.

Ishai, Y., Prabhakaran, M., Sahai, A., Wagner, D.: Private circuits II: keeping secrets in tamperable circuits. In: EUROCRYPT, volume 4004 of Lecture Notes in Computer Science, pp. 308–327, Springer, Berlin (May 28–June 1, 2006). St. Petersburg, Russia (2006)

24.

Ishai, Y., Sahai, A., Wagner, D.: Private circuits: securing hardware against probing attacks. In: CRYPTO, volume 2729 of Lecture Notes in Computer Science, pp. 463–481, Springer, Berlin (August 17–21 2003). Santa Barbara, California, USA (2003)

25.

Kocher, P.C.: Timing attacks on implementations of Diffie-Hellman, RSA, DSS, and other systems. In: Proceedings of CRYPTO’96, volume 1109 of LNCS, pp. 104–113, Springer, Berlin (1996)

26.

Kocher, P.C., Jaffe, J., Jun, B.: Differential power analysis. In: Wiener, M.J. (Ed.), CRYPTO, volume 1666 of Lecture Notes in Computer Science, pp. 388–397, Springer, Berlin (1999)

27.

Kocher, P.C., Jaffe, J., Jun, B.: Differential power analysis. In: Proceedings of CRYPTO’99, volume 1666 of LNCS, pp. 388–397, Springer, Berlin (1999)

28.

Köpf, B., Basin, D.A.: An information-theoretic model for adaptive side-channel attacks. In: Peng N., Sabrina De C. V., Syverson, P.F. (Eds.), ACM Conference on Computer and Communications Security, pp. 286–296, ACM, New York (2007)

29.

Köpf, B., Dürmuth, M.: A provably secure and efficient countermeasure against timing attacks. In: CSF, pp. 324–335, IEEE Computer Society (2009)

30.

Mangard, S., Oswald, E., Popp, T.: Power analysis attacks: revealing the secrets of smart cards. Springer, Berlin (2006). ISBN 0-387-30857-1. http://www.dpabook.org/

31.

Mangard, S., Oswald, E., Standaert, F.-X.: One for all—all for one: unifying standard dpa attacks. Information Security, IET, 5(2):100–111 (2011). ISSN: 1751–8709. Digital Object Identifier. doi:10.1049/iet-ifs.2010.0096

32.

Mangard, S., Schramm, K.: Pinpointing the side-channel leakage of masked AES hardware implementations. In: CHES, volume 4249 of LNCS, pp. 76–90, Springer, Berlin (October 10–13 2006), Yokohama, Japan (2006)

33.

Mather, L., Oswald, E.: Pinpointing side-channel information leaks in web applications. J. Cryptogr. Eng. 2(3), 161–177 (2012)CrossRef

34.

Medwed, M., Standaert, F.-X., Großschädl, J., Regazzoni, F.: Fresh re-keying: security against side-channel and fault attacks for low-cost devices. In: AFRICACRYPT, volume 6055 of LNCS, pp. 279–296, Springer, (May 03–06 2010). Stellenbosch, South Africa. doi:10.1007/978-3-642-12678-9_17

35.

Moore, S., Anderson, R., Mullins, R., Taylor, G., Jacques, J.J.A.: Balanced self-checking asynchronous logic for smart card applications. J. Microprocess. Microsyst. 27(9), 421–430 (2003)CrossRef

36.

Moss, A., Oswald, E., Page, D., Tunstall, M.: Compiler assisted masking. In: Emmanuel P., Patrick S., (Eds.), CHES, volume 7428 of LNCS, pp. 58–75, Springer, Berlin (2012)

37.

Nassar, M., Bhasin, S., Danger, J.-L., Duc, G., Guilley, S.: BCDL: a high performance balanced DPL with global precharge and without early-evaluation. In: DATE’10, pp. 849–854, IEEE Computer Society, (March 8–12 2010). Dresden, Germany

38.

Popp, T., Mangard, S.: Masked dual-rail pre-charge logic: DPA-resistance without routing constraints. In: Rao, J.R., and Sunar, B. (Eds.), Cryptographic hardware and embedded systems- CHES 2005, volume 3659 of LNCS, pp. 172–186, Springer, Berlin (2005)

39.

Renauld, M., Standaert, F.-X.: Algebraic side-channel attacks. In: Feng B., Moti Y., Dongdai L., Jiwu J., (Eds.), Inscrypt, volume 6151 of Lecture Notes in Computer Science, pp. 393–410, Springer, Berlin (2009)

40.

Renauld, M., Standaert, F.-X., Nicolas, V.-C.: Algebraic side-channel attacks on the AES: why time also matters in DPA. In: CHES, volume 5747 of Lecture Notes in Computer Science, pp. 97–111. Springer, (September 6–9 2009). Lausanne, Switzerland (2009)

41.

Rivain, M., Prouff, E.: Provably secure higher-order masking of AES. In: Stefan M.,. Standaert, F.-X. (Eds.), CHES, volume 6225 of LNCS, pp. 413–427. Springer, Berlin (2010)

42.

Schramm, K., Paar, C.: Higher order masking of the AES. In: David P., (Ed.), CT-RSA, volume 3860 of LNCS, pp. 208–225, Springer, Berlin (2006)

43.

Selmane, N., Bhasin, S., Guilley, S., Graba, T., Danger, J.-L.: WDDL is protected against setup time violation attacks. In: FDTC, pp. 73–83. IEEE Computer Society, (September 6th 2009). In conjunction with CHES’09, Lausanne, Switzerland. doi:10.1109/FDTC.2009.40; Online version: http://hal.archives-ouvertes.fr/hal-00410135/en/

44.

Servant, V., Debande, N., Maghrebi, H., Bringer, J.: Study of a Novel software constant weight implementation. In: CARDIS, Lecture Notes in Computer Science. Springer, (November 2014). Paris, France (2014)

45.

Shams, M., Ebergen, J.C., Elmasry, M.I.: Modeling and comparing CMOS implementations of the C-Element. IEEE Trans. VLSI Syst. 6(4), 563–567 (1998)CrossRef

46.

Thillard, A., Prouff, E., Roche, T.: Success through confidence: evaluating the effectiveness of a side-channel attack. In: Guido Bertoni and Jean-Sébastien Coron, editors, CHES, volume 8086 of Lecture Notes in Computer Science, pp. 21–36, Springer, Berlin (2013)

47.

Tiri, K., Verbauwhede, I.: A logic level design methodology for a secure DPA resistant ASIC or FPGA implementation. In: DATE’04, pp. 246–251, IEEE Computer Society, (February 2004). Paris, France. doi:10.1109/DATE.2004.1268856

48.

Tiri, K., Verbauwhede, I.: Place and route for secure standard cell design. In: Kluwer, (Ed.), Proceedings of WCC / CARDIS, pp. 143–158, (Aug 2004). Toulouse, France

49.

Tiri, K., Verbauwhede, I.: A digital design flow for secure integrated circuits. IEEE Trans. CAD Integrat. Circuits Syst. 25(7), 1197–1208 (2006)CrossRef

50.

Zhang, Y., Juels, A., Reiter, M.K., Ristenpart, T.: Cross-VM side channels and their use to extract private keys. In: Yu, T., Danezis, G., Gligor, V.D. (Eds.), ACM Conference on Computer and Communications Security, pp. 305–316. ACM, New York (2012)

Titel: Formally proved security of assembly code against power analysis
A case study on balanced logic
verfasst von: Pablo Rauzy
Sylvain Guilley
Zakaria Najm
Publikationsdatum: 01.09.2016
Verlag: Springer Berlin Heidelberg
Erschienen in: Journal of Cryptographic Engineering / Ausgabe 3/2016
Print ISSN: 2190-8508
Elektronische ISSN: 2190-8516
DOI: https://doi.org/10.1007/s13389-015-0105-2

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Weitere Artikel der Ausgabe 3/2016

PAC learning of arbiter PUFs

Method taking into account process dispersion to detect hardware Trojan Horse by side-channel analysis

Inversion-free arithmetic on elliptic curves through isomorphisms

Physical functions: the common factor of side-channel and fault attacks?

Implementation of a leakage-resilient ElGamal key encapsulation mechanism

Faster 64-bit universal hashing using carry-less multiplications