Secret Independence for ML-KEM and ML-DSA

[karthikbhargavan]

We need to prove secret-independence for the code in libcrux-ml-kem and libcrux-ml-dsa This will require merging some ongoing work in https://github.com/hacspec/hax/tree/karthik/secret-integers

[karthikbhargavan]

We never got around to doing this.

[franziskuskiefer]

• [ ] Check C and compiled versions
• [ ] Consolidate and write up our story
• [ ] Automate checks

[karthikbhargavan]

• I have created a new branch: https://github.com/cryspen/libcrux/tree/libcrux-secret-independence/libcrux-ml-kem
• The secret independence (aka secret integers) crate is now here: https://github.com/cryspen/libcrux/tree/libcrux-secret-independence/libcrux-secret-independence
• I extended libcrux-intrinsics to support secret-independent SIMD instructions: use avx2_secret and neon_secret modules to get the secret independent versions
• This branch uses secret integers throughout libcrux-sha3, which is proved to be secret independent (yay!)
• Now all SHA-3 functions expect &[U8] and produce arrays of [U8]
• I propagated the use of SHA-3 throughout libcrux, resulting in changes to ML-KEM and ML-DSA
• For now the pattern for using SHA-3 is: first classify the input, call SHA-3, then declassify the output
• As more code becomes secret independent, we can move this classification dance higher and higher till it only applies to user inputs and outputs
• There is some bug in psq that seems unrelated and needs fixing.
• I did not propagate the changes to the old Kyber code yet.