TLDR Tech / InfoSec
A Blueprint for Formal Verification of Apple corecrypto
Apple has outlined its approach to formally verifying corecrypto for its post-quantum cryptography implementations, ML-KEM and ML-DSA. The implementation was developed in portable C, with select subroutines optimized using ARM64 assembly. To achieve formal verification, Apple translated their C implementation into Cryptol and utilized SAW to verify its equivalence with the model. The Cryptol model was then translated into Isabelle, along with the FIPS specification, to confirm their identical nature. Finally, the assembly-optimized subroutines were also translated into Isabelle and verified to be functionally equivalent to the C subroutines they replace, ensuring a high level of assurance for their cryptographic foundations.
Read the full story