scrypt

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.