International Association
for Cryptologic Research

This paper presents KyberSlash1 and KyberSlash2 – two timing vulnerabilities in several implementations (including the official reference code) of the Kyber Post-Quantum Key Encapsulation Mechanism, recently standardized as ML-KEM. We demonstrate the exploitability of both KyberSlash1 and KyberSlash2 on two popular platforms: the Raspberry Pi 2 (Arm Cortex-A7) and the Arm Cortex-M4 microprocessor. Kyber secret keys are reliably recovered within minutes for KyberSlash2 and a few hours for KyberSlash1. We responsibly disclosed these vulnerabilities to maintainers of various libraries and they have swiftly been patched. We present two approaches for detecting and avoiding similar vulnerabilities. First, we patch the dynamic analysis tool Valgrind to allow detection of variable-time instructions operating on secret data, and apply it to more than 1000 implementations of cryptographic primitives in SUPERCOP. We report multiple findings. Second, we propose a more rigid approach to guarantee the absence of variable-time instructions in cryptographic software using formal methods.

In this talk, we describe PQXDH, a new post-quantum key agreement protocol deployed by Signal, its formal analysis using the ProVerif and CryptoVerif protocol analysis tools, and how this analysis influenced version 2 of PQXDH. We focus on the lessons learned in this process and how formal verification can be a powerful tool in an industrial setting. The talk will be given jointly by Rolfe Schmidt and Karthikeyan Bhargavan.

Recent years have seen several landmark results in the formal verification of high-performance cryptographic libraries, leading to verified crypto code being adopted by mainstream projects like Chrome, Firefox, and Linux. Despite these successes, the secure integration and composition of verified cryptographic components within larger unverified applications remains an open challenge. The first problem is that each verification project uses its own formal specification language (F*, EasyCrypt, Coq), making its guarantees and assumptions hard for an application developer to read and understand. Second, each verified implementation presents its own low-level API that is easy to misuse. Third, when verified code is embedded within an application written in an unsafe language like C, any memory safety error in the surrounding unverified code may be used to attack the crypto code, potentially nullifying the formal guarantees of verification. In this talk, we propose a new approach that closes these gaps by integrating specification and verification within the cryptographic software development workflow. Our approach is built around HACSPEC, a new language for writing succinct, executable, formal specifications for cryptographic constructions, which aims to be equally accessible to developers, cryptographers, and verification experts. We describe translations from HACSPEC to F*, Coq, and EasyCrypt. We also present the first release of LIBCRUX, most comprehensive high- assurance cryptographic provider to date, combining verified code from HACL*, Fiat-Crypto, Vale, Jasmin, and AUCurves.

WebAuthn, forming part of FIDO2, is a W3C standard for strong authentication, which employs digital signatures to authenticate web users whilst preserving their privacy. Owned by users, WebAuthn authenticators generate attested and unlinkable public-key credentials for each web service to authenticate users. Since the loss of authenticators prevents users from accessing web services, usable recovery solutions preserving the original WebAuthn design choices and security objectives are urgently needed. We examine Yubico's recent proposal for recovering from the loss of a WebAuthn authenticator by using a secondary backup authenticator. We analyse the cryptographic core of their proposal by modelling a new primitive, called Asynchronous Remote Key Generation (ARKG), which allows some primary authenticator to generate unlinkable public keys for which the backup authenticator may later recover corresponding private keys. Both processes occur asynchronously without the need for authenticators to export or share secrets, adhering to WebAuthn's attestation requirements. We prove that Yubico's proposal achieves our ARKG security properties under the discrete logarithm and PRF-ODH assumptions in the random oracle model. To prove that recovered private keys can be used securely by other cryptographic schemes, such as digital signatures or encryption schemes, we model compositional security of ARKG using composable games by Brzuska et al. (ACM CCS 2011), extended to the case of arbitrary public-key protocols. As well as being more general, our results show that private keys generated by ARKG may be used securely to produce unforgeable signatures for challenge-response protocols, as used in WebAuthn. We conclude our analysis by discussing concrete instantiations behind Yubico's ARKG protocol, its integration with the WebAuthn standard, performance, and usability aspects.