Demonstrate use of CBMC in example of (de)compression routines

[hanno-becker]

Depends on: #44 by @potsrevennil

C code in MLKEM-C-AArch64 should be free of undefined behaviour. The C Bounded Model Checker (CBMC) is a tool which can prove absence of various classes of undefined behaviour.

This commit is a first step towards using CBMC to harden MLKEM-C-AArch64.

• Setup CBMC boilerplate using cbmc-starter-kit: All proof harnesses, scripts and Makefiles needed to run CBMC are in the cbmc/ directory. Harnesses are organized by the (main) function to which they apply, and stored in separate directories with the name of the function.
• Demonstrate the use of CBMC in the example of the (de)compression functions poly_decompress and poly_compress: Specify (in natural language, in a function contract, and in the test harness) that the coefficients in the output polynomial of this function are unsigned canonical. Hoist out scalar (de)compression routines as separate functions scalar_[de]compress_q_[16|32] for independent verification.
• Guided by CBMC, make smaller changes to poly_decompress to avoid integer truncation warnings. The previous code did not trigger undefined behaviour to my understanding (signed -> unsigned conversions are always defined), but it is arguably still better style to make truncations explicit.
• Run CBMC in CI

Note that CBMC blasts through the Barrett reduction to show that it's a genuine rounded division, which is pretty cool.

To run the poly_decompress proofs alone:

cd cbmc/proofs/poly_decompress
make

To run all CBMC tests (only poly_decompress so far, but more will hopefully be added) and print a summary,

cd cbmc/proofs
KYBER_K={2,3,4} run-cbmc-proofs.py --summarize

[hanno-becker]

@mkannwischer @potsrevennil I have issues running astyle locally. When I do

astyle $(git ls-files "*.c" "*.h") --options=.astylerc --formatted

on main, a bunch of files get modified in weird ways.

I'm using Astyle 3.4.16 (brew doesn't seem to know 3.4.10 used in the CI, but I don't think that should matter).

[cothan]

Different versions of Astyle are incompatible to each other. Like this: PQClean/PQClean#520
sometimes it makes me mad. I don't know if there is a better solution.
open-quantum-safe/liboqs#56

[hanno-becker]

Ah, thank you @cothan! I will see if I can get the specific version used by CI.

[hanno-becker]

@cothan Yes, that works, thank you 🙏

Unfortunately, astyle mangles the CBMC assertions in ugly ways.

[hanno-becker]

@cothan @potsrevennil @mkannwischer Is there a way to run the nix CI tasks locally to avoid pushing lots of revisions until the CI is appeased?

[cothan]

People use https://github.com/nektos/act run GitHub action locally.

Because we have openssf, it generates a lot of noise.

[hanno-becker]

@mkannwischer @potsrevennil @cothan

I'll stop here for the initial CBMC PR and leave further harnesses and proofs for separate PRs. I am overall quite happy how easy things are once the tool is setup, and think we will be able to roll it out more broadly for the verification of the C code in MLKEM-C-{Generic, AArch64, Embedded}.

[cothan]

Thanks @hanno-becker , it's look very good. Regards to the boilerplate from CBMC starter, I think we can reduce LoC (although it's not very important) by deleting them.
Like in https://github.com/aws/aws-encryption-sdk-c/tree/master/verification/cbmc, they remove CMBC guide text.

P/S: Do you know why the CBMC check these functions 3 times?
https://github.com/pq-code-package/mlkem-c-aarch64/actions/runs/9335413029

[hanno-becker]

Rebased after merge of #44.

[hanno-becker]

P/S: Do you know why the CBMC check these functions 3 times?

@cothan It's for KYBER_K=2,3,4