Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Failure to check that input pointers are disjoint from globals #642

Closed
brianhuffman opened this issue Jan 28, 2020 · 2 comments · Fixed by #752
Closed

Failure to check that input pointers are disjoint from globals #642

brianhuffman opened this issue Jan 28, 2020 · 2 comments · Fixed by #752
Assignees
Labels
bug crucible/llvm Related to crucible-llvm verification unsoundness
Milestone

Comments

@brianhuffman
Copy link
Contributor

Here's another one. This is kind of the dual to #641, but it's about checking input pointers instead of checking output pointers. Here's the C code:

#include <stdlib.h>

int glob;

int foo (int *x) {
	return (x == &glob);
}

int bar () {
	return foo(&glob);
}

and here's the saw-script, which proves that bar always returns 0, and always returns 1:

bc <- llvm_load_module "isglob.bc";

let i32 = llvm_int 32;

foo_ov <-
  crucible_llvm_verify bc "foo" [] false
    do {
      crucible_alloc_global "glob";
      x <- crucible_alloc i32;
      crucible_execute_func [x];
      crucible_return (crucible_term {{ 0 : [32] }});
    }
    z3;

bar_ov0 <-
  crucible_llvm_verify bc "bar" [foo_ov] false
    do {
      crucible_alloc_global "glob";
      crucible_execute_func [];
      crucible_return (crucible_term {{ 0 : [32] }});
    }
    z3;

bar_ov1 <-
  crucible_llvm_verify bc "bar" [] false
    do {
      crucible_alloc_global "glob";
      crucible_execute_func [];
      crucible_return (crucible_term {{ 1 : [32] }});
    }
    z3;

To preserve soundness, the disjointness check that we do to ensure that input pointers are disjoint from each other should also check that input pointers are disjoint from globals.

@brianhuffman brianhuffman added bug crucible/llvm Related to crucible-llvm verification unsoundness labels Jan 28, 2020
@brianhuffman
Copy link
Contributor Author

We should similarly enforce that input pointers declared in this way are non-NULL. A similar program that compared an input pointer with NULL instead of the address of a global would also cause a soundness problem, except that we are saved by the memory invalidation pass: we get an error message "Invalidation of unallocated or immutable region" during symbolic simulation. Anyway, we should be detecting this problem earlier; the memory invalidation pass should never be expected to fail.

@langston-barrett langston-barrett self-assigned this Feb 11, 2020
@atomb atomb added this to the 0.6 milestone Apr 3, 2020
@brianhuffman
Copy link
Contributor Author

As of revision 8610ae9, we check validity of all input pointers, which (among other things) ensures that they are non-NULL.

To check that input pointers are disjoint from globals, I think we just need to extend function enforceDisjointness in module SAWScript.Crucible.LLVM.Override to include allocated globals (csGlobalAllocs) instead of just ordinary ones (csAllocs).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug crucible/llvm Related to crucible-llvm verification unsoundness
Projects
None yet
Development

Successfully merging a pull request may close this issue.

3 participants