back

libmasking – Masked Gadgets in Jasmin

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.

As of now, several masking schemes have been developed [3, 4, 5] which carefully design so *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 Coq/Rocq theorem prover [7]. Finally, it has also been used to develop the cryptographic library “libjade” [8] due to its correctness and constant-time security guarantees.

Goal

The goal of this thesis is to build a small library of masked gadgets in Jasmin for developers to use when building hardened cryptographic codebases. For this, it is necessary to implement state-of-the-art gadgets like [4, 9, 10] in Jasmin. The gadgets must be implemented in a way that makes them portable to both ARM and RISC-V architectures. The library will include additional infrastructure to make the gadgets executable on embedded devices. In addition, for a fixed masking order, it should be verified that the assembly output of Jasmin retains value leakage guarantees. This can be achieved using, e.g., the scverif toolchain [3]. Correctness reasonings or proofs of the gadgets are desirable but not strictly necessary.

Requirements

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

References

Supervisors