Memory safety is traditionally characterized in terms of bad things that cannot happen. This approach is currently embraced in the literature on formal methods for memory safety. However, a general semantic principle for memory safety, that implies the negative items, remains elusive. This paper focuses on the allocator-specific aspects of memory safety, such as null-pointer dereference, use after free, double free, and heap overflow. To that extent, we propose a notion of gradual allocator independence that accurately captures the allocator-dependent aspects of memory safety. Our approach is inspired by the previously suggested connection between memory safety and noninterference, but extends that connection in a fundamentally important direction towards downgrading. We consider a low-level language with access to an allocator that provides malloc and free primitives in a flat memory model. Pointers are just integers, and as such it is trivial to write memory-unsafe programs. The basic intuition of gradual allocator independence is that of noninterference, namely that allocators must not influence program execution. This intuition is refined in two important ways that account for the allocators running out-of-memory and for programs to have pointer-to-integer casts. The key insight of the definition is to treat these extensions as forms of downgrading and give them satisfactory technical treatment using the state-of-the-art information flow machinery.

翻译：传统上，内存安全被描述为“某些坏事不会发生”。这种方法目前被形式化方法文献所采纳，用于研究内存安全。然而，一个能够包含这些负面条款的一般性内存安全语义原则仍未被揭示。本文聚焦于分配器特定的内存安全问题，如空指针解引用、释放后使用、双重释放及堆溢出。为此，我们提出了一种逐步分配器独立性的概念，该概念精确捕捉了内存安全中依赖分配器的方面。我们的方法受之前关于内存安全与非干扰之间联系的启发，但将该联系朝着下放方向进行根本性的扩展。我们考虑一种低级语言，该语言可通过扁平内存模型中的分配器访问malloc和free原语。指针仅是整数，因此编写内存不安全程序是微不足道的。逐步分配器独立性的基本直觉是非干扰性，即分配器不得影响程序执行。这一直觉通过两个重要方式得到细化，以解释分配器内存耗尽及程序中存在指针到整数转换的情况。该定义的关键见解是将这些扩展视为下放形式，并利用最先进的信息流机制为它们提供令人满意的技术处理。