SnoopStop Origin

Paste your C or Rust code. For every array access, division and integer operation you get one of two answers: either a mathematical proof that it is safe for every possible input, or the real input that triggers the bug, run and shown to you, together with a patch that has been proved to close it.

This is a trial version. For now it understands part of C: every integer type (char, short, int, long, unsigned, size_t), arrays of them, strings, loops, conditions, your own functions and library functions such as strcpy, strcat, strncpy, strlen, memcpy and memset, pointers (*p, p + i, &a[i], NULL) and malloc / calloc / free. and struct (s.x, p->x, a[i].x, p->name[i], typedef). Pointers to pointers and fields that hold pointers are not supported yet. Concurrency and authorization (new): global variables, pthread_mutex_t locks, //@ guarded_by m (data races), double locking and returning with a lock held; an authorization model declared with //@ grants X if ... / //@ requires \granted(X). The rules are the ones you declare; the tool proves they hold on every path. Thread interleavings are not enumerated one by one: code that follows the locking discipline has no race, and a path that breaks it is shown. Rust (new): integer types, slices (&[T], &mut [T]), arrays ([v; N]), subslices (&a[i..j]), .len(), for / while, if expressions, as, wrapping_*, assert! / panic!. It assumes a build with overflow checks on, so overflow counts as a panic. Structs, Vec and iterators are not supported yet, and automatic patches and "Fix everything" are C only for now. "Proved" holds only for the properties listed below and assumes this tool works correctly; it has not had an independent audit. It does not replace a security review.

//@ requires 0 <= i && i < n;      // the caller must ensure this
//@ ensures \result >= 0;            // the function guarantees this
int get(int a[], int n, int i) { ... }

//@ invariant 0 <= i && i <= n;      // true on every iteration
for (int i = 0; i < n; i++) { ... }