一句话：提出 unsafety isolation graph 与隔离类型/结构模式，将 Rust 的 interior unsafe 封装拆为自包含审计单元并做半自动验证。
Rust 社区倡导用 interior unsafe 封装 unsafe 代码，但缺乏官方指南与最佳实践，如何保证封装 soundness 仍是难题。本文研究真实 Rust 项目中 interior unsafe 的实践，提出 unsafety isolation graph 来建模 unsafe 代码的基本使用与封装关系。基于该图，作者定义四种隔离类型和九种结构模式，把图划分为若干小型自包含子图，作为审计 unsafe 封装 soundness 的单元。方法应用于四个真实 Rust 项目，结果显示能有效刻画其封装代码，并识别出三种封装模式与两个常见问题，这些问题可能使 soundness 验证复杂化或导致不健全。工作为 Rust unsafe 代码封装设计提供了半自动验证思路与实践指导。
Interior unsafe is an essential design paradigm advocated by the Rust community in system software development. However, there is little official guidance or few best practices regarding how to encapsulate unsafe code and achieve interior unsafe. To address this issue, this paper studies how interior unsafe is achieved in practice, aiming to identify best practices to guide Rust code design concerning unsafe code encapsulation. Specifically, we propose a novel unsafety isolation graph to model the essential usage and encapsulation of unsafe code. Based on the graph, we further propose four major isolation types and nine structural patterns to split a graph into several small self-contained subgraphs. These subgraphs can serve as useful audit units for examining the soundness of unsafe code encapsulation. We applied our approach to four real-world Rust projects. The experimental results demonstrate that our method is effective in characterizing their encapsulation code. Additionally, we identified three encapsulation patterns and two common issues in these projects that could complicate soundness verification or incur unsoundness issues.
DOI 原文 ·
@inproceedings{paperbot8369,
title = {Semi-Automated Verification of Interior Unsafe Code Encapsulation in Real-World Rust Systems},
author = {Zihao Rao},
booktitle = {ASE},
year = {2024},
doi = {10.1145/3691620.3695373}
}