Unwind Issue: How to make a loop inductive? #8353
Comments
|
I'm also wondering about general approach to make loops inductive(what's possible and what's not with CBMC) and if there's any documentation on that. |
|
Yes, CBMC support loop contracts to prove loops inductively: https://github.com/diffblue/cbmc/blob/develop/src/goto-instrument/contracts/doc/user/contracts-loop-invariants.md. In your example, the clause |
|
You might take a look at my "cbmc-examples" repository. This contains a selection of simple functions and their verification. All the examples use contracts (including loop invariants) to show how unbounded verification can be done with CBMC. The "arrays" subdirectory there includes function that do array initialization, assignment, and some cryptographic things like constant-time equality and conditional copy. See https://github.com/rod-chapman/cbmc-examples/
|
Thank you for the reply! In my harness I used |
After running to instrument loop contracts in will prove the harness with loop contracts. If you don't want to use dynamic frame condition checking (https://diffblue.github.io/cbmc/contracts-dev-spec-dfcc.html), instrumenting loop contracts with instead. |
|
@qinheping I'm using cbmc-starter-kit to run the proof and I added the --apply-loop-contracts flag to the makefile. I have another proof for SymCryptMd2, and I annotated loop invariants for this loop in SymCryptMd2AppendBlocks in the hope that CBMC does not need to unwind 18*48 times: but when I run make goto-instrument reported the following error: |
|
I tried to reproduced the issue with a smaller example and observed the same error. I believe the issue is caused by writing to field Where HARNESS_NAME is the name of the harness function, and should be You may also want to write loop contracts for the outer while-loop to avoid long verification time. |
|
Thank you @qinheping. So I added the --dfcc flag but the pipeline failed at the checking property step, and I saw the warning that the loops are missing assigns clauses. I followed the __CPROVER_assigns documentation and added the clauses as below but received parsing error. In md2.c Assigns clause parsing error: |
|
Loop contracts have to be specified in order. |
|
I've switch the order but the error persists. You can see from the parsing error it's referring to the line pChaint->X[k] and the assign clause precedes the other statements. |
Could you provide more detail about the failure by running the command after
Sorry I didn't notice that you write two assigns clauses for one loop. All assign targets must be specified in one assign clause, for example |
|
With the assign clauses now and --dfcc and --apply-loop-contract there is no direct failure but the report is giving me the following warning and errors: |
|
You should look at the "init_st" function in my cbmc-examples repository, which does almost exactly the same time. Using CBMC 6.0.0, if I run: the output concludes: |
|
I assed a "zero_slice()" function, which is closer to your example. Just do |
|
Thank you @rod-chapman! Using __CPROVER_object_upto() resolved the assignable error, but the first error(Check invariant after step for loop) still persists: I'm not sure what the error itself means. Is it saying that we should only check invariant after the loop has started or we should not? |
This error means the loop contracts are not inductive. Take your invariant To get a better idea of why some properties fail, you can run CBMC on the produced goto program with the flag |
|
The loop invariant needs to be "i <= cbData", since the invariant is verified just before the loop exit condition gets evaluated. It's not exactly intuitive, but see my examples that I mentioned earlier. |
|
@qinheping I was looking at the proofs for aws c common and aws encryption sdk and it looks like they didn't turn on the |
|
Also I'm getting a lot of warning: |
You can find the unbounded proof of aws c common here. However, the proofs only use old loop contracts but not dfcc.
The actual unwinding bounds are specified for each proof separately in the variable |
The third warning For the first two warnings, there are duplicate functions. @tautschnig , what is the right way to supress the duplicate symbol warning? |
I could point you at an entire crypto library that has sound, unbounded verification of type safety, but it ain't C.. :-) |
😮 @rod-chapman Could you still give me the reference? What language is it in and what's the verification tool? |
|
Here's MLKEM (aka "Kyber"): https://github.com/awslabs/LibMLKEM/tree/main/spark_ada |
|
The execution failed after switching to --smt2 😿 |
The image tells that there is some error when running SMT2 solver, but it doesn't show the actual error.I suppose it is the same issue as #8329. Could you find and share the accrual error message. Searching for |
|
@qinheping I believe it's the same issue with #8329 since I'm also using the for_all statement in a similar way: What's the best approach right now? If SAT and SMT both are not able to evaluate the for_all statment correctly is there another way to make this loop inductive? I just tried switching back to SAT and re-run the proof for SymCryptMd2 and it gave the following errors: |
|
@qinheping I followed up with the SymCrypt dev team on the destination writable errors we found in sat_not_stub_result: |
|
While we are fixing #8361, you may want to use |
|
I made the following modification to Md2:
|
|
My other question is for nested loops, if the outer loop has loop contracts, does the inner loops must also use loop contract? |
|
In the first error report, the first failure tells that the assign target In the last image, line 36-line54 are red because
Yes, the inner loops must also use loop contracts. |
|
All the errors are listed above, and somehow there's not an error associated with line 63. What are the potential causes of other errors in the report? Or are these errors that are subsequent results of the first one? |
|
So I added three more loop contracts for Md2 which I believe covers all major long loops:
|
|
For 1, the assigns clauses of a outer loop should include all assigns of the inner loops. |
|
I found that if the variable is declared inside the loop(e.g. for the outer while loop in 1, variable L is declared inside the loop), adding it to the assign clause will cause a conversion error: |
|
Hi, the assigns clause must only mention locations that are declared externally with respect to the loop, loop-locals are always considered assignable by the loop. In the example below,
Since loops are nested, the outer loop has at least all the side effect of the inner loop. int array[16] = { {0} }; // external to both loop 1 and loop 2
int i = 0; // external to loop 1 only
// loop1
while( i < 4 )
// declares targets that are assigned and external to loop 1
__CPROVER_assigns(i, __CPROVER_object_whole(array))
{
int j = 0; // local to loop 1, external to loop 2
// loop2
while (j < 4)
// declares targets that are assigned and external to loop 2
__CPROVER_assigns(j, __CPROVER_object_whole(array))
{
array[i*MAX + j];
j++;
}
i++;
}With for loops, variables declared in the for-clause are considered external to the loop: for(size_t i; i < MAX ; i++)
__CPROVER_assigns(i,...)
{
body();
}Because the size_t i;
while (i < MAX)
__CPROVER_assigns(i,...)
{
body();
i++;
}and There are other situations like this one that may seem strange : the side effect on bool find_even(int *array, size_t size, size_t *result)
__CPROVER_requires(0 < size && size < 100000 && __CPROVER_is_fresh(array, size*sizeof(int)))
__CPROVER_requires(__CPROVER_is_fresh(result, sizeof(size_t)))
__CPROVER_assigns(*result)
{
size_t i = 0;
while(i < size)
__CPROVER_assigns(i)
__CPROVER_loop_invariant(i <= size)
{
// the if-condition evaluation is part of the loop
if (array[i]%2 == 0)
{
// this is not part of the loop
*result = i;
return true;
}
i++;
}
return false;
}Hoping this helps. |
|
I don't have any quantifiers in my loop contracts and when I used the |
|
ERROR means that the SMT return with error but the error message is not included in the image. So I am not sure what went wrong in the proof with SMT2. For the unwinding error, could you try to remove the global unwinding flag |
|
For SAT, without |
|
@rod-chapman I was aware that the SMT solver had some issues with the quantifier so I tried to replicate your zero_slice example with the SAT solver by removing the forall quantifier: //playground.c
#include <stdio.h>
#include <stdint.h>
void array_wipe(size_t len, uint8_t * array)
__CPROVER_requires(__CPROVER_is_fresh(array, len))
__CPROVER_assigns(__CPROVER_object_upto(array, len))
{
__CPROVER_assume(array != NULL);
size_t i;
for (i = 0; i < len; i++)
__CPROVER_assigns(i, __CPROVER_object_upto(array, len))
__CPROVER_loop_invariant(i >= 0 && i <= len)
{
array[i] = 0; //set all array indices to 0
}
}but I got the following failures and unknowns: Also an obversation is that without the |
|
@qinheping Changes for SymCryptMd2 has been pushed, including the latest goto program and cbmc result. We have the following failures: |
|
Another issue for the make pipeline is that although I've specified |
|
I worked with the SymCrypt developer and we've made some changes to reduce the failures. For For I tried adding |
|
I think the missing part in the loop invariants is I used the following loop contracts for the outer while-loop (line 161 in __CPROVER_assigns(t, j, k, cbData, pbData, __CPROVER_object_whole(pChain))
__CPROVER_loop_invariant(cbData <= __CPROVER_loop_entry( cbData ))
__CPROVER_loop_invariant( cbData % 16 == __CPROVER_loop_entry( cbData ) % 16 && __CPROVER_same_object(pbData, __CPROVER_loop_entry(pbData)))
__CPROVER_loop_invariant( __CPROVER_POINTER_OFFSET(pbData)+ cbData == __CPROVER_POINTER_OFFSET(__CPROVER_loop_entry(pbData))+ __CPROVER_loop_entry(cbData))
__CPROVER_decreases( cbData )and run CBMC with the flag . I got the result |
|
Thank you @qinheping! I can confirm that by adding I do wonder since the |
Decreases clauses are used to prove the termination of the loops, and don't restrict the program state of the inductive step. To be precise, the loop invariant |
I guess the question is why does Is automatically adding this invariant in all cases costly? |
No. It is not hard to automatically add this predicate into loop invariants. |
I'm verifying the SymCrypt library and I'm running into unwinding failure for the SymCryptWipeAsm function, which is a simple loop that sets the buffer to 0, but because the loop iteration depends on cbData, I believe CBMC want to unwind it to the max value of cbData(under the proof constrain of 1024). I'm trying to specify invariants to make this loop inductive so that CBMC only unwinds once. I've also tried using __CPROVER_ensures with __CPROVER_forall as specified in this documentation, but I got a parsing error from goto-cc.
Harness(SymCryptWipeAsm is implemented here to overwrite the assembly version):
Related source files:
PROJECT_SOURCES += $(SRCDIR)/lib/sha256.c
PROJECT_SOURCES += $(SRCDIR)/lib/env_linuxUserMode.c
PROJECT_SOURCES += $(SRCDIR)/lib/libmain.c
PROJECT_SOURCES += $(SRCDIR)/lib/sha256Par.c
CBMC version: 5.95.1
Operating system: WSL
What behaviour did you expect: The loop become inductive and CBMC unwind once
What happened instead: unwinding failure for unwind --32
Please let me know if you need more information and I appreciate the help!
The text was updated successfully, but these errors were encountered: