Shift overflow can cause incorrect verification of insecure circuits

[frereit]

When iterating all the combinations of extended probes, SILVER uses a left-shift operation on an integer to calculate the number of required iterations (and produce the selection mask):

SILVER/src/Silver.cpp

Line 282 in 0a3c85f

for (int comb = 1; comb < (1 << extended.size()); comb++) {

SILVER/src/Silver.cpp

Line 342 in 0a3c85f

for (int comb = 1; comb < (1 << extended.size()); comb++) {

SILVER/src/Silver.cpp

Line 499 in 0a3c85f

for (int comb = 1; comb < (1 << extended.size()); comb++) {

SILVER/src/Silver.cpp

Line 657 in 0a3c85f

for (int comb = 1; comb < (1 << extended.size()); comb++) {

The left-shift operation is evaluated on a literal 1, which has type int and therefore a size of 32 bit. When shifted by 31 bit to the left, the 1 ends up in the MSB of the integer, causing the value to become -2147483648 because int is a signed number type. When shifted 32 bit, the 1 is entirely shifted out of the integer, causing the value to become 0. In either case, the loop body is never executed.

When enabling the Undefined Behavior Sanitizer with -fsanitize=undefined, the overflow is detected at runtime and reported:

$ ./bin/verify --insfile repro.nl 
[     0.000] Netlist: repro.nl
[     0.005] probing.standard (d ≤ 1) -- PASS.
src/Silver.cpp:282:46: runtime error: shift exponent 32 is too large for 32-bit type 'int'
[     0.006] probing.robust   (d ≤ 1) -- PASS.
[     0.014] NI.standard      (d ≤ 1) -- PASS.
src/Silver.cpp:342:46: runtime error: shift exponent 32 is too large for 32-bit type 'int'
[     0.015] NI.robust        (d ≤ 1) -- PASS.
[     0.015] SNI.standard     (d ≤ 1) -- FAIL.
[     0.015] SNI.robust       (d ≤ 1) -- FAIL.
[     0.015] PINI.standard    (d ≤ 1) -- FAIL.
src/Silver.cpp:657:46: runtime error: shift exponent 32 is too large for 32-bit type 'int'
[     0.016] PINI.robust      (d ≤ 1) -- PASS.
[     0.016] uniformity               -- PASS.

A simple netlist to trigger the overflow is here, which was produced from the following Verilog code:

module repro (
    input [1:0] A,
    input [1:0] B,
    input [29:0] Fresh,
    input clk,
    output [1:0] Z);

    // Placing one glitch-extended probe on Z[0] gives A[0] and B[1], violating PINI.
    assign Z[0] = ^Fresh ^ A[0] ^ B[1];
    assign Z[1] = A[1] ^ B[1];
endmodule

There should be a check before these for-loops to assert that the size does not exceed 30, as explained above. In such cases, the verification should fail or be skipped with a message saying that the number of extended probes is too large.

The size of comb could also be increased to uint64_t, but then care must be taken that all other variables created based on comb are resized as well. In this case, the loop could be rewritten as

                for (uint64_t comb = 1; comb < (1ull << extended.size()); comb++) {

Note that an increase beyond a 64-bit value is probably not necessary, as even with an optimistic $10^{12}$ loop iterations per second, 63 extended probes would still require roughly half a year to verify.