The Meaning of Memory Safety
This work provides a foundational formalization for memory safety, aiding in secure programming language design and verification, though it is incremental in extending existing proof systems.
The paper tackles the problem of rigorously defining memory safety in programming languages, showing that it enables local reasoning about state through a noninterference property and an enhanced separation logic rule, and applies this to evaluate a dynamic monitor's security.
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.