High-assurance Post-Quantum Crypto with Franziskus Kiefer and Karthik Bhargavan
Jan 29, 2024
auto_awesome
Franziskus Kiefer and Karthik Bhargavan discuss high-assurance implementation of ML-KEM, transitioning from Rust to C in cryptographic code development, optimizing performance and ensuring safety in cryptographic implementations, tools for formal analysis in cryptography, advancements in post-quantum crypto, and proving TLS security using cryptographic proofs in TLS 1.3 implementation.
High assurance methods ensure correctness and security of cryptographic algorithms like MLCam.
Formal methods like F* and EasyCrypt are essential for analyzing security properties of cryptographic protocols.
Deep dives
Implementation of High Assurance Crypto Code in Pure Rust and C
The podcast episode discusses the creation of a high assurance implementation of Kyber, now called MLCam, written in pure Rust with some C components. The importance of using high assurance methods in code development is emphasized, focusing on the rigor and correctness of the implemented cryptographic algorithms.
Verification Tools and Formal Methods for Protocol Analysis
The discussion extends to the use of verification tools like F* and EasyCrypt for protocol analysis, specifically examining the design of PQ XDH protocol. The podcast highlights the significance of employing formal methods to analyze the security properties of cryptographic protocols, ensuring they meet desired security standards and resist potential vulnerabilities.
Potential for Formal Verification in Post-Quantum Cryptography Transition
The conversation moves towards the transition to post-quantum cryptography, stressing the importance of formal verification in ensuring the correctness and security of new cryptographic implementations. The necessity of adopting high assurance code, regardless of the language, and the potential benefits of an orchestrated shift from C to Rust in future cryptographic developments are also touched upon.
Future Plans for Improvements and Expansions in Verification Tools
The episode hints at upcoming projects, such as developing a vectorized version of MLCam for enhanced speed and parallelization. Additionally, it discusses the integration of technologies like ProVerif for cryptographic security proofs and F* for correctness verification into TLS implementations, showcasing the versatility and capabilities of a tool like hex for different verification needs.
We welcome Franziskus and Karthik from Cryspen to discuss their new high-assurance implementation of ML-KEM (the final form of Kyber), discussing how formal methods can both help provide correctness guarantees, security assurances, and performance wins for your crypto code!