GaloisInc / cryptol-specs

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

Bring sampling and cryptographic functions in ML-KEM up to gold standard #146

Open marsella opened 2 weeks ago

marsella commented 2 weeks ago

This is a bunch of small clean-up tasks that arose during implementation of #143. They're all related to pseudo-randomness and sampling. See ML-KEM spec, gold standards

I also think that there is some un-aligned bit ordering in here that's caused by SHA3. The SHA-3 spec expects bits in an unusual order (MSB bytes, LSB bits) for both input and output; previously, the SHA-3 interface required the user to pass / take their input / output in that order. As of #142, there is a sleeker SHA-3 interface that interacts with MSB bit vectors. However, ML-KEM assumes bit vectors are in LSB order. There is some strange usage of SHA3 in ML-KEM: the uses of SHAKe128 and SHAKE256 convert from MSB to SHA3 bit vectors, but returns SHA3 bit vectors. ~I'm not sure whether there are additional bit order changes in some of the other bit-manipulation functions, like BytesToBits, BitsToBytes, and maybe the BitstoZ and ZtoBits~ (see comment for notes on these conversions). The gold-standard version of this spec should use the gold-standard version of SHA-3, so we will need to track down all the places where bit ordering is compensating for SHA-3 and remove them from this spec.

marsella commented 1 week ago

In our implementation, the hash functions XOF and J and PRF all use SHAKE functions and call toBytes on the input but use the output as-is. The manual transformation of the bytes to put them in the correct order happens elsewhere: