search

GaloisInc / cryptol-specs

A central repository for specifications of cryptographic algorithms in Cryptol
BSD 3-Clause "New" or "Revised" License
30 stars 6 forks source link

Update MLKEM for FIPS 203 FINAL #116

Closed rod-chapman closed 1 week ago

rod-chapman commented 4 weeks ago

Final issue of FIPS 203 was made public on 13th August 2024. There are functional changes.

This issue to track updates to Cryptol model, test cases, and so on.

kiniry commented 3 weeks ago

Wooo!

rod-chapman commented 2 weeks ago

I have this updated on a branch of my fork. Testing against the new KATs now. I will open a PR as soon as possible.

rod-chapman commented 2 weeks ago

FIPS 203 FINAL has a group of new input-data validation functions that are required. I have them done in SPARK. Would anyone like to have a crack at them in Cryptol?

mccleeary-galois commented 2 weeks ago

FIPS 203 FINAL has a group of new input-data validation functions that are required. I have them done in SPARK. Would anyone like to have a crack at them in Cryptol?

We have a need to train up some folks in Cryptol so this might be a good issue for them to take a crack at. @marsella

rod-chapman commented 2 weeks ago

The SPARK implementations start here: https://github.com/awslabs/LibMLKEM/blob/1bec368e14ecd79625a18b8b787cfe2f595814f0/spark_ada/src/mlkem.adb#L1951

It should be too hard to turn those back into Cryptol...

rod-chapman commented 1 week ago

OK - KATs look good. I have opened: https://github.com/GaloisInc/cryptol-specs/pull/131

rod-chapman commented 1 week ago

We still need those new input validation functions though.