Unverified KMAC-128 and KMAC-256 implementation

[kraemv]

Hello everyone,
I implemented KMAC-128 and KMAC-256 in Rust and would like to contribute my code to libcrux. I am not familiar with hax and F*, hence my commit does not contain a correctness proof.
I have tested my code with the wycheproof project, the test vectors and the changes to the /tests repository are included in this PR.
I made changes to sha3/src/portable.rs to implement an iterative CShake API with the correct Keccak padding. An iterative API is required to make the code no_std compatible.
Could you please share your thoughts about the length values (e.g. key_length) in hacl/kmac.rs, as they will panic for inputs larger than 2^61 bytes.

[jschneider-bensch]

Thank you!
I haven't had time for a detailed look yet, just a few comments.

[franziskuskiefer]

@kraemv do you think you could add runtime safety, i.e. that the code never panics, if you help you with the set up?

[jschneider-bensch]

In this PR to your branch, I've added a basic setup for doing runtime safety proofs. Let me know what you think!

[kraemv]

The fstar runtime safety proof now goes through.

[jschneider-bensch]

It's very nice that you can extract and typecheck this code for runtime safety without any annotations!
I came up with some ideas for refactoring the code and tried them out on this branch: https://github.com/cryspen/libcrux/tree/jonas/refactor-kmac-cshake (comparison)

• I reduced code duplication a bit using a const generic for the RATE and passing in the CSHAKE implementation as a generic as well.
• I moved the CSHAKE-specific parts out of KMAC and into a general purpose CSHAKE implementation in sha3.
• To do this I needed to add some annotations for runtime safety, but the extraction should typecheck on that branch as well.

Would you be okay with incorporating these changes here?

[kraemv]

Hi Jonas,
I like your changes to the code, they benefit readability and structure! Also, the structure is now closer to the definitions of KMAC and CSHAKE in the standard.
Do you think it is easier to proof functional correctness at some future point for a more generic code?
With the new structure, you should be able to remove CShake128It in [crates/algorithms/sha3/src/portable/cshake.rs] as it is superseded by CShake128 in [crates/algorithms/sha3/src/portable/incremental.rs].

[jschneider-bensch]

I think we have found in ML-KEM and ML-DSA as well that doing a functional correctness proof on a generic implementation can be advantageous since you only do the proof once and it should hold for all different (valid!) parameters the generic implementation can be instantiated with.

I made a few more small changes on the refactoring branch, updating changelogs and removing the obsolete code you found. I think with these also merged into your PR this looks very good to me already!
One thing we should do before merging the PR is add some more documentation around the new CSHAKE and KMAC APIs. Just let me know if you'd like to give that a shot or if not, I can do it.

[kraemv]

Well, then I am very happy to have the generic code now :)
I merged the most recent changes into this PR already. I am also very happy with the state of the code!
I would be grateful if you could do the documentation, as I am currently quite busy with another project.

[jschneider-bensch]

Okay, then I'll take care of the rest. 👍 Thanks a lot for your efforts!

[kraemv]

Thank you for your feedback on the code and the support to prove runtime safety!