University of Surrey

Test tubes in the lab Research in the ATI Dance Research

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

Almeida, JB, Barbosa, M, Barthe, G and Dupressoir, FSP (2016) Verifiable Side-Channel Security of Cryptographic Implementations: Constant-Time MEE-CBC In: FSE 2016 - 23rd International Conference on Fast Software Encryption, 2016-03-20 - 2016-03-23, Bochum, Germany.

Full text not available from this repository.


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.

Item Type: Conference or Workshop Item (Conference Paper)
Subjects : Computing
Divisions : Surrey research (other units)
Authors :
Almeida, JB
Barbosa, M
Barthe, G
Date : 20 July 2016
DOI : 10.1007/978-3-662-52993-5_9
Copyright Disclaimer : © International Association for Cryptologic Research 2016
Contributors :
Peyrin, T
publisherSpringer Nature,
Depositing User : Symplectic Elements
Date Deposited : 17 May 2017 13:58
Last Modified : 23 Jan 2020 19:00

Actions (login required)

View Item View Item


Downloads per month over past year

Information about this web site

© The University of Surrey, Guildford, Surrey, GU2 7XH, United Kingdom.
+44 (0)1483 300800