Memory Safety: Uniqueness as Separation

Pilar Selene Linares Arévalo

doi:10.1007/978-981-95-3585-9_1

2026-01-01

PRE

Pilar Selene Linares Arévalo *

Arthur Azevedo de Amorim

DOI：10.1007/978-981-95-3585-9_1

原文链接

原文求助

摘要

En 中文

具有唯一性类型系统的编程语言可防止指针别名化，简化内存安全推理。然而，在这些语言中实现的代码通常通过外部函数接口与在缺乏同等静态安全保证的语言中实现的外部组件进行互操作。为验证组合系统中的安全更新，必须手动验证外部组件是否保持唯一性类型系统的安全不变量。特别是，近期研究显示，可以通过在高级逻辑中直接推理C代码，手动完成来自跨语言Cogent-C系统的C组件的唯一性安全义务。然而，即使在简单示例中，在不专门为直接推理堆和指针而设计的逻辑中完成唯一性安全义务（即帧条件）并不理想。分离逻辑是一种成熟的逻辑，通过将推理限定在程序修改的堆部分，便于对命令式程序进行推理。这引发了一个关键问题：我们能否使用分离逻辑来完成唯一性类型所强加的安全义务？答案是肯定的。本文表明，帧条件可以从特定的分离逻辑三元组中推断出来，并通过使用分离逻辑进行推理来完成。我们识别并验证了特定的分离逻辑三元组，这些三元组蕴含了唯一性类型系统强加的帧条件。

Keyword:

Memory Safety

Uniqueness Types

Separation Logic