.png){kind=icon}
返回
Revisiting Borrow Checking with Abstract Interpretation
.png){kind=icon}
PRE
AI
DOI：10.5381/jot.2026.25.1.a14.png)
.png){kind=icon}
原文求助.png){kind=icon}
分享.png){kind=icon}
收藏
摘要
En 中文
当代软件系统中内存安全漏洞的普遍性，使得采用内存安全编程语言变得越来越关键。在现有选项中，由Rust编程语言引入的借用检查机制通过在编译时强制实施规范化的所有权和引用语义，在安全性与性能之间提供了极具吸引力的平衡。然而，对底层框架进行进一步的正式化和完善是必要的，特别是为了增强其在存在流敏感编程模式时的精确性。在本文中，我们提出了一种新颖的重新解释，将Rust的借用检查机制视为对专用中间表示（IR）的一种抽象解释。我们的方法通过构建抽象程序轨迹来捕获变量的别名和初始化属性，从而实现对内存安全属性的细粒度、路径敏感验证。我们形式化了IR的语法和操作语义，并开发了一种健全的类型系统，该系统对引用施加基于来源的约束。通过一系列示例，我们展示了我们的框架如何成功验证那些由于保守近似而被Rust当前实现拒绝的程序。通过将借用检查与Rust的表层语法解耦，并将其嵌入到一种语言无关的IR中，我们的工作为将Rust风格的内存安全集成到更广泛的编程语言和编译器基础设施中奠定了基础。
Keyword:
Borrow Checking
Abstract Interpretation
Memory Safety
Intermediate Representation
