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 provides adequate mitigation - its existence shows that conventional software validation processes are not being effective in this domain. 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.
Category / Keywords: implementation / TLS, MEE-CBC, Timing attacks, Side-channel attacks, Countermeasures, Formal Verification Date: received 30 Dec 2015 Contact author: mbb at dcc fc up pt Available format(s): PDF | BibTeX Citation Version: 20151231:164806 (All versions of this report) Short URL: ia.cr/2015/1241 Discussion forum: Show discussion | Start new discussion