Binsec/Rel: Efficient Constant-Time Analysis of Binary-Level Code with Relational Symbolic-Execution

Tuesday, November 5, 2019, 10:30 am - 11:30 am PDTiCal
Conference Room 1135 - ISI Marina del Rey
This event is open to the public.
ISI Cybersecurity Seminar
Lesly-Ann Daniel, CEA List and INRIA Sophia Antipolis
Video Recording:

Abstract: Timing side-channel attacks can be mitigated by adopting the constant-time programming (CT) discipline which requires the control-flow and the memory accesses to be independent from the secrets. Reasoning about CT is challenging as it is not a standard safety property but a 2-hypersafety property, relating two execution traces. Additionally, it is generally not preserved by the compiler and thus requires binary-level code analysis. Whereas writing CT code is error prone, there is a lack of automatic verification tools that can cope efficiently with these difficulties. Indeed, current tools for CT either reason at higher level, and/or sacrifice bug-finding/bounded-verification by over/under-approximating the program.

We tackle the problem of designing an efficient symbolic verification tool for CT at binary-level that leverages the full power of symbolic execution without sacrificing correct bug-finding nor bounded-verification. We design optimizations for efficient relational symbolic execution at binary-level, that analyse pairs of traces exercising the same path. We implement a prototype, Binsec/Rel, and use it to perform intensive analysis of cryptographic implementations. Using Binsec/Rel, we extend previous analyses of CT preservation by compilers. Interestingly, we discovered that gcc -O0 and backend passes of clang introduce violations of CT that were out of reach of state-of-the-art CT verification tool at LLVM or source level, demonstrating the importance of reasoning at binary-level.

Speaker Bio: Lesly-Ann Daniel is a second year PhD student at CEA List and INRIA Sophia Antipolis, working under the supervision of Sébastien Bardin and Tamara Rezk. She is interested in the application of formal methods for software security, in particular in the context of binary analysis. Currently, she works on designing automatic verification tools for security properties at binary level, with applications to constant-time cryptography. She received her master degree in 2018 from the University of Rennes (France).

ISI Host: Dr. Christophe Hauser

« Return to Upcoming Events