__CPROVER_w_ok has weird behaviour #5194
Comments
|
Most likely related to the issue in https://github.com/danielsn/s2n/tree/cbmc_issue_5194 on the s2n/tests/cbmc/proofs/s2n_stuffer_init proof |
|
This is tracked internally by ADA-450 |
|
This behavior is due to how bounds checking for dynamically allocated memory is implemented in cbmc. The model for The nondeterministic switch controls whether the address and size of the memory block allocated in this particular invocation of The condition To illustrate how the bounds checking works, consider the following example program: Here the assertion should fail. In the approach outlined above it indeed can, as one can choose true for This approach for bounds checking is also the reason for why there is (almost) always a trace for which If choosing false for In summary, this behavior is not a bug but due to how cbmc implements bounds checking for dynamically allocated memory. Also while the negative version |
|
Here's another example that @danielsn and I came up with: #include <stdlib.h>
int main()
{
int *x = malloc(2), *y = malloc(2);
assert(__CPROVER_r_ok(x, 3) == __CPROVER_r_ok(y, 3));
}This assertion fails. It also fails if you change the |
|
This behavior is due to how |
|
The example I mentioned today: #include <assert.h>
#include <stdlib.h>
#include <stdint.h>
#include <stdio.h>
#include <stdbool.h>
int main() {
char* foo;
__CPROVER_assume(__CPROVER_r_ok(foo, 10));
foo[20];
return 1;
} |
|
Thanks for the example. After looking further into this, it turns out that all uses of |
|
It is obvious this is how it is currently implemented, so whether you consider it a bug or not depends on whether you consider design issues. To me, this is not a useful definition in full generality. What is required here is a mechanism for getting the size of an allocated pointer. Rather than There are many useful problems that could be solved by supporting such a macro, including using the __CPROVER_r_ok in negative contexts (it is not just assumptions, it is under any negation where it will fail, so the renaming trick is not sufficient). |
|
@danpoe is this something that somebody at Diffblue could work on implementing, or give me some pointers on how to get started? This is feature is vital to us–we'll need a predicate that does the right thing when used in an assume (so So the required behavior would be: if we assume that a pointer The broader context is the function contracts work: we need to be able to say that a function parameter is backed by valid memory in a function precondition. This needs to work in the case where we're checking a function independently of its calling context; since nobody has called the function, there isn't a real object that was passed into the function, so we need to assume that the object exists in the function precondition. |
This is while we work to resolve an issue with CBMC, described at diffblue/cbmc#5194
This commit attempts to preserve the functionality of the memory checks in is_valid_IotResponseHandle until the issue in diffblue/cbmc#5194 is sorted out. This commit is needed because is_valid_IotResponseHandle uses the __CPROVER_r_ok and __CPROVER_w_ok macros, and is_valid_IotResponseHandle itself is used inside an assume statement, triggering the issue mentioned in that bug.
|
@danpoe @karkhaz @danielsn Should this one be closed now that #5247 has been merged? Though perhaps this should be done with an additional regression test that actually uses assumes. How about this one, which would not previously have worked: |
|
Two further questions:
1. Are the __CPROVER_r_ok and __CPROVER_w_ok functions fixed?
2. If so, can we continue to use them (rather than use workarounds) for assumptions?
Thanks,
Mike
From: Michael Tautschnig <[email protected]>
Reply-To: diffblue/cbmc <[email protected]>
Date: Monday, March 2, 2020 at 10:55 AM
To: diffblue/cbmc <[email protected]>
Cc: "Whalen, Mike" <[email protected]>, Comment <[email protected]>
Subject: Re: [diffblue/cbmc] __CPROVER_w_ok has weird behaviour (#5194)
@danpoe<https://github.com/danpoe> @karkhaz<https://github.com/karkhaz> @danielsn<https://github.com/danielsn> Should this one be closed now that #5247<#5247> has been merged? Though perhaps this should be done with an additional regression test that actually uses assumes. How about this one, which would not previously have worked:
#include <stdlib.h>
int main() {
unsigned length;
char* foo = malloc(length);
…__CPROVER_assume(__CPROVER_r_ok(foo, 21));
char x = foo[20];
return 1;
}
—
You are receiving this because you commented.
Reply to this email directly, view it on GitHub<#5194?email_source=notifications&email_token=ANIVFYETQAWPJRCWNWERY6DRFPP4PA5CNFSM4JPYV43KYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOENQB4MA#issuecomment-593501744>, or unsubscribe<https://github.com/notifications/unsubscribe-auth/ANIVFYEQT2SHEFSZEVY3XTTRFPP4PANCNFSM4JPYV43A>.
|
|
@tautschnig @mww-aws let's not close this quite yet. I haven't had a chance to play with #5247 yet, but @danpoe mentioned that it's only a partial fix. I haven't studied how it works, but it does work on my example with the two |
This is while we work to resolve an issue with CBMC, described at diffblue/cbmc#5194
|
I had a chat with @danpoe, writing down notes for the record:
Implementation idea: if a pointer is INVALID during symex when we reach an
Other ideas: @danpoe had proposed creating an |
This is while we work to resolve an issue with CBMC, described at diffblue/cbmc#5194
This commit attempts to preserve the functionality of the memory checks in is_valid_IotResponseHandle until the issue in diffblue/cbmc#5194 is sorted out. This commit is needed because is_valid_IotRequestHandle and is_valid_IotResponseHandle use the __CPROVER_r_ok and __CPROVER_w_ok macros, and they are used inside an assume statement, triggering the issue mentioned in that bug.
This commit attempts to preserve the functionality of the memory checks in is_valid_IotResponseHandle until the issue in diffblue/cbmc#5194 is sorted out. This commit is needed because is_valid_IotRequestHandle and is_valid_IotResponseHandle use the __CPROVER_r_ok and __CPROVER_w_ok macros, and they are used inside an assume statement, triggering the issue mentioned in that bug.
* Temporarily disable the __CPROVER_{r,w}_ok macros
This is while we work to resolve an issue with CBMC, described at
diffblue/cbmc#5194
* fix aws_array_list_back
* fix aws_array_list_front
* fix aws_array_list_get_at
* fix aws_byte_cursor_read_u8 proof
* fix CBMC proof for aws_array_list_set_at
* fix aws_byte_buf_write_from_whole_cursor CBMC proof, and minor issue in aws_byte_buf_write
* fix CBMC proof for aws_array_list_push_back
* fix byte_cursor read proofs
Co-authored-by: Daniel Schwartz-Narbonne <[email protected]>
This commit attempts to preserve the functionality of the memory checks in is_valid_IotResponseHandle until the issue in diffblue/cbmc#5194 is sorted out. This commit is needed because is_valid_IotRequestHandle and is_valid_IotResponseHandle use the __CPROVER_r_ok and __CPROVER_w_ok macros, and they are used inside an assume statement, triggering the issue mentioned in that bug.
|
If the constraints are contradictory, how come the |
|
The fact that this fails on |
|
I believe that #5247 was never intended to fix this, it's supposed to fix negative uses inside an assert rather than positive uses inside assume. But otherwise you're right: the fact that the @danielsn had tried this example because we were wondering whether the FTR The command to reproduce is cbmc --bounds-check --div-by-zero-check --float-overflow-check --nan-check --pointer-check --pointer-overflow-check --signed-overflow-check --undefined-shift-check --unsigned-overflow-check --unwind 1 --unwinding-assertions /tmp/test.cas of 8911c0a. |
|
We can distinguish between the semantics of the program, and cbmc's implementation of the semantics (which may be slightly overapproximate). According to the semantics, the above program would not be able to execute past the assume. However, due to cbmc's overapproximate behavior in that case, there are spurious executions in the encoding that can get past the assume, hence the I think there would be two possible ways of building confidence that assumptions aren't inconsistent:
|
|
Daniel,
We want a generic, foolproof way of detecting inconsistent assumptions on any program. Is there a good way to do that, currently?
Mike
From: Daniel Poetzl <[email protected]>
Reply-To: diffblue/cbmc <[email protected]>
Date: Tuesday, April 14, 2020 at 7:33 AM
To: diffblue/cbmc <[email protected]>
Cc: "Whalen, Mike" <[email protected]>, Mention <[email protected]>
Subject: Re: [diffblue/cbmc] __CPROVER_w_ok has weird behaviour (#5194)
We can distinguish between the semantics of the program, and cbmc's implementation of the semantics (which may be slightly overapproximate). According to the semantics, the above program would not be able to execute past the assume. However, due to cbmc's overapproximate behavior in that case, there are spurious executions in the encoding that can get past the assume, hence the assert(0) can fail. None of those executions however can violate the pointer checks implied by *p, thus this property does not fail.
I think there would be two possible ways of building confidence that assumptions aren't inconsistent:
1. Instead of using assert(0), check that properties relevant to the assume that one would expect to fail can still fail, e.g. assert(__CPROVER_r_ok(p, 10)) for the program above
2. Fixing the ways in which cbmc might overapproximate, enabling the use of assert(0) to detect inconsistent assumptions
—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub<#5194 (comment)>, or unsubscribe<https://github.com/notifications/unsubscribe-auth/ANIVFYDI4XHWZXK235CEL6TRMRJYFANCNFSM4JPYV43A>.
|
|
We've tried to distil this issue into a series of precise test cases that capture what we think the problem is. We would expect CBMC to report failure on each of these programs when run with // Assume a buffer is 10 ints long, then assign to the 11th element.
int main(){
int *p;
__CPROVER_assume(__CPROVER_w_ok(p, 10 * sizeof(int)));
p[10] = 0;
}// sizeof int is larger than 1 byte, so having only 1 byte readable
// and dereferencing an int ought to fail. Note that we're assuming a
// readable length of 1, not (1 * sizeof(int)).
int main()
{
int* p;
__CPROVER_assume(__CPROVER_r_ok(p,1));
*p;
}// This represents a function stub that checks its input for validity. We
// often want to ensure that a data structure has enough space to read from or
// write to, so we assert that it does.
// We expect this to fail because we assert that a data structure has more space
// than it actually does.
void fun(int *p){
__CPROVER_precondition(__CPROVER_w_ok(p, 11), "");
}
int main(){
int *p;
__CPROVER_assume(__CPROVER_w_ok(p, 10));
fun(p);
}As a variation on the above: if you write // Very similar to the above program
int main(){
int *p;
__CPROVER_assume(__CPROVER_w_ok(p, 10));
__CPROVER_assert(__CPROVER_w_ok(p, 11), "");
}As a slightly different issue to all those examples above, we would expect the following program to have no memory safety issues, but CBMC reports that the assignment to void fun(int *p){
__CPROVER_precondition(__CPROVER_w_ok(p, 10 * sizeof(int)), "");
p[9] = 0;
}
int main(){
int *p;
__CPROVER_assume(__CPROVER_w_ok(p, 10 * sizeof(int)));
fun(p);
} |
|
http://cprover.diffblue.com/cprover__builtin__headers_8h.html |
|
Thanks for those examples. To confirm our understanding, here's the next steps for us: (1) We'll produce a testsuite to determine to what extent inconsistent assumptions involving memory primitives such as (2) We'll provide a cbmc option (3) We'll provide a new primitive or library function
For the last point there are essentially three options:
We'd tend towards the last option as it would be the most safe. Would you agree with that? If possible, we'd like to avoid changing the existing semantics of |
|
I agree that failing an assertion would be the safest thing in that situation. |
|
The steps look appropriate and should help us in the future. These changes are very high priority for us (we have to report to our management about it), is it possible to have (1) and (2) implemented in one week's time? I realize that this is abrupt, but it would be very helpful to us. Having at least (1) would allow us to easily double check all of our proofs. |
|
Yes, it should be possible to provide (1) and (2) within a week. |
|
We've now created the testsuites of point (1). We checked the primitives listed by @danielsn above (except For (2), we've added a new option |
|
@danpoe which are the PRs that add those? |
|
@danpoe Thanks. I've added comments on those PRs. One thing that would really help is a document listing in one place the expected semantics of each primitive. Does such a document exist / would it be possible to create one? |
|
The behavior of the primitives (including preconditions) has been documented at http://cprover.diffblue.com/memory-primitives.html. In addition, there is now an option |
Since
y > x, it should be true that!__CPROVER_w_ok(a, y)is always false. However, if you assert this fact, you get an assertion violation.The text was updated successfully, but these errors were encountered: