Explore the use of CBMC

[hanno-becker]

Relates to: #37

CBMC can be used to verify the absence of certain classes of undefined behaviour in C programs. This issue asks for an exploration of the potential use of CBMC for hardening of mlkem-c-aarch64.

Acceptance criteria:

• PR opened illustrating the use of CBMC for one or more selected C functions in mlkem-c-aarch64.
• Decision made on whether to use CBMC for wider parts of mlkem-c-aarch64.

[hanno-becker]

Potentially useful references:

• @rod-chapman's examples: https://github.com/rod-chapman/cbmc-examples/
• CBMC documentation: https://github.com/diffblue/cbmc/blob/develop/doc
• CBMC starter kit: https://github.com/model-checking/cbmc-starter-kit
• CBMC in s2n-tls: https://github.com/aws/s2n-tls/tree/main/tests/cbmc/proofs

[hanno-becker]

Started addressing this in #46

[hanno-becker]

@mkannwischer @cothan Can you give CBMC a go and make sure you can reproduce the proofs? We should all be able to write / [have CBMC] prove simple specs.

[hanno-becker]

@mkannwischer @cothan I am positive about the use of CBMC to prove absence of [some classes of] UD for the C code. I don't think it will be feasible to show functional correctness for anything beyond very simple functions.

I think we should strive to roll this out more broadly.

[hanno-becker]

Initial investigation promising, we'll try to roll out CBMC more broadly.