# The Meaning of Memory Safety

arXiv: https://arxiv.org/abs/1705.07354 · HTML: https://mlsanity.com/paper/1705.07354/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 20 May 2017.

## Built on by (most cited first, 1 of 1)

- [RFCAudit: An LLM Agent for Functional Bug Detection in Network Protocols](https://mlsanity.com/paper/2506.00714/) (2025)

## Abstract (arXiv)

We give a rigorous characterization of what it means for a programming language to be memory safe, capturing the intuition that memory safety supports local reasoning about state. We formalize this principle in two ways. First, we show how a small memory-safe language validates a noninterference property: a program can neither affect nor be affected by unreachable parts of the state. Second, we extend separation logic, a proof system for heap-manipulating programs, with a memory-safe variant of its frame rule. The new rule is stronger because it applies even when parts of the program are buggy or malicious, but also weaker because it demands a stricter form of separation between parts of the program state. We also consider a number of pragmatically motivated variations on memory safety and the reasoning principles they support. As an application of our characterization, we evaluate the security of a previously proposed dynamic monitor for memory safety of heap-allocated data.