Motivation

Timing channels are software vunelrabilities happening when execution times in a program depend on secret information. They can be exploited by an attacker to recover this secret information, such as plaintext data or secret keys.

Take for instance the following password_checker program, which compares a secret password to an attacker controlled guess:

bool password_checker(char *password, char *guess, int length) {
 for (int i = 0; i < length; ++i) {
    if (guess[i] != password[i]) return false;
 }
 return true;
}

The function iterates through each character of the guess and returns false as soon as there is a mismatch with the actual password. Let PasSw0rD be this actual password. Notice that the attempt Myguess? will fail after only one iteration of the loop, whereas the attempt Password will fail after three loop iterations. An attacker can thus measure the execution time of the function with different values of guess, in order to recover the secret value of password one character at a time.

More sophisticated attacks also exploit timing variations resulting from uses of the CPU cache. For instance, an attacker can monitor the cache to retrieve information about the memory addresses accessed by a victim.

Constant-Time Programming

To protect against these timing attacks, cryptogtaphic libraries such as OpenSSL, Libsodium, etc., use constant-time programming. It basically means that the program is designed in such a way that the control-flow and the memory accesses are independent from the secrets.

Formally, two executions of a program that only differ in their secret input must have the same control-flow and the same memory accesses.

For instance, a constant-time implementation of our password_checker function would be:

int ct_password_checker(char *password, char *guess, int length) {
    int result = 0;
    for(int i = 0; i < length, ++i) {
        result |= secret[i] ^ public[i];
    }
    return result; 
}

Challenges of Constant-Time Verification

Writing constant-time code is difficult as it usually deviates from traditional programming behaviors (for instance, it requires a lot of bitwise operations), and compiler can sometimes put a spoke in the developer’s wheel by optimizing away constant-time protections (see [1]).

Consider for instance the following constant-time selection function:

uint32_t ct_select_u32_v4(uint32_t x, uint32_t y, bool bit) {
  signed b = 0-bit;
  return (x&b) | (y&~b);
}

Compiled with clang -m32 -march=i386 -O0 (i.e. all compiler optimizations off), this function is compiled to constant-time binary code, whereas with clang -m32 -march=i386 -O3 (i.e. all compiler optimizations on), it is compiled to a conditional jump, violating constant-time. For this reason, we have to check constant-time directly on the binary.

A second challenge, is that constant-time relates two executions of a program, contrary to usual properties that guarantee the absence of bugs along one execution. Therefore, common bug-finding tools are not directly applicable to constant-time and we need tools that can efficiently reason about pairs of executions.

This is why we need efficient verification tools for constant-time operating at binary level.

Unfortunately existing techniques operate at a higher-level (C or LLVM), or do not provide necessary guarantees for bug-finding and verification, or do not scale on real-world cryptographic implementations.

Contributions

We tackle the problem of designing an efficient tool that is both able to find bugs or verify that a program is constant-time, and which operates binary level.

In summary, this paper makes the following contributions:

• We design dedicated optimizations to make the symbolic execution code analysis technique amenable for constant-time analysis at binary level. We formally prove that our analysis is correct for bug-finding and bounded-verification of constant-time.
• We propose a verification tool named Binsec/Rel and evaluate it against standard approaches on 338 cryptographic binaries, reporting a ×700 speedup compared to standard approaches.
• Using Binsec/Rel, we perform an extensive analysis of constant time at binary-level: we analyze 296 cryptographic implementations previously verified at a higher-level, and replay known bugs in 42 programs (including x86 and ARM binaries).
• We automate and extend a study on constant-time preservation by compilers. Interestingly, we discovered that gcc -O0 and backend passes of clang with -O3 -m32 -march=i386 introduce violations of constant-time that cannot be detected by LLVM verification tools, showing the importance of reasoning at binary level.

Binsec/Rel is shown to be efficient on bug-finding and bounded-verification, paving the way to systematic binary-level analysis of constant-time on cryptographic implementations, while our experiments demonstrate the importance of developing constant-time verification tools reasoning at binary-level.

Further information

• Read the paper
• Presented at the 41st IEEE Symposium on Security and Privacy
• Download the tool and benchmarks.
  
  

References

• [1] Simon L, Chisnall D, Anderson R. What you get is what you C: Controlling side effects in mainstream C compilers. (EuroS&P) 2018.