This talk presents the Formosa Crypto toolchain for end-to-end, formally verified, crypto software, with a focus on side-channel security. Formosa tools allow specifying cryptographic security properties, such as IND-CCA, and writing high-speed implementations of cryptographic schemes, such as ML-KEM. The tools allow proving that (1) said implementations are functionally correct and secure with respect to said security properties, that (2) they are protected against (speculative) side-channel attacks, and that (3) these guarantees carry to the assembly level. The tools span interactive and automated theorem proving, static analysis, and verified compilation.
To protect crypto implementations against (speculative) side-channel attacks, Formosa provides type systems to check for (1) constant-time (including instruction-specific leakage, e.g., Intel DOIT and ARM DIT) and (2) speculative constant-time (Spectre-v1 and RSB, supporting selective SLH protections). These type systems operate at the source level, so carrying the result to the assembly level is essential. This talk discusses experiments with different strategies to achieve this goal: proving preservation as in verified compilation, checking directly at the assembly level, and others in between.