A Trace-based Approach for Code Safety Analysis

Basic Information

• Paper ID: 2510.10410
• Title: A Trace-based Approach for Code Safety Analysis
• Author: Hui Xu (Fudan University)
• Classification: cs.PL (Programming Languages), cs.SE (Software Engineering)
• Publication Date: October 2025
• Paper Link: https://arxiv.org/abs/2510.10410

Abstract

Rust is a memory-safe programming language that prohibits undefined behavior. Its safety guarantees have been verified through extensive empirical research by the community, which is a key reason for its remarkable success. However, unsafe code remains a critical issue in Rust. This paper establishes a systematic framework for understanding unsafe code and undefined behavior by reviewing Rust's safety design and analyzing real-world Rust projects. It summarizes soundness standards for Rust code and further proposes actionable guidance for implementing sound encapsulation.

Research Background and Motivation

Problem Context

1. Limitations of Rust's Safety Promises: Although Rust guarantees that safe code will not lead to undefined behavior, unsafe code may still introduce security risks
2. Lack of Systematic Framework: Existing research lacks systematic theoretical analysis of the relationship between unsafe code and undefined behavior
3. Difficulty in Verifying Encapsulation Soundness: Lack of actionable methods to verify the soundness of functions and structures containing unsafe code

Research Significance

• The widespread application of Rust in systems programming makes the safety of unsafe code critically important
• Establishing a theoretical framework helps developers better understand and use unsafe code
• Provides scientific basis for security auditing of the Rust ecosystem

Limitations of Existing Approaches

• Lack of formal description of safety constraints for unsafe code
• Absence of unified soundness verification standards
• Missing systematic analysis methods from functions to structures to modules

Core Contributions

1. Establishment of Main Theorem: Formally proves the relationship between undefined behavior and unsafe code, establishing the core principle that "undefined behavior originates solely from unsafe code and is entirely determined by its safety constraints"
2. Proposal of Soundness Standards: Establishes soundness judgment criteria for safe and unsafe functions, structures, and modules respectively
3. Development of Encapsulation Guidance: Derives actionable principles and corollaries for implementing sound encapsulation
4. Construction of Audit Framework: Proposes a systematic audit method based on Unsafe Propagation Graphs (UPG)

Methodology Details

Task Definition

The core task of this paper is to establish a theoretical framework for analyzing the safety of unsafe portions in Rust code, specifically including:

• Input: Rust programs containing unsafe code
• Output: Soundness judgment and encapsulation guidance
• Constraints: Based on Rust's type system and safety constraints

Theoretical Framework Architecture

1. Core Theorem

Main Theorem (Theorem 1): For a well-typed Rust program P, undefined behavior occurs only when P contains unsafe code and violates its associated safety constraints:

P ⊢ UB ⇒ (P ∋ UC) ∧ (P ⊬ SC_UC)

where UC denotes unsafe code and SC_UC denotes the safety constraints of unsafe code.

2. Safety Constraint Assumptions

Assumption 1: Each unsafe function has explicit safety constraints with the following properties:

• Universality: Every unsafe function has safety constraints that must be satisfied
• Consistency: The safety constraints of a given function remain consistent across all call sites

3. Soundness Standards

Safe Function Soundness (Definition 2):

∀P_fs, P_fs ⊬ UB

Unsafe Function Soundness (Definition 3):

∀P_fu, P_fu ⊢ SC_fu ⇒ P_fu ⊬ UB

Encapsulation Principle Derivation

Function Encapsulation (Corollary 4)

Unified function soundness condition:

∀fu ∈ UnsafeCallee(f), (f ∪ SC_f) ⊢ SC_fu ⇒ ∀P_f ⊢ SC_f, P_f ⊬ UB

Structure Encapsulation (Corollary 7)

Soundness requirements for structure S = {C, F, M, d}:

1. Static Methods: All constructors and static methods must satisfy the function encapsulation principle
2. Dynamic Methods: Consider the impact of destructive methods, ensuring safety constraints are satisfied across all combinations of constructors and methods

Technical Innovations

1. Trace-based Analysis Method: Similar to taint analysis, treating unsafe code as taint sources and function exits as sinks
2. Hierarchical Soundness: Progressive analysis from functions → structures → modules → crates
3. Destructive Method Handling: Innovatively considers the impact of mutable methods on safety invariants of other methods
4. Unsafe Propagation Graph: Provides visualization tools for auditing

Experimental Setup

Theoretical Verification Methods

This paper is primarily theoretical work, with verification methods including:

1. Formal Proof: Proves the correctness of theorems and corollaries through logical reasoning
2. Real Project Analysis: Validates the applicability of the theory based on real-world Rust projects
3. Case Studies: Demonstrates the operability of the method through concrete examples

Evaluation Criteria

• Theoretical Completeness: Whether it covers the main scenarios of Rust unsafe code
• Practicality: Whether the derived principles are actionable
• Consistency: Alignment with Rust's official safety promises

Experimental Results

Main Theoretical Results

1. Main Theorem Proof: Successfully establishes the causal relationship between undefined behavior and unsafe code
2. Encapsulation Principles: Derives four core corollaries covering sound encapsulation of functions and structures
3. Module Extension: Extends the theory to module and crate levels, supporting both strong and weak soundness

Application Framework

Unsafe Propagation Graph (UPG) Definition:

UPG G(F, E, S(C, M, d))

• F: Set of function and static method nodes
• E: Set of edges involving unsafe calls
• S: Set of structures containing unsafe calls

Audit Subgraph Types

1. Unsafe Nodes: Require explicit safety constraint specifications
2. Unsafe Calls: Must satisfy Corollary 4 or the first part of Corollary 7
3. Structures: Must satisfy the second part of Corollary 7

Related Work

Main Research Directions

1. Rust Safety Research: Community empirical research on Rust's safety guarantees
2. Formal Verification: Formal verification methods for Rust programs
3. Unsafe Code Analysis: Static analysis tools for unsafe code

Contributions Compared to Related Work

• Theoretical Innovation: First to establish formal relationship between unsafe code and undefined behavior
• Systematicity: Provides complete analysis framework from functions to crates
• Practicality: Derives actionable audit guidance

Conclusions and Discussion

Main Conclusions

1. Establishes theoretical foundation for safety analysis of unsafe code
2. Provides systematic soundness judgment standards
3. Develops actionable audit methods

Limitations

1. Assumption Dependency: Theory is built upon assumptions about safety constraint properties
2. Complexity: UPG for large projects may become overly complex
3. Automation Level: Requires manual specification of safety constraints and invariants

Future Directions

1. Develop automated tools supporting UPG construction and analysis
2. Extend to more complex unsafe operation scenarios
3. Integrate with existing static analysis tools

In-Depth Evaluation

Strengths

1. Theoretical Rigor: Establishes a complete formal framework with clear proof procedures
2. Practical Value: Provides actionable audit guidance beneficial to actual development
3. Strong Systematicity: Complete coverage from functions to crates
4. Innovation: Introduction of trace-based analysis method is novel

Weaknesses

1. Insufficient Experimental Validation: Lacks validation experiments on large-scale real projects
2. Tool Support: No automated tool implementation provided
3. Performance Considerations: Does not discuss computational complexity and scalability of the method
4. Assumption Limitations: Assumptions about safety constraint properties may be overly idealistic

Impact

1. Academic Contribution: Provides theoretical foundation for Rust safety research
2. Practical Value: Can guide security audit practices in Rust projects
3. Tool Development: Provides theoretical support for developing automated safety analysis tools

Applicable Scenarios

• Security auditing of system-level Rust projects
• Soundness verification of Rust standard library and core crates
• Theoretical research on programming language safety
• Design and implementation of static analysis tools

References

1. Rust Team. Soundness (of code / a library). Rust Unsafe Code Guidelines.
2. Zihao Rao, et al. Annotating and Auditing the Safety Properties of Unsafe Rust. arXiv preprint arXiv:2504.21312, 2025.

Overall Assessment: This paper makes important theoretical contributions to the safety analysis of Rust unsafe code, establishing a systematic analysis framework. Although experimental validation and tool implementation require further enhancement, its theoretical value and practical potential are noteworthy. This work provides a solid theoretical foundation for Rust safety research and practice.