Open rod-chapman opened 3 months ago
Command line is:
make TARGET=constant_time_equals_strict
I tried a simpler version without loops.
#include <stdbool.h>
#include <stddef.h>
#include <stdint.h>
#define C 8
bool constant_time_equals_strict(
const uint8_t *const a,
const uint8_t *const b,
const uint32_t len)
{
bool arrays_differ = false;
size_t i;
arrays_differ = arrays_differ || (a[i] != b[i]);
uint8_t c = a[i] - b[i];
__CPROVER_assert(
arrays_differ !=
__CPROVER_forall {
size_t j;
(j >= 0 && j < len) ==> (a[j] == b[j])
},
"Post-loop assertion");
return !arrays_differ;
}
void main()
{
uint32_t len;
uint8_t *a = malloc(sizeof(uint8_t) * len);
uint8_t *b = malloc(sizeof(uint8_t) * len);
bool result;
__CPROVER_assume(a != NULL);
__CPROVER_assume(b != NULL);
__CPROVER_assume(len >= 1);
result = constant_time_equals_strict(a, b, len);
}
I run the program with CBMC develop
and with the following commands
goto-cc main.c
goto-instrument --dfcc main --apply-loop-contracts a.out b.out
cbmc b.out -- smt2
CBMC didn't terminate. My z3 version is 4.12.5
. I also tried to run CBMC with cvc4 and cvc5 but got
** 4 of 1380 failed (2 iterations)
VERIFICATION ERROR
without detailed error message.
I think the problem could be caused by the smt encoding for quantified expression. More investigation are needed to find the cause of error.
Many thanks for the update. Please keep digging! This is blocking my work on unbounded verification of s2n-tls.
See the latest code here: https://github.com/rod-chapman/cbmc-examples/tree/main/arrays
make TARGET=constant_time_equals_strict
now works as expected with the latest CBMC 6.0.0-alpha (built today), following your fix to make "==" work inside quantifiers.
BUT... I have added a new function constant_time_equals_total() (that calls constant_time_equals_strict).
Verification of that with make TARGET=constant_time_equals_total
does not terminate. Is this the same problem as that reported above? Or perhaps a new issue?
I observed the same issue that removing or adding a simple statement, such as uint8_t c = a[i] - b[i];
in my above example will result in CBMC not terminating from terminating. So I suppose they are the same problem.
A couple of observations:
--cvc5
instead of --smt2
) makes it terminate pretty quickly, but then CVC5 actually says "unknown" for a number of properties. I don't know how to debug this, perhaps @martin-cs can contribute some insight?--smt2
) this solves in under 10 seconds with MiniSat as back-end and under 18 seconds with CaDiCaL as back-end.This problem still affects the function constant_time_equals_total() in my examples. Can I get an update or a workaround please?
This might be the same problem as #8365
CBMC version: 6.0.0-preview (cbmc-6.0.0-alpha-400-gc320360eef) Operating system: macOS 13.6.6 (Apple Silcon)
See new code in https://github.com/rod-chapman/cbmc-examples/blob/52d6ddeb15a23ed75802b15f69611dc735b6fe78/arrays/ar.c#L179
I added a "decreases" clause to the loop. CBMC 5.95.1 terminates OK after about 10 seconds. CBMC 6.0.0-preview fails to terminate, with repeated messages, such as:
and so on.
Please fix. This is blocking progress on verification of s2n-tls.