Formally verified, high-speed, constant-time cryptography

Summary

Modern computer systems, like servers, microcontrollers, or edge devices, all require cryptographic algorithms to secure their communication. These algorithms are standardized to be secure from a cryptological standpoint: they cannot be compromised by analysis of public in- and outputs. However, applying these schemes in practice requires care of additional criteria, such as the device's performance, side-channel resistance, and for the implementation to be bug-free. Direct assembly-level programming is the most common way to fulfill these properties because high-level languages (C, etc.) may introduce side-channel leakage of secrets and they don't allow for fine-grained optimization to achieve maximum performance. While performance is measurable, programming errors of popular cryptographic implementations often go unnoticed until exploited maliciously. This can be both due to typical, logical errors in the code, but increasingly due to side-channel leakage that exposes secrets via, for example, fluctuations in the power-consumption, small variations in execution time, or memory accesses. To make matters worse, optimizing compilers can introduce side-channel leakage that is not present in the source code of an algorithm.

Jasmin addresses this issue by allowing for the formal verification of cryptographic software. It comprises a toolchain for the development of verifiably correct programs: its programming language gives users fine control over the exact behavior that the compiled assembly will have, such as which registers are used to store intermediate values, and what exact machine-instruction is used for an expression. Jasmin's compiler is formally verified in Rocq (formerly Coq) to produce machine-code that preserves the semantics of a program, meaning that the compiler won't introduce unintended leakage. Further, Jasmin programs can be extracted to EasyCrypt, a proof assistant for cryptographic schemes, that can be used to show the Jasmin program is cryptographic constant-time and functionally correct. This project implements the Codes and Restricted Objects Signature Scheme (CROSS) in Jasmin and verifies it to be cryptographically constant-time.