CodeQL: Multiplication result converted to larger type

[robn]

I ran CodeQL, a static analysis tool, on monocypher 3.1.3 (more below). It reports "Multiple result converted to large type" on these four lines in poly1305_blocks:

const u64 x0 = s0*r0+ s1*rr3+ s2*rr2+ s3*rr1+ s4*rr0; // <= 97ffffe007fffff8
const u64 x1 = s0*r1+ s1*r0 + s2*rr3+ s3*rr2+ s4*rr1; // <= 8fffffe20ffffff6
const u64 x2 = s0*r2+ s1*r1 + s2*r0 + s3*rr3+ s4*rr2; // <= 87ffffe417fffff4
const u64 x3 = s0*r3+ s1*r2 + s2*r1 + s3*r0 + s4*rr3; // <= 7fffffe61ffffff2

Adding a pile of casts silences the warnings, and the tests still pass:

const u64 x0 = (u64)s0*r0+ (u64)s1*rr3+ (u64)s2*rr2+ (u64)s3*rr1+ (u64)s4*rr0; // <= 97ffffe007fffff8
const u64 x1 = (u64)s0*r1+ (u64)s1*r0 + (u64)s2*rr3+ (u64)s3*rr2+ (u64)s4*rr1; // <= 8fffffe20ffffff6
const u64 x2 = (u64)s0*r2+ (u64)s1*r1 + (u64)s2*r0 + (u64)s3*rr3+ (u64)s4*rr2; // <= 87ffffe417fffff4
const u64 x3 = (u64)s0*r3+ (u64)s1*r2 + (u64)s2*r1 + (u64)s3*r0 + (u64)s4*rr3; // <= 7fffffe61ffffff2

I looked at the disassembly of both and they are subtly different, but I don't know enough to know if that's meaningful.

If you think this is a false positive I would be happy to take it up with the CodeQL people myself, but I'd be interested to know if you think the version with the casts is still "safe", as that is likely the workaround I will use for my project.

As for CodeQL, I don't actually know it or use it myself; its an automated Github thing that open source projects can opt in to, and one I am contributing to (see openzfs/zfs#14249) is using it. I am mostly looking to you for guidance here.

Reproduction:

monocypher-3.1.3$ codeql database create codeql.db --language=cpp --command='bash -c "make clean && make"'
Initializing database at monocypher-3.1.3/codeql.db.
Running build command: [bash, -c, make clean && make]
[2022-12-03 11:20:10] [build-stdout] rm -rf lib/
[2022-12-03 11:20:10] [build-stdout] rm -f  *.out
[2022-12-03 11:20:10] [build-stdout] gcc -std=gnu99  -pedantic -Wall -Wextra -O3 -march=native -I src -I src/optional -fPIC -c -o lib/monocypher.o src/monocypher.c
[2022-12-03 11:20:12] [build-stdout] ar cr lib/libmonocypher.a lib/monocypher.o
[2022-12-03 11:20:12] [build-stdout] gcc -std=gnu99  -pedantic -Wall -Wextra -O3 -march=native  -shared -Wl,-soname,libmonocypher.so.3 -o lib/libmonocypher.so.3 lib/monocypher.o
[2022-12-03 11:20:12] [build-stdout] ln -sf `basename lib/libmonocypher.so.3` lib/libmonocypher.so
Finalizing database at monocypher-3.1.3/codeql.db.
Successfully created database at monocypher-3.1.3/codeql.db.

monocypher-3.1.3$ codeql database analyze --format=csv --output=codeql.csv --download -- codeql.db codeql/cpp-queries:'Likely Bugs/Arithmetic/IntMultToLong.ql'
{
  "packs" : [
    {
      "name" : "codeql/cpp-queries",
      "version" : "0.4.4",
      "library" : false,
      "result" : "IGNORED"
    }
  ],
  "packDir" : "/home/robn/.codeql/packages"
}
Running queries.
[1/1] Loaded /home/robn/.codeql/packages/codeql/cpp-queries/0.4.4/Likely Bugs/Arithmetic/IntMultToLong.qlx.
IntMultToLong.ql: [1/1 eval 6.5s] Results written to codeql/cpp-queries/Likely Bugs/Arithmetic/IntMultToLong.bqrs.
Shutting down query evaluator.
Interpreting results.

monocypher-3.1.3$ cat codeql.csv 
"Multiplication result converted to larger type","A multiplication result that is converted to a larger type can be a sign that the result can overflow the type converted from.","warning","Multiplication result may overflow 'unsigned int' before it is converted to 'unsigned long'.","/src/monocypher.c","349","51","349","56"
"Multiplication result converted to larger type","A multiplication result that is converted to a larger type can be a sign that the result can overflow the type converted from.","warning","Multiplication result may overflow 'unsigned int' before it is converted to 'unsigned long'.","/src/monocypher.c","350","51","350","56"
"Multiplication result converted to larger type","A multiplication result that is converted to a larger type can be a sign that the result can overflow the type converted from.","warning","Multiplication result may overflow 'unsigned int' before it is converted to 'unsigned long'.","/src/monocypher.c","351","51","351","56"
"Multiplication result converted to larger type","A multiplication result that is converted to a larger type can be a sign that the result can overflow the type converted from.","warning","Multiplication result may overflow 'unsigned int' before it is converted to 'unsigned long'.","/src/monocypher.c","352","51","352","56"

GCC 10.2.1, Linux x86_64.

[LoupVaillant]

OK, I think I can explain this:

• This is not a false positive (the warning is saying a true thing).
• My code is safe (there is no actual overflow).
• The difference in assembly is normal, and safe.

The source of the warning are the following 4 multiplications:

s4*rr0;
s4*rr1;
s4*rr2;
s4*rr3;

Those are pure 32-bit multiplications, because contrary to s0, s1, s2, and s3, s4 is a u32. And yes, it is then converted to u64. Still, there is no overflow because s4, rr0, rr1, rr2, and rr3 are all small enough that their multiplications never exceed 2³¹. The tool just doesn't know about that invariant, hence the warning.

To silence the warning, you don't need all your conversions, you can be content with those:

const u64 x0 = s0*r0+ s1*rr3+ s2*rr2+ s3*rr1+ (u64)s4*rr0; // <= 97ffffe007fffff8
const u64 x1 = s0*r1+ s1*r0 + s2*rr3+ s3*rr2+ (u64)s4*rr1; // <= 8fffffe20ffffff6
const u64 x2 = s0*r2+ s1*r1 + s2*r0 + s3*rr3+ (u64)s4*rr2; // <= 87ffffe417fffff4
const u64 x3 = s0*r3+ s1*r2 + s2*r1 + s3*r0 + (u64)s4*rr3; // <= 7fffffe61ffffff2

This is indeed perfectly safe. My problem here is the performance impact: I've ran the benchmarks (make speed) on my Skylake laptop, and Poly1305 go from 870MB/s down to 841MB/s, or a 3.3% loss of speed. Authenticated encryption is less affected, from 277MB/s to 274MB/s, or just over 1%. My benchmarks are very stable there, so I'm pretty sure the loss is real. (This is not a surprise: we're replacing 32-bit multiplications by a 64-bit ones, of course it is slower.)

Now there are two questions:

• Can you do the conversion to make the warning go away? Yes you can, it is safe.
• Will I upstream your fix? Probably not.

Thing is, Poly1305, and the bignum arithmetic that goes with it, is incredibly error prone no matter how you cut it. To make sure I caught all edge cases I have written a proof of correctness, and I'm even considering automating the part that shows there is no overflow.

You may note that this proof hinges on specific input invariants, that are not enforced by C's type system. So as long as CodeQL only goes by C's type system, it has to warn us. Ideally we'd be able to add annotations that make pinky promises on the range of s4, rr0, rr1, rr2, and rr3. Similar to my comments, only in a format CodeQL would understand. Maybe that would be worth reporting?

[robn]

Thank you for the analysis, and the link to the proof. I suspected it was fine, but now I have justification for whatever I decide to do!

I've reported this to the CodeQL people in github/codeql#11556, so we'll see what they want to do there. Unfortunately they don't have an inline suppression mechanism, so probably I will just leave a comment for the next person and move on. If adding the cast was free I'd use it, but I see no reason to take a performance hit to silence a warning that only a tiny number of people will see.

Thanks for your time, I very much appreciate it!

[LoupVaillant]

OK, closing this as wontfix then. Still, I believe something should be done at some point to assure reviewers and auditors that the current code is okay, despite the scary warnings from the tools. Hence #246.

[LoupVaillant]

A quick update: I have now added a little script that automatically checks the absence of integer overflow in the Poly1305 main loop (poly_block()). It's a little crude, but I'm confident it works as intended. We can verify that it does catch overflows by playing with the preconditions.

It won't help CodeQL, but this step towards actual formal verification does give some piece of mind.