search

xr0-org / xr0

The Xr0 Verifier for C
https://xr0.dev
Apache License 2.0
173 stars 4 forks source link

Extend Xr0 to reject uninitialised memory and use-after-free bugs. #32

Closed claude-betz closed 5 months ago

claude-betz commented 5 months ago

The high level functionality involved in getting this to work involves:

  1. “pass by pointer” functionality for the arguments to functions.
  2. Verification that “setup preconditions” defined in a particular function’s abstract are met by the state of the caller when said function is invoked.
  3. Encoding well defined memory access semantics which
    • Rejects cases of uninitialised memory accesses
    • Rejects cases of invalid pointer dereferences.
  4. Reworking our branching model to reconcile with the evaluation of “setup preconditions”.