Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Annotating and Auditing the Safety Properties of Unsafe Rust

Zihao Rao, Hongliang Tian, Xin Wang, Hui Xu

TL;DR

The paper tackles the challenge of language-level safety in Rust by introducing a domain-specific language to annotate safety properties of unsafe APIs and a novel unsafety propagation graph to model how unsafety flows through code. It then partitions large unsafe-code graphs into minimal audit units and defines audit rules and a set-based safety-tag analysis to verify consistency between declarations and actual usage. Applied to the Rust standard library, the approach achieves language-level safety coverage of 96.1% across 516 public unsafe APIs, identifies 181 APIs missing safety descriptions, and fixes 23 APIs, resulting in 49 safety tags added. The work demonstrates practical viability for guiding safety documentation in Rust and provides a foundation for future automated verification and standardization of unsafe API safety guarantees.

Abstract

Unsafe code is a critical topic in ensuring the security of system software development in Rust. It is the sole source of potential undefined behaviors, assuming the compiler is sound. To avoid the misuse of unsafe code, Rust developers should provide clear safety property annotations for unsafe APIs. However, there is limited official guidance and few best practices for annotating unsafe code. Even the current best practices for safety property annotations in the Rust standard library are ad hoc and informal. In this paper, we design a domain-specific language to describe the safety properties of unsafe APIs, which may serve as a precursor for automated verification in the future. Furthermore, to ensure that the caller of an unsafe API properly delegates the safety property required by the callee, we propose a novel unsafety propagation graph to model the usage and propagation of unsafe code. Based on this graph, we further introduce a method to partition the graph into smaller graphs, such that each graph serves as a self-contained audit unit for examining the soundness of unsafe code encapsulation and safety property annotation. We applied our approach to the Rust standard library, and the experimental results demonstrate that our method is both practical and effective. Additionally, we have fixed safety property description issues in 23 APIs.

Annotating and Auditing the Safety Properties of Unsafe Rust

TL;DR

The paper tackles the challenge of language-level safety in Rust by introducing a domain-specific language to annotate safety properties of unsafe APIs and a novel unsafety propagation graph to model how unsafety flows through code. It then partitions large unsafe-code graphs into minimal audit units and defines audit rules and a set-based safety-tag analysis to verify consistency between declarations and actual usage. Applied to the Rust standard library, the approach achieves language-level safety coverage of 96.1% across 516 public unsafe APIs, identifies 181 APIs missing safety descriptions, and fixes 23 APIs, resulting in 49 safety tags added. The work demonstrates practical viability for guiding safety documentation in Rust and provides a foundation for future automated verification and standardization of unsafe API safety guarantees.

Abstract

Unsafe code is a critical topic in ensuring the security of system software development in Rust. It is the sole source of potential undefined behaviors, assuming the compiler is sound. To avoid the misuse of unsafe code, Rust developers should provide clear safety property annotations for unsafe APIs. However, there is limited official guidance and few best practices for annotating unsafe code. Even the current best practices for safety property annotations in the Rust standard library are ad hoc and informal. In this paper, we design a domain-specific language to describe the safety properties of unsafe APIs, which may serve as a precursor for automated verification in the future. Furthermore, to ensure that the caller of an unsafe API properly delegates the safety property required by the callee, we propose a novel unsafety propagation graph to model the usage and propagation of unsafe code. Based on this graph, we further introduce a method to partition the graph into smaller graphs, such that each graph serves as a self-contained audit unit for examining the soundness of unsafe code encapsulation and safety property annotation. We applied our approach to the Rust standard library, and the experimental results demonstrate that our method is both practical and effective. Additionally, we have fixed safety property description issues in 23 APIs.
Paper Structure (54 sections, 6 equations, 4 figures, 4 tables, 1 algorithm)

This paper contains 54 sections, 6 equations, 4 figures, 4 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. The Safety Promise and Unsafety Perils of Rust
  3. Memory Safety of Rust
  4. Safe Rust
  5. Unsafe Rust
  6. Unsafe Code Encapsulation
  7. Modularized Safety
  8. Unsafety Perils
  9. Unsafe Code Annotation
  10. Safety Property Annotation Language
  11. Specification of Primitive Safety Properties
  12. Layout
  13. Pointer
  14. Content
  15. Alias
  16. ...and 39 more sections

Figures (4)

  • Figure 1: Unsafety propagation graph analysis for Listing \ref{['lst:case']}
  • Figure 2: Workflow of our auditing experiments.
  • Figure 3: Distribution of safety property tags in Rust standard library.
  • Figure 4: Distribution of structural patterns in basic units for each crate of the Rust standard library.

Theorems & Definitions (1)

  • Definition 1: Unsafety Propagation Graph (UPG)