# Verifying memory safety A **memory error** is a program mishandling its own storage. The program reads or writes outside an allocation, uses memory after freeing it, leaks it, or runs out of it. The class is narrow and well understood, yet it remains one of the most exploited bug classes in languages without memory safety (Szekeres et al. 2013)[^szekeres2013]. Memory errors fall into two kinds. **Safety violations** break the language's own rules and are undefined behavior, so the program may then do anything (Szekeres et al. 2013)[^szekeres2013]. **Management errors** leave behavior defined but use storage wrongly: memory or a resource is leaked, exhausted, or fragmented. The two kinds need different methods, and no single method covers both. ## Safety violations **Spatial safety** covers buffer overflow and underflow and out-of-bounds reads and writes (Nagarakatte et al. 2009)[^nagarakatte2009]. Absence is proved or inferred by [abstract interpretation](https://quality.stereobooster.com/abstract-interpretation.md), [bounded model checking](https://quality.stereobooster.com/bounded-model-checking.md), [symbolic execution](https://quality.stereobooster.com/symbolic-execution.md), and [theorem proving](https://quality.stereobooster.com/theorem-proving.md); flagged heuristically by [linters](https://quality.stereobooster.com/linters.md) on C/C++; and caught at runtime by [fuzzing](https://quality.stereobooster.com/fuzzing.md) under [ASan](https://clang.llvm.org/docs/AddressSanitizer.html). A memory-safe language rules it out too, but from **runtime bounds checks and a managed heap, not the type checker**: an ordinary [static type](https://quality.stereobooster.com/static-types.md) does not bound an array index, though a [refinement or dependent type](https://quality.stereobooster.com/refinement-and-dependent-types.md) can prove index bounds directly. **Temporal safety** covers use-after-free, double-free, use-after-return, and invalid free (Nagarakatte et al. 2010)[^nagarakatte2010]. Affine ownership closes it by construction: [linear types](https://quality.stereobooster.com/linear-types.md) reject a value used after it is moved or freed in the safe subset. Otherwise a garbage collector retires it, or [fuzzing](https://quality.stereobooster.com/fuzzing.md) under ASan finds it at runtime, with [Miri](https://github.com/rust-lang/miri) for `unsafe` Rust. **Null dereference and type confusion** are the whole of what ordinary static typing closes on its own. A null dereference is ruled out by non-nullable and option types: [static types](https://quality.stereobooster.com/static-types.md) that distinguish `T` from `T?` (Kotlin, Swift, Rust's `Option`, Haskell's `Maybe`, TypeScript under `strictNullChecks`) make a null value unrepresentable where one is not expected. Type confusion (reinterpreting bytes as the wrong type) is forbidden by a *sound* type system, which cannot express the reinterpretation; it survives only where an unsafe cast or union escapes the checker (C/C++), where [static analysis](https://quality.stereobooster.com/linters.md) and [UBSan](https://clang.llvm.org/docs/UndefinedBehaviorSanitizer.html) catch what is left. Spatial and temporal safety, by contrast, need the runtime, an analysis, or an affine type. **Uninitialized reads** are proved absent statically by [abstract interpretation](https://quality.stereobooster.com/abstract-interpretation.md) and caught at runtime by [MSan](https://clang.llvm.org/docs/MemorySanitizer.html) and [Valgrind](https://valgrind.org/) memcheck. **Data races**, two threads accessing one location without synchronization and at least one of them writing, are the concurrency case of memory safety. Rust's `Send` and `Sync` bounds close them by construction ([linear types](https://quality.stereobooster.com/linear-types.md)); otherwise [systematic concurrency testing](https://quality.stereobooster.com/systematic-concurrency-testing.md) and [TSan](https://clang.llvm.org/docs/ThreadSanitizer.html) find them. ## Management errors **Leaks** come in two shapes. The *unreachable* leak, memory whose last pointer is lost, is impossible for a resource held under an affine [linear type](https://quality.stereobooster.com/linear-types.md), and found otherwise by heap profilers ([heaptrack](https://github.com/KDE/heaptrack), [dhat](https://valgrind.org/docs/manual/dh-manual.html), [scalene](https://github.com/plasma-umass/scalene), Valgrind massif; see [profiling](https://quality.stereobooster.com/profiling.md)) and [LSan](https://clang.llvm.org/docs/LeakSanitizer.html). The *logical* leak, memory still reachable but never used again, is the one a garbage collector cannot reclaim and reachability tools miss; it shows up only as growth, caught by heap profiling and by soak testing under [load](https://quality.stereobooster.com/load-and-stress-testing.md). **Resource lifecycle**: a file, socket, or lock must be released exactly once, the same discipline as temporal safety. It is closed by construction by [linear types](https://quality.stereobooster.com/linear-types.md) or by RAII, and its error paths are exercised with [fault injection](https://quality.stereobooster.com/fault-injection.md). **Out of memory** is a *reliability* concern: the question is whether the allocation-failure path is both present and correct. Its *presence* can be forced by construction where allocation is fallible and typed as an error the caller must discharge (Zig's `error{OutOfMemory}` unions, Rust's `try_reserve` returning a `Result`), and flagged otherwise by [static analysis](https://quality.stereobooster.com/linters.md) reporting an unchecked allocation. Its *correctness* is exercised at runtime: [fault injection](https://quality.stereobooster.com/fault-injection.md) with failing allocators is the direct method, [deterministic simulation testing](https://quality.stereobooster.com/deterministic-simulation-testing.md) drives the allocator to fail on a fixed schedule, and soak and spike [load testing](https://quality.stereobooster.com/load-and-stress-testing.md) reach exhaustion under sustained or bursty demand. **Fragmentation**, where allocation fails though enough total memory is free, surfaces only over long runs, caught by soak [load testing](https://quality.stereobooster.com/load-and-stress-testing.md) and allocator instrumentation via [profiling](https://quality.stereobooster.com/profiling.md). ## Garbage collection is a trade, not a win Garbage collection is the mainstream way to get memory safety without an ownership discipline. It eliminates the temporal-safety class and the unreachable leak: a live pointer keeps memory alive, so use-after-free and double-free cannot occur in safe code. The logical leak survives, since a reachable object is never collected; non-memory resources still need explicit release, which is why `try-with-resources`, `defer`, and RAII exist alongside it; and pause times and a memory-footprint overhead disqualify it for hard-real-time and tight-memory targets. Use-after-free can also reappear through `unsafe` code, native interop, or off-heap buffers. Collection is not exclusive with substructural typing: [Pony](https://www.ponylang.io/) pairs its reference capabilities with ORCA, a concurrent collector that relies on the data-race freedom those capabilities guarantee to let each actor collect its own heap without stop-the-world pauses (Clebsch et al. 2017)[^clebsch2017]. ## Referenced by - [Linear types](https://quality.stereobooster.com/linear-types.md) · Methods - [Linters](https://quality.stereobooster.com/linters.md) · Methods - [Schema and boundary validation](https://quality.stereobooster.com/schema-and-boundary-validation.md) · Methods - [Static analysis](https://quality.stereobooster.com/static-analysis.md) · Methods ## References [^szekeres2013]: Szekeres, Laszlo, Mathias Payer, Tao Wei, and Dawn Song. 2013. "[SoK: Eternal War in Memory](https://nebelwelt.net/publications/files/13Oakland.pdf)." *2013 IEEE Symposium on Security and Privacy*, 48–62. . [^nagarakatte2009]: Nagarakatte, Santosh, Jianzhou Zhao, Milo M. K. Martin, and Steve Zdancewic. 2009. "[SoftBound: Highly Compatible and Complete Spatial Memory Safety for C](https://www.cis.upenn.edu/~stevez/papers/NZMZ09.pdf)." *Proceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '09)*, 245–58. . [^nagarakatte2010]: Nagarakatte, Santosh, Jianzhou Zhao, Milo M. K. Martin, and Steve Zdancewic. 2010. "[CETS: Compiler Enforced Temporal Safety for C](https://www.cis.upenn.edu/~stevez/papers/NZMZ10.pdf)." *Proceedings of the 2010 International Symposium on Memory Management (ISMM '10)*, 31–40. . [^clebsch2017]: Clebsch, Sylvan, Juliana Franco, Sophia Drossopoulou, Albert Mingkun Yang, Tobias Wrigstad, and Jan Vitek. 2017. "[Orca: GC and Type System Co-design for Actor Languages](https://www.ponylang.io/media/papers/orca_gc_and_type_system_co-design_for_actor_languages.pdf)." *Proceedings of the ACM on Programming Languages* 1 (OOPSLA): 72:1–28. .