back

High Assurance Masking Compilation

Bachelor Thesis

Motivation

Power leakage attacks [0] 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 so-called 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, libmasking [8] introduced a library of masked gadgets written in Jasmin, providing formal correctness and security guarantees for the generated assembly. However, libmasking currently provides only individual gadgets, there is no automated way to compose them into a full masked algorithm. Doing so manually requires expert knowledge, naively replacing operations with their masked counterparts does not preserve security, as the composition of gadgets can introduce new leakage. Furthermore, device-specific leakage effects such as register transitions require additional optimization strategies when composing gadgets [3]. Barthe et al. demonstrate that exploiting such composition optimizations can reduce overhead by up to 64% for the PRESENT S-Box [3], highlighting both the importance and the difficulty of correct gadget composition.

Goal

The goal of this thesis is to build a frontend for libmasking that automatically compiles an unprotected algorithm into a masked implementation using libmasking's verified gadgets. For this, existing state-of-the-art masking compilers will be surveyed and the most suitable one will be selected as the basis for refresh insertion and gadget composition. The masked circuit produced by this compiler will then serve as input for pattern matching that maps circuit operations to optimized libmasking gadget calls, following composition optimization strategies as demonstrated in [3]. The resulting pipeline should preserve the security guarantees of libmasking at each compilation stage, and this preservation should be argued formally where possible. The pipeline will be evaluated on a concrete cryptographic primitive such as KECCAK-f[1600] or the PRESENT S-Box.

Requirements

  • Very good programming skills in C/C++
  • Some familiarity with programming on embedded devices
  • Basic knowledge of cryptography
  • High motivation + ability to work independently
  • Knowledge of the English language, Git, LaTeX, etc.

References

Supervisors

Core data