CBMC proof complexity/time in mldsa-native top-level signature generation

[rod-chapman]

CBMC version 6.7.1
Repository: https://github.com/pq-code-package/mldsa-native.git
Branch: cbmc-prove_signature_internal

File: mldsa/sign.c
Function: crypto_sign_signature_internal()

Link to specific source code: https://github.com/pq-code-package/mldsa-native/blob/d5c85f8c6ed0bd04b9f875ca0c3a902458d6b39f/mldsa/sign.c#L265

This function implements the top-level signature generation algorithm of mldsa-native.
It implements a "rejection sampling" loop - various things are calculated, then validity checks are applied. If these fail, then a "continue" statement goes back to the top of the loop to try again.

We have been developing a proof by commenting-out the loop body, then re-introducing the code one line at a time.

Problem: the first instance of a "continue" statement causes the proof complexity/time to blow up.

See the code at the link above. With the final un-commented line as:

    z_invalid = polyvecl_chknorm(&z, MLDSA_GAMMA1 - MLDSA_BETA);

and no more, then:

cd proofs/cbmc/crypto_sign_signature_internal
time make result

completes successfully in 56s, which is OK.

If I un-comment the next statement:

     if (z_invalid)
    {
      /* reject */
      continue;
    }

and try again, then the proof does not terminate in any reasonable time.

In the former case, the SMT2 file is about 13 Megabytes. In the latter, it grows to 21 Megabytes.

[tautschnig]

Thank you for the report, I'm taking a look.

[tautschnig]

On my Ubuntu 24.04 running on a c5.9xlarge EC2 instance the proof terminates in under 5 minutes with Z3 4.8.12 (though I acknowledge the increase in runtime up from 35 seconds). Would you mind sharing your resulting goto binary and perhaps also SMT2 file to help me reproduce problem in its entirety?

[rod-chapman]

That's with the branch and the continue statement? Interesting. We're running Z4 4.15.0, so I will see. I can also reproduce the GOTO and SMT files.

[rod-chapman]

OK... on my Mac, using CBMC 6.7.1.

First up - the code as in the repo, without the if/continue block, and using z3 4.15.0

make goto
cbmc  --smt2 --slice-formula --no-array-field-sensitivity --flush --object-bits 11    --conversion-check  --float-overflow-check --nan-check  --pointer-overflow-check    --unsigned-overflow-check --outfile z.smt2 --z3 gotos/crypto_sign_signature_internal_harness.goto
time z3 z.smt2

says "unsat" in 41s. The z.smt2 file is 13.2 megabytes.

Now let's try an earlier Z3 - this time version 4.8.17 that I happen to have installed:

time z3_4.8.17 z.smt2

returns "unsat" in 37s

So far so good. Next, I will try again un-commenting the if/continue block.

[rod-chapman]

Did you re-produce using the Makefile and exactly the options given above?
Do you see the same growth in the SMT2 file from 13 to 21 MB?

[rod-chapman]

NOW... I un-comment the if/continue block, and try again. First 2 commands the same, except I save output to znew.smt2. This time, the file is 21.8 Megabytes.

Trying the older version of Z3 first:

time z3_4.8.17 znew.smt2

says "unsat" after 9 minutes 21 seconds.

Now I'll try that again with z3 4.15.0...

[rod-chapman]

Note that there are THREE MORE if/continue blocks still to come in that function, so I am worried this is going to blow up even more when I eventually un-comment all of them...

[rod-chapman]

A friend suggested factoring out the entire loop body into a single static function that returns 0 for "all OK" and -1 for "reject". I am trying that now.

[tautschnig]

Note that there are THREE MORE if/continue blocks still to come in that function, so I am worried this is going to blow up even more when I eventually un-comment all of them...

I tried and, yes, adding yet another one of those blocks keeps Z3 going for at least 1 hour (still running). In the context of this function/this loop, do we actually need all the value bounds on array elements? As is, each such additional block will introduce another bunch of quantified expressions.

[rod-chapman]

I have factored out the entire loop body into a separate local function, and that seems to be working well for now.
We're still struggling to get predictable performance from Z3 though on all platforms. e.g. proof works fine on macOS, but fails on EC2/Linux and on our CI runners. I am investigating now.

[rod-chapman]

With refactoring and Z3 4.12.6, this proof completes OK, so closing this issue.