Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Trace-based Approach for Code Safety Analysis

Hui Xu

TL;DR

The paper addresses undefined behavior in Rust by formalizing a trace-based safety framework that separates safe from unsafe code via explicit safety constraints. It presents a main theorem establishing that UB arises only from unsafe code and is governed by the unsafe code's safety constraints, and it derives soundness criteria for safe and unsafe functions. Extending the theory to struct, module, and crate levels, it introduces corollaries for sound function and struct encapsulation and defines an Unsafety Propagation Graph (UPG) to audit crates at scale. The work offers an actionable workflow for Rust crate auditing, enabling boundary-respecting encapsulation and practical verification of safety guarantees across code boundaries.

Abstract

Rust is a memory-safe programming language that disallows undefined behavior. Its safety guarantees have been extensively examined by the community through empirical studies, which has led to its remarkable success. However, unsafe code remains a critical concern in Rust. By reviewing the safety design of Rust and analyzing real-world Rust projects, this paper establishes a systematic framework for understanding unsafe code and undefined behavior, and summarizes the soundness criteria for Rust code. It further derives actionable guidance for achieving sound encapsulation.

A Trace-based Approach for Code Safety Analysis

TL;DR

The paper addresses undefined behavior in Rust by formalizing a trace-based safety framework that separates safe from unsafe code via explicit safety constraints. It presents a main theorem establishing that UB arises only from unsafe code and is governed by the unsafe code's safety constraints, and it derives soundness criteria for safe and unsafe functions. Extending the theory to struct, module, and crate levels, it introduces corollaries for sound function and struct encapsulation and defines an Unsafety Propagation Graph (UPG) to audit crates at scale. The work offers an actionable workflow for Rust crate auditing, enabling boundary-respecting encapsulation and practical verification of safety guarantees across code boundaries.

Abstract

Rust is a memory-safe programming language that disallows undefined behavior. Its safety guarantees have been extensively examined by the community through empirical studies, which has led to its remarkable success. However, unsafe code remains a critical concern in Rust. By reviewing the safety design of Rust and analyzing real-world Rust projects, this paper establishes a systematic framework for understanding unsafe code and undefined behavior, and summarizes the soundness criteria for Rust code. It further derives actionable guidance for achieving sound encapsulation.

Paper Structure

This paper contains 16 sections, 7 theorems, 16 equations.

Table of Contents

  1. Introduction
  2. Notations
  3. Main Theorem
  4. Soundness Criterion of Safe Code
  5. Soundness Criterion of Unsafe Code
  6. Sound Function Encapsulation
  7. Struct Soundness
  8. Soundness Criteria of Structs
  9. Sound Struct Encapsulation
  10. Considerations of Traits
  11. Module and Crate Soundness
  12. Soundness Criteria of Modules
  13. Sound Module Encapsulation
  14. Crate Soundness
  15. Application
  16. ...and 1 more sections

Key Result

Theorem 1

Let $P$ be a well-typed Rust program. Then, undefined behavior can occur in $P$ only if $P$ contains unsafe code and $P$ violates its associated safety constraints. Formally, where $UC$ denotes a piece of unsafe code (typically an unsafe function call) contained in $P$, and $SC_{UC}$ denotes the safety constraints of the unsafe code.

Theorems & Definitions (14)

  • Theorem 1: Main Theorem
  • Definition 1: Safety Promise of Rust
  • Definition 2: Soundness criterion of Safe Functions
  • Definition 3: Soundness Criterion of Unsafe Functions
  • corollary 1: Safe Function Encapsulation
  • corollary 2: Unsafe Function Encapsulation
  • corollary 3: Sound Function Encapsulation
  • Definition 4: Soundness Criteria of Structs
  • corollary 4: Sound Static Method Encapsulation
  • corollary 5: Sound Method Encapsulation
  • ...and 4 more