# The Meaning of Memory Safety

## TL;DR

This paper rigorously defines memory safety in programming languages, formalizes its principles through noninterference and separation logic extensions, and evaluates a dynamic monitor for memory safety security.

## Contribution

It provides a formal characterization of memory safety, extending separation logic with a stronger frame rule, and analyzes practical implications for security.

## Key findings

- Memory safety supports local reasoning about state.
- A stronger, memory-safe frame rule applies even with buggy or malicious code.
- The security of a dynamic memory safety monitor is evaluated.

## Abstract

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.