back

Leakage Preservation in a Minimalistic Model Compiler

Bachelor Thesis

Motivation

Power leakage attacks [1] allow to extract secret values by observing the power consumption while executing a program. In cryptographic implementations, they can be exploited to learn secret keys and other secret values whose confidentiality needs to be protected. Masking [2] has proven to be a successful measure for hardening cryptographic implementations against value leakage attacks by performing computation on secret-shared values.

Several masking schemes have been developed [3, 4, 5] which carefully design gadgets for basic operations, such as secure addition and secure multiplication. However, these gadgets are typically developed directly in assembly. This is because the most common compilers like GCC and LLVM perform transformations that can jeopardize leakage guarantees, even when disabling optimizations [6]. While developing in assembly gives us clear guarantees about the security of a given code, it is clearly undesirable and does not scale well.

Jasmin [1] is a formally verified compiler framework for high-performance cryptographic implementations. It offers a low-level assembly-like programming language which can be compiled to different targets, like ARM, RISC-V, and x86. Furthermore, the Jasmin compiler performs very little optimizations and already offers proofs of memory-safety and constant-time security using the Rocq theorem prover [7]. Recently, Arranz Olmos et al. [8] showed how to prove preservation of constant-time under speculation to ensure that programs are protected against Spectre-v1 attacks. However, the existing proofs of security preservation do not suffice when considering power leakage attacks. Power leakage attacks have different leakage behavior than timing attacks, thus we need to reason about them differently.

Goal

The goal of this thesis is to prove for very simple compiler passes that they preserve power side channel leakage behavior of a source program throughout compilation. The proofs should be written in Rocq using a similar modeling of programs and compiler passes as in [8] .

Requirements

  • Some familiarity with Rocq or similar theorem provers
  • Basic knowledge of cryptography
  • High motivation + ability to work independently
  • Knowledge of the English language, Git, LaTeX, etc.

References

Supervisors