Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
New Bounds for Keyed Sponges with Extendable Output: Independence Between Capacity and Message Length Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

Verifiable Side-Channel Security of Cryptographic Implementations: Constant-Time MEE-CBC

verfasst von : José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir

Erschienen in: Fast Software Encryption

Verlag: Springer Berlin Heidelberg

Einloggen

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

search-config
loading …

Abstract

We provide further evidence that implementing software countermeasures against timing attacks is a non-trivial task and requires domain-specific software development processes: we report an implementation bug in the s2n library, recently released by AWS Labs. This bug (now fixed) allowed bypassing the balancing countermeasures against timing attacks deployed in the implementation of the MAC-then-Encode-then-CBC-Encrypt (MEE-CBC) component, creating a timing side-channel similar to that exploited by Lucky 13.
Although such an attack could only be launched when the MEE-CBC component is used in isolation – Albrecht and Paterson recently confirmed in independent work that s2n’s second line of defence, once reinforced, provides adequate mitigation against current adversary capabilities – its existence serves as further evidence to the fact that conventional software validation processes are not effective in the study and validation of security properties. To solve this problem, we define a methodology for proving security of implementations in the presence of timing attackers: first, prove black-box security of an algorithmic description of a cryptographic construction; then, establish functional correctness of an implementation with respect to the algorithmic description; and finally, prove that the implementation is leakage secure.
We present a proof-of-concept application of our methodology to MEE-CBC, bringing together three different formal verification tools to produce an assembly implementation of this construction that is verifiably secure against adversaries with access to some timing leakage. Our methodology subsumes previous work connecting provable security and side-channel analysis at the implementation level, and supports the verification of a much larger case study. Our case study itself provides the first provable security validation of complex timing countermeasures deployed, for example, in OpenSSL.

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
Vorheriges Kapitel Optimizing S-Box Implementations for Several Criteria Using SAT Solvers
Nächstes Kapitel White-Box Cryptography in the Gray Box
Fußnoten
2
 
3
We note that the delay randomization countermeasure was further improved since the attacks we describe to sampling the delay between 10 s and 30 s (https://​github.​com/​awslabs/​s2n/​commit/​731e7d). Further, measures were added to prevent careless or rogue application code from forcing s2n to signal decryption failures to the adversary before that delay had passed (https://​github.​com/​awslabs/​s2n/​commit/​f8a155).
 
5
The very interesting blog post in http://​blogs.​aws.​amazon.​com/​security/​post/​TxLZP6HNAYWBQ6/​s2n-and-Lucky-13 analyses these events from the perspective of the AWS Labs development team.
 
6
Formalizing all known results for MEE-CBC would be beyond the scope of this paper, and we assume that our EasyCrypt specification of the construction inherits all the security properties that have been proved in the literature. In other words, in addition to the properties we formalize, we assume that our MEE-CBC specification satisfies the standard notions of security for authenticated encryption as proved, e.g., by Paterson, Ristenpart and Shrimpton [26].
 
8
Plaintext recovery is easier than in Lucky 13, since leakage occurs whether or not the padding string is correct.
 
9
For simplicity, the length of random inputs is assumed to be fixed by the algorithm itself.
 
10
This is only for convenience in these definitions.
 
12
In a recent development in this direction, Almeida et al. [3] describe a method, based on limited product programs, for verifying constant-time properties of LLVM code. Their method and the implementation they describe can deal with many examples that the type system from [4] cannot handle, including a less ad hoc version of our code and some of the OpenSSL code for MEE-CBC, whilst preserving a high degree of automation. In addition, their construction easily extends to situations where public outputs are needed to simulate the leakage trace.
 
13
The numbers were obtained in a virtualized Intel x86-64 Linux machine with 4 GB RAM.
 
14
This is in line with general CompCert benchmarks.
 
15
Some anonymity properties, such as untraceability, may require the cause of decryption failure to remain secret in the black-box model, in which case leakage must not reveal it either [17].
 
Literatur
1.
Albrecht, M.R., Paterson, K.G.: Lucky microseconds: a timing attack on Amazon’s s2n implementation of TLS. Cryptology ePrint Archive, report 2015/1129 (2015). http://​eprint.​iacr.​org/​
2.
AlFardan, N.J., Paterson, K.G.: Lucky thirteen: breaking the TLS and DTLS record protocols. In: IEEE Symposium on Security and Privacy SP 2013, pp. 526–540. IEEE Computer Society (2013)
3.
4.
Barthe, G., Betarte, G., Campo, J.D., Luna, C.D., Pichardie, D.: System-level non-interference for constant-time cryptography. In: Ahn, G.-J., Yung, M., Li, N. (eds.) ACM CCS 2014, pp. 1267–1279. ACM Press, November 2014
5.
Barthe, G., Crespo, J.M., Grégoire, B., Kunz, C., Lakhnech, Y., Schmidt, B., Béguelin, S.Z.: Fully automated analysis of padding-based encryption in the computational model. In: Sadeghi, A.-R., Gligor, V.D., Yung, M. (eds), ACM CCS 2013, pp. 1247–1260. ACM Press, November 2013
6.
Barthe, G., Dupressoir, F., Grégoire, B., Kunz, C., Schmidt, B., Strub, P.-Y.: EasyCrypt: a tutorial. In: Aldini, A., Lopez, J., Martinelli, J. (eds.) FOSAD 2013, pp. 146–166. Springer, Heidelberg (2014)
7.
Barthe, G., Grégoire, B., Heraud, S., Béguelin, S.Z.: Computer-aided security proofs for the working cryptographer. In: Rogaway, P. (ed.) CRYPTO 2011. LNCS, vol. 6841, pp. 71–90. Springer, Heidelberg (2011)CrossRef
8.
Barwell, G., Page, D., Stam, M.: Rogue decryption failures: reconciling AE robustness notions. In: Groth, J., et al. (eds.) IMACC 2015. LNCS, vol. 9496, pp. 94–111. Springer, Heidelberg (2015). doi:10.​1007/​978-3-319-27239-9_​6 CrossRef
9.
Bellare, M., Namprempre, C.: Authenticated encryption: relations among notions and analysis of the generic composition paradigm. In: Okamoto, T. (ed.) ASIACRYPT 2000. LNCS, vol. 1976, pp. 531–545. Springer, Heidelberg (2000)CrossRef
10.
Bellare, M., Paterson, K.G., Rogaway, P.: Security of symmetric encryption against mass surveillance. In: Garay, J.A., Gennaro, R. (eds.) CRYPTO 2014, Part I. LNCS, vol. 8616, pp. 1–19. Springer, Heidelberg (2014)CrossRef
11.
Bernstein, D., Schwabe, P.: Cryptographic software, side channels, and verification. In: COST CryptoAction WG3 Meeting, April 2015
12.
13.
Bernstein, D.J.: Cache-timing attacks on AES (2005). Author’s webpage
14.
Bernstein, D.J., Lange, T., Schwabe, P.: The security impact of a new cryptographic library. In: Hevia, A., Neven, G. (eds.) LatinCrypt 2012. LNCS, vol. 7533, pp. 159–176. Springer, Heidelberg (2012)CrossRef
15.
Boldyreva, A., Degabriele, J.P., Paterson, K.G., Stam, M.: On symmetric encryption with distinguishable decryption failures. In: Moriai, S. (ed.) FSE 2013. LNCS, vol. 8424, pp. 367–390. Springer, Heidelberg (2014)
16.
Canvel, B., Hiltgen, A.P., Vaudenay, S., Vuagnoux, M.: Password interception in a SSL/TLS channel. In: Boneh, D. (ed.) CRYPTO 2003. LNCS, vol. 2729, pp. 583–599. Springer, Heidelberg (2003)CrossRef
17.
Chothia, T., Smirnov, V.: A traceability attack against e-Passports. In: Sion, R. (ed.) FC 2010. LNCS, vol. 6052, pp. 20–34. Springer, Heidelberg (2010)CrossRef
18.
Degabriele, J.-P., Paterson, K.G., Watson, G.J.: Provable security in the real world. IEEE Secur. Priv. 9(3), 33–41 (2011)CrossRef
19.
Goguen, J.A., Meseguer, J.: Security policies and security models. In: 1982 IEEE Symposium on Security and Privacy, Oakland, CA, USA, April 26–28, pp. 11–20. IEEE Computer Society (1982)
20.
21.
Käsper, E., Schwabe, P.: Faster and timing-attack resistant AES-GCM. In: Clavier, C., Gaj, K. (eds.) CHES 2009. LNCS, vol. 5747, pp. 1–17. Springer, Heidelberg (2009)CrossRef
22.
Krawczyk, H.: The order of encryption and authentication for protecting communications (or: how secure is SSL?). In: Kilian, J. (ed.) CRYPTO 2001. LNCS, vol. 2139, pp. 310–331. Springer, Heidelberg (2001)CrossRef
23.
24.
Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: ACM Symposium on Principles of Programming Languages POPL 2006 (2006)
25.
Maurer, U., Tackmann, B.: On the soundness of Authenticate-then-Encrypt: formalizing the malleability of symmetric encryption. In: Al-Shaer, E., Keromytis, A.D., Shmatikov, V. (eds.) ACM CCS 2010, pp. 505–515. ACM Press, October 2010
26.
Paterson, K.G., Ristenpart, T., Shrimpton, T.: Tag size Does matter: attacks and proofs for the TLS record protocol. In: Lee, D.H., Wang, X. (eds.) ASIACRYPT 2011. LNCS, vol. 7073, pp. 372–389. Springer, Heidelberg (2011)CrossRef
27.
Rauzy, P., Guilley, S.: A formal proof of countermeasures against fault injection attacks on CRT-RSA. J. Crypt. Eng. 4(3), 173–185 (2014)CrossRef
28.
29.
Vaudenay, S.: Security flaws induced by CBC padding - applications to SSL, IPSEC, WTLS. In: Knudsen, L.R. (ed.) EUROCRYPT 2002. LNCS, vol. 2332, pp. 534–546. Springer, Heidelberg (2002)CrossRef
Metadaten
Titel
Verifiable Side-Channel Security of Cryptographic Implementations: Constant-Time MEE-CBC
verfasst von
José Bacelar Almeida
Manuel Barbosa
Gilles Barthe
François Dupressoir
Copyright-Jahr
2016
Verlag
Springer Berlin Heidelberg
Buch
Fast Software Encryption

Print ISBN: 978-3-662-52992-8

Electronic ISBN: 978-3-662-52993-5

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-662-52993-5_9