What Sanitizers and Miri Cannot Prove

A program that passes a sanitizer run has been tested, not verified. The distinction is not pedantic: every dynamic technique in common use observes a finite set of executions and reports the violations those executions triggered. Nothing about a clean report constrains the executions that were not run. Reading the reports as a certificate is the failure mode, and it is more dangerous than not running the tools at all, because it converts an open question into a false belief.

Each tool also has a characteristic blind spot that follows from its mechanism, and the mechanism determines which bugs a clean run rules out and which it does not.

Shadow memory and the address checks

AddressSanitizer maps a shadow byte for every eight bytes of application memory, at a fixed offset from the application address, so that translating an address to its shadow is an addition and a shift. The shadow byte records how many of the eight bytes are addressable: zero for none, one to seven for a partial region, and a small set of negative values for the redzones around allocations and for memory that has been freed.

Every load and store is instrumented with a check of the corresponding shadow bytes. A hit on a redzone is a heap or stack overflow; a hit on a freed region is a use-after-free, provided the region is still in the quarantine rather than reallocated. The quarantine is the mechanism’s central parameter: freed blocks are held rather than returned to the allocator, so a use-after-free is caught instead of landing on a live object. A use that occurs after the quarantine has been drained is not caught, and the size of the quarantine decides how much history is retained.

The blind spots follow directly. A use-after-free of an object that was reallocated to the same size class may not be detected even inside the quarantine window, because the shadow now says the bytes are addressable. An overflow that stays within the same allocation (an index error inside a struct’s array member) is invisible, because the shadow covers the allocation, not the member. And uninitialised reads are entirely outside the model: the shadow says a byte is addressable, not that it holds a defined value.

The instrumentation also changes the program’s memory layout, so a bug that depends on adjacency between two allocations may not reproduce under the sanitizer, and a bug that only appears with a particular alignment may appear only under it.

Happens-before and the limits of race detection

ThreadSanitizer maintains a shadow record for each memory word holding the most recent accesses and their vector clocks, and it detects a race when two accesses to the same location are unordered by happens-before and at least one is a write. The vector clocks are updated at every synchronisation operation the tool intercepts: mutex lock and unlock, atomic operations, thread creation and join, and condition variable waits.

The first limitation is that interception is the whole basis. Synchronisation implemented in a way the tool does not recognise (a custom lock built from a futex system call, a spinlock over a relaxed atomic, a barrier built from a file descriptor) is invisible, and accesses ordered by it appear unordered. The result is a false positive, and the standard response is an annotation that tells the tool about the ordering.

The second is coverage of interleavings. A race requires a particular schedule to manifest, and the tool observes the schedules the scheduler actually produced. A race in a code path taken once in a thousand runs may never be reached. Tools that deliberately perturb scheduling exist precisely because the observed schedule is a sample, and a clean report from a single run says only that the sampled schedules were clean.

The third is that the tool reports conflicts it observed, not conflicts that are possible. A race that requires three threads and a specific order of two lock acquisitions is not visible in a two-thread test.

Uninitialised bytes and the shadow of definedness

MemorySanitizer tracks definedness rather than addressability. Its shadow records, per bit, whether the bit is derived from an initialised source, and it propagates definedness through arithmetic, copies, and calls. A branch or a system call argument that depends on an undefined bit is reported.

The precision is high, which is the tool’s advantage: it names the read that consumed the uninitialised value rather than a downstream crash. The cost is that every dependency must be instrumented. A call into a library that was not built with the sanitizer returns values the tool cannot classify, and the usual resolution is to treat them as defined, which silently removes the taint. An uninstrumented library that fills a buffer leaves the buffer’s definedness unknown, and the tool’s report depends on the interceptor it has for that function.

The mechanism also cannot see an uninitialised read whose result is discarded or masked before use. A byte that is copied into a structure and never read is not a violation, and the tool correctly stays silent, which means a structure with uninitialised padding passes a clean run.

UndefinedBehaviourSanitizer checks a list

UBSan is the most easily misunderstood, because its name suggests a category rather than an enumeration. It inserts checks for a specific set of operations: signed integer overflow, division by zero, shifts by an out-of-range amount, misaligned pointer use, null pointer dereference, out-of-bounds indexing on arrays with known bounds, invalid enum values, and a few others depending on the flag set.

Each check is a comparison and a call, and the set is chosen for cheapness rather than completeness. Several classes of undefined behaviour have no check at all: strict aliasing violations, data races, use of an invalidated pointer in the provenance sense, and reading an object whose lifetime has ended are all outside the instrumented set. A program free of UBSan reports can still be undefined.

The other property is that the checks are inserted into the optimised code, so the compiler has already applied the transformations that the undefined behaviour licensed. An operation that the optimiser deleted because it was unreachable under an assumption does not get checked, and a check that survives may fire in a situation the optimiser had already assumed away. This is why sanitizer builds are usually compiled at a low optimisation level: the checks and the assumptions interact in ways that make the report hard to attribute.

Interpretation as a different kind of evidence

Miri runs the program on an interpreter for the Rust abstract machine rather than on hardware. It models allocations with provenance, tracks initialisation per byte, enforces the aliasing model, and reports the operation that violated a rule. Because it executes the abstract machine, it can detect violations that have no runtime manifestation at all: a reference to a dead value, an out-of-bounds pointer formed but never dereferenced, a call that violates Stacked Borrows even though the generated code would have worked.

That capability is why Miri finds bugs that no native tool can, and it is also why its reports must be read as statements about the model. A program that violates Stacked Borrows is undefined under the model the compiler targets, so the report is correct even if every native run passed. A program that Miri accepts is defined under the model, subject to the model being the specification.

The limits are structural. Miri can only interpret code it can execute, so any call into a foreign function, any inline assembly block, and any operation the interpreter does not implement stops the run. Crates that wrap a C library cannot be checked end to end. Interpretation is also slow enough that only small test inputs are practical, which means the coverage is a handful of paths.

Concurrency is the sharper limit. Miri can explore some interleavings under a flag, but the state space grows with the number of threads and operations, and the exploration is bounded. A clean run under one schedule is evidence about that schedule.

Combining evidence honestly

The four tools cover different slices. AddressSanitizer covers spatial memory errors on executed paths. ThreadSanitizer covers races on the schedules observed. MemorySanitizer covers definedness where instrumentation is complete. UBSan covers an enumerated list of arithmetic and pointer faults. Miri covers the abstract-machine rules for code it can interpret.

None of them covers the others’ blind spots, and running all of them still leaves the unexecuted paths unchecked. The technique that closes part of that gap is not another sanitizer but a proof: a soundness argument for each unsafe abstraction, written down and reviewed, that establishes the invariant for all inputs rather than for the tested ones. The wrapper discipline that makes such an argument possible is treated in What Makes a Safe Wrapper Around Unsafe Code Sound, and the reason a clean optimised build is not evidence either is treated in Undefined Behaviour as a Compiler Permission.

The honest summary of a clean sanitizer run is narrow and useful: the tested inputs, on the tested schedule, in the instrumented build, did not trigger the classes of violation the tool can see. That is worth having. It is not the same as knowing the code is correct, and the difference is exactly the set of executions nobody ran.