Make constant_time_ops.rs and utils.rs panic-free #404
Conversation
|
I didn't get to add serialize.rs module today, hopefully will include it tomorrow. |
|
Let's go one module at a time. So just drop serialize from this PR and we have something to get in. |
mamonet
changed the title
|
Ok. Let me see where it goes wrong. |
|
Apparently, the process of lax-checking |
| #[cfg_attr(hax, hax_lib::requires( | ||
| lhs.len() == rhs.len() && | ||
| lhs.len() == SHARED_SECRET_SIZE | ||
| ))] |
There was a problem hiding this comment.
Here's my observation, with this pre-condition applied, decapsulate function in Libcrux_ml_kem.Ind_cca.fst takes 2.5 mins to lax-check. Without the pre-condition, that function takes ~1 min to lax-check. encapsulate function lax-checks right away in both cases.
There was a problem hiding this comment.
It seems F* has difficulty to handle decapsulate function, is splitting it up an option?
|
@franziskuskiefer It seems the last commit makes hax CI job green, could you review it please or assign someone who is aware of |
| let implicit_rejection_shared_secret = | ||
| Scheme::kdf::<K, CIPHERTEXT_SIZE, Hasher>(&implicit_rejection_shared_secret, ciphertext); | ||
| let shared_secret = Scheme::kdf::<K, CIPHERTEXT_SIZE, Hasher>(shared_secret, ciphertext); | ||
|
|
||
| select_shared_secret_in_constant_time( | ||
| compare_ciphertexts_select_shared_secret_in_constant_time( |
There was a problem hiding this comment.
I think this should be fine. But I wonder why F* has trouble here. @karthikbhargavan do you understand what's going on here?
|
SHA-3 C extraction should be fixed with the changes in #412. |
This is an entry PR that makes sure particular modules of ML-KEM are panic-free, it adds assumptions and pre-conditions using
hax_lib::requiresto functions that have a potential to panic to get the extracted F* filed verifiable. For now, two modules have been added and others are yet to be followed.