The Meaning of Memory Safety
share
We propose 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 different ways. First, we show how a small memory-safe imperative language validates a noninterference property: parts of the state that are not reachable from a given part of the program can neither affect nor be affected by its execution. Second, we show how to take advantage of memory safety to extend separation logic, a framework for reasoning about heap-manipulating programs, with a variant of its frame rule. Our new rule is stronger because it applies even when parts of the program are buggy or malicious, but also weaker because it requires a stricter form of separation between parts of the program state. We also consider a number of pragmatically motivated variations of 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.
READ FULL TEXT