Download Slides (pdf)

By Prof. Manuel Barbosa, HASLab/INESC TEC & UMinho, and DCC-FCUP.

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 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.

Keywords. Cryptography and Information Security, Cryptographic protocol implementation, Timing attacks, Formal verification.

About the speaker. Manuel Barbosa is an Assistant Professor at the Department of Computer Science, Faculty of Science, University of Porto. He is a member and co-coordinator of the High Assurance Software Laboratory at INESC TEC, where he leads the Cryptography and Information Security group. He obtained a degree in Electrical and Computer Engineering from the University of Porto in 1996, an MSc degree from University Newcastle in 1997 and a PhD degree in Electric and Electronic Engineering from the University of Newcastle upon Tyne in 2000. His recent research contributions have been in the field of provable security of cryptographic algorithms and domain-specific languages for the implementation and formal verification of cryptographic software.

LOCATION AND TIME

Address:  University of Minho, Gualtar campus, Braga, Portugal.

Building. Departamento de Informatica, Building 07.

Coffee session: at 1:30PM-2PM, Sala de Estar, 4th floor.

Talks session: at 2PM-3PM, Auditório A2, 1st floor.