内存安全的意义

我们对编程语言内存安全的含义给出了严格的刻画，捕捉了内存安全支持对程序状态进行局部推理这一直觉。我们通过两种方式形式化这一原则。首先，我们展示了一个小型内存安全语言如何验证非干涉性质：一个程序既不能影响状态中不可达的部分，也不受其影响。其次，我们扩展了分离逻辑——一种用于堆操作程序的证明系统——为其添加了内存安全版本的框架规则。这条新规则更强，因为它即使在程序部分存在缺陷或恶意行为时也适用，但同时也更弱，因为它要求程序状态各部分之间具有更严格的分离形式。我们还考虑了若干出于实用动机的内存安全变体及其支持的推理原则。作为我们刻画的一个应用，我们评估了一种先前提出的、用于堆分配数据内存安全的动态监控器的安全性。