Shift overflow can cause incorrect verification of insecure circuits

[frereit]

This issue documents the same underlying bug as Chair-for-Security-Engineering/SILVER/issues/4.

In VERICA, a left-shift on an integer value is used to create the mask for the selected extended probes in analysis:

VERICA/src/analyzer/ConfigurationComposability.cpp

Line 136 in ef089f4

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

VERICA/src/analyzer/ConfigurationProbing.cpp

Line 115 in ef089f4

for (uint64_t comb = 1; comb < (uint64_t)(1 << extended_probes.size()) && this->m_independent; comb++)

Similarly to the SILVER issue, this causes the loop to be skipped when the number of extended probes exceeds 30.

There is a check in VERICA to prevent such an overflow from happening:

VERICA/src/analyzer/ConfigurationComposability.cpp

Line 124 in ef089f4

if (extended_probes.size() > 63) throw std::logic_error("[COMPOSABILITY]: More than 63 extended probes detected (overflow)!");

This is incorrect in two regards:

• Firstly, the check fails if the size is larger than 63, but this is incorrect, as explained in the SILVER issue. The overflow happens as soon as the size is larger than 30 bytes. To make the check valid, the loop condition would need to be comb < (1ull << extended_probes.size()), as is done in some other places of VERICA. This would also need to be updated in line 142, to comb & (1ull << elem).
• Secondly, the check is performed before "virtual" probes are added to the probe set in line 132. This means that the check may pass, and then the virtual probes are added, which may increase the size beyond an acceptable limit.

Additionally, it seems risky to perform the check inside an if-branch, when it could be performed instead right before the relevant for-loop to ensure it is always reached when the for-loop is reached.

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

 rc/analyzer/ConfigurationComposability.cpp:136:43: runtime error: shift exponent 32 is too large for 32-bit type 'int' %
src/analyzer/ConfigurationComposability.cpp:142:31: runtime error: shift exponent 32 is too large for 32-bit type 'int'

  TIME [s]    SERVICE          CONFIGURATION         INFO: ANALYSIS REPORT
----------------------------------------------------------------------------------------------------
     0.064    ANALYZER         PINI                  model parameters:
     0.064    ANALYZER         PINI                     glitches    : yes
     0.064    ANALYZER         PINI                     transitions : no
     0.064    ANALYZER         PINI                     couplings   : no
     0.064    ANALYZER         PINI                  verification:
     0.064    ANALYZER         PINI                     assuming : d ≤ 1
     0.064    ANALYZER         PINI                     verified : d ≤ 1
     0.064    ANALYZER         PINI                  failing probe combinations:
     0.064    ANALYZER         PINI                     total : 0
     0.064    ANALYZER         PINI                     first : - 
----------------------------------------------------------------------------------------------------
     0.065    ANALYZER         PINI                  SUCCESS

The incorrect verification can be observed with the same netlist as the SILVER issue.

To fix this issue, I think it makes most sense to "upgrade" the relevant integers to their unsigned 64-bit variants, i.e.

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

Note that this might need to be propagated to other variables as well, I did not fully investigate the code to figure out where updates are needed.

[jrichterb]

Hi,

Thanks for reporting this bug. We tried to address this issue and adjusted the variable types at the corresponding positions in the code.

Thanks,
Jan