Skip to content

Software Quality

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)1.

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)1. 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)2. Absence is proved or inferred by abstract interpretation, bounded model checking, symbolic execution, and theorem proving; flagged heuristically by linters on C/C++; and caught at runtime by fuzzing under ASan. 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 does not bound an array index, though a refinement or dependent type can prove index bounds directly.

Temporal safety covers use-after-free, double-free, use-after-return, and invalid free (Nagarakatte et al. 2010)3. Affine ownership closes it by construction: linear types reject a value used after it is moved or freed in the safe subset. Otherwise a garbage collector retires it, or fuzzing under ASan finds it at runtime, with 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 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 and UBSan 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 and caught at runtime by MSan and Valgrind 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); otherwise systematic concurrency testing and TSan 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, and found otherwise by heap profilers (heaptrack, dhat, scalene, Valgrind massif; see profiling) and LSan. 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.

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 or by RAII, and its error paths are exercised with fault injection.

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 reporting an unchecked allocation. Its correctness is exercised at runtime: fault injection with failing allocators is the direct method, deterministic simulation testing drives the allocator to fail on a fixed schedule, and soak and spike load testing 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 and allocator instrumentation via profiling.

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 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)4.

Referenced by

References

  1. Szekeres, Laszlo, Mathias Payer, Tao Wei, and Dawn Song. 2013. "SoK: Eternal War in Memory." 2013 IEEE Symposium on Security and Privacy, 48–62. https://doi.org/10.1109/SP.2013.13. ↩↩

  2. Nagarakatte, Santosh, Jianzhou Zhao, Milo M. K. Martin, and Steve Zdancewic. 2009. "SoftBound: Highly Compatible and Complete Spatial Memory Safety for C." Proceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '09), 245–58. https://doi.org/10.1145/1542476.1542504. ↩

  3. Nagarakatte, Santosh, Jianzhou Zhao, Milo M. K. Martin, and Steve Zdancewic. 2010. "CETS: Compiler Enforced Temporal Safety for C." Proceedings of the 2010 International Symposium on Memory Management (ISMM '10), 31–40. https://doi.org/10.1145/1806651.1806657. ↩

  4. 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." Proceedings of the ACM on Programming Languages 1 (OOPSLA): 72:1–28. https://doi.org/10.1145/3133896. ↩