Secure Compilation of Cryptographic primitives – scrypt

We use the formal methods providing the highest level of trust i.e proof assistants (Coq, Easycrypt). They are used to prove mathematical results but also prove the absence of bugs in the compiler chain. We use and develop CompCert and Jasmin which are compilers developed using this methodology.

We have studied side-channel attacks based on the execution time, in particular «cache timing attacks« and safe erasure. We have evaluated the severity of these vulnerabilities for cryptographic primitives. Based on our findings, we have proposed an evaluation methodology.

We have proposed formal models to semantically capture the notion of side-channel and proposed proof techniques to prove the preservation of these properties by compilation. Our focus has been on safe-erasure [CSF2019] and cryptographic constant-time [POPL2020]. In particular, we have formally proved that the CompCert compiler preserves the property of cryptographic constant-time.

We have developped a verification framework around Jasmin, our domain-specific language for programming cryptographic primitives. We use our own proof-assistant, Easycrypt, which program logics can be reused for Jasmin. We have developed a formal library for modular arithmetics and improved the ergonomy of Easycrypt. This allowed us to prove the correctness of various cryptographic primitives (CHACHA20, POLY1035, SHA3)
[S&P2020]. In particular, for SHA3, we have the first implementation with the following properties: efficiency, function correctness, provable security and protection against side-channel [CCS2019].

Proving that the Jasmin compiler preserves constant-time is work in progress.
Because it is based on a different semantic model, this requires to adapt the proof techniques. CompCert does not preserve the property of safe-erasure. We are therefore modifying the compiler. Before proving the preservation of security, the functional correctness proof needs to be adapted.

We keep extending Jasmin and its compiler; adding the necessary features to implement more complexe algorithmes. Ces modifications have significant consequences on the compiler (especially register allocation) and therefore on its correctness proof. One exemple of a primitive for which these extensions are mandatory is the post-quantum scheme Kyber

POPL2020] Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie and Alix Trieu. Formal verification of a constant-time preserving C compiler. PACMPL, 4(POPL). 2020.

[CCS2019] José Bacelar Almeida, Cecile Baritel-Ruet, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Alley Stoughton and Pierre-Yves Strub. Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3. CCS 2019. ACM. hal.inria.fr/hal-02404581v1

[S&P2020] José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Vincent Laporte, Tiago Oliveira, Pierre-Yves Strub. The Last Mile: High-Assurance and High-Speed Cryptographic Implementations. accepted S&P 2020. IEEE.

[CSF2019] Frédéric Besson, Alexandre Dang, Thomas P. Jensen: Information-Flow Preservation in Compiler Optimisations. CSF 2019. IEEE.

Robust cryptographic primitives are essential to ensure the security of
communication. Security is relative to an attacker model which evolves with the
technological context. Elliptic Curve Cryptography is an alternative to
traditional asymmetric cryptography primitives e.g., RSA, that is attractive for
constrained devices e.g., smartcards or smartphones. In this context, the
mathematical strength of the cryptographic algorithm is not sufficient because the
attacker has physical access to the device and can therefore eavesdrop the
computation performed by the cryptographic primitive and recover secret,
e.g. cryptographic keys, through side-channel attacks.

The goal of the project is to develop a security-aware compiler toolchain to
ensure, using formal methods, end-to-end security of cryptographic primitives
from the source code until the binary code. We aim at proving the absence of
programming errors but also at ensuring that security countermeasures are
present in the binary and are provably effective at mitigating side-channel
attacks which are usually not accounted for in the mathematical model. The
challenge is to produce compiled cryptographic code that is both provably secure
but also meet stringent efficiency requirements.

For efficiency, our approach is to design a low-level programming
language providing the right abstractions that are needed for
cryptographers to get a fined-tuned control of the hardware. For
security, our approach is grounded on machine-checked proofs which
reduce the Trusted Computing Base to the logic kernel of a
proof-assistant. Our toolchain will use the technology of certified
compilation where the compiler is both programmed and proved inside
the Coq proof-assistant. Our proof-infrastructure will include a
deductive verification framework for proving the functional
correctness of optimised cryptographic primitives but also program
transformations to enforce side-channel countermeasures. A distinctive
feature of our compiler is the guarantee that the side-channel
robustness is preserved from the source code until the binary.

The project is focused on the design and implementation of the compiler
toolchain that is a major outcome of the project. The practical evaluation is
also an objective. In term of cryptographic primitives, we target
Elliptic Curve Cryptography (ECC) which is challenging to get fast and correct
due to both the substantial mathematical background that is involved and the
low-level implementation details. An expected outcome of the project is a
formally verified ECC library competitive w.r.t. unverified state-of-the-art
implementations. In terms of side-channels, we will focus on timing and
power-analysis attacks by enforcing and improving established countermeasures
such as masking and the constant-time programming discipline.

Best practices encourage to directly program cryptographic primitives
in assembly or manually inspect the generated code. This is both
error-prone and slows down the development process. Moreover, this is
no way for a third-party to be sure that the code is secure. Our
compiler-based technology automatically ensures the security of
compiled cryptographic primitives but also provides, by construction,
verifiable security. This is especially important for Open Source
cryptographic libraries.