Scrypt project

Scrypt is a four years ANR project.
Start date: Febrary 1st, 2019.



The goal of the project is to ensure, using formal methods, end-to-end security of cryptographic primitives going from the source code until the binary code. We aim at proving the absence of programming errors, especially those due to the difficulty of efficiently implementing complex mathematics but also at ensuring that security counter-measures are present in the binary and are provably effective at mitigating side-channel attacks which are usually not accounted for in the mathematical model. In our approach, a key role is given to security-aware certified compilation: the compiler is instrumental at both preserving and enforcing security properties which are, at best, ignored by general-purpose compilers. Well known side-channel attacks are timing attacks where the attacker observes the execution time of a cryptographic primitive. Because of hardware optimisations, e.g., memory cache, pipeline, branch prediction, observing the running time of an algorithm allows to deduce information about the program control-flow and its memory accesses. Another side-channel is the power consumption or the electromagnetic radiations that can also be observed by an attacker with physical access to a device. The leak of information due to side-channels may be sufficient for an attacker to recover a secret cryptographic key. Another obstacle to obtain secure cryptography is that, even if the source code of a cryptographic primitive implements state-of-the-art counter-measures, existing compilers may break security because of aggressive optimisations. To get the maximum control over the executed code, this forces cryptographers to directly program in assembly or manually inspect the generated code. This is both error-prone and slows down the development process.

The goal of the project is to tackle all these obstacles and develop a comprehensive toolchain dedicated to the end-to-end secure implementation of cryptographic primitives, from the source code until the binary code. The challenges are to provide a toolchain which provides formal guarantees but also meets the high efficiency requirements of cryptographic primitives. Formal guarantees will be obtained by combining formal verification of the source code of a cryptographic library with certified compilation that provides guarantees of the compiled binary code. More precisely, the project will make the following contributions: