arXiv subjects

Xizhe Yin

Publications and source records attributed to Xizhe Yin.

4 recordsLinked to original sources

arXiv2026

UnsafeChecker: Finding Soundness Bugs in Rust Safe Abstractions

Rust guarantees memory safety without garbage collection through a strict ownership and borrowing system. However, for low-level systems programming, many widely used libraries rely on the unsafe keyword. These libraries encapsulate raw-pointer operations behind safe APIs to form safe abstractions. A single mistake in this internal unsafe code can break its safety contract, rendering the abstraction unsound and allowing safe clients to trigger undefined behavior. Detecting these potential soundness violations is challenging. Existing static analysis tools for C/C++ ignore Rust-specific safety contracts, while current Rust tools lack the deep semantic modeling required to track the contexts that raw pointers erase. To address this gap, we present UnsafeChecker, a compiler-integrated static analysis framework for detecting potential soundness violations in Rust safe abstractions. UnsafeChecker analyzes Rust MIR using a flow-sensitive abstract interpretation that maintains a shared state with three components: ownership, object validity, and layout. Each warning rule consumes the subset of facts needed for the corresponding Rust safety obligation. UnsafeChecker reports both instruction-level undefined behavior and boundary-level contract violations that may escape through safe APIs. We evaluate UnsafeChecker on a benchmark of 46 RustSec vulnerabilities, which contain 53 ground-truth bugs. UnsafeChecker outperforms several state-of-the-art tools, detecting 32 CVEs and covering 36 bugs (67.9% recall) with 51.6% alert-level precision. Furthermore, in a large-scale scan of real-world crates on crates.io, UnsafeChecker uncovered 114 previously unknown bugs across 83 crates, with 45 confirmed and 27 already fixed by maintainers.

cs.PL↗

arXiv2025

An Empirical Study of Rust-Specific Bugs in the rustc Compiler

Rust is gaining popularity for its well-known memory safety guarantees and high performance, distinguishing it from C/C++ and JVM-based languages. Its compiler, rustc, enforces these guarantees through specialized mechanisms such as trait solving, borrow checking, and specific optimizations. However, Rust's unique language mechanisms introduce complexity to its compiler, leading to Rust-specific compiler bugs that are less common in traditional compilers. With Rust's increasing adoption in safety-critical domains, understanding these language mechanisms and their impact on compiler bugs is essential for improving the reliability of both rustc and Rust programs. Yet, we still lack a large-scale, detailed, and in-depth study of Rust-specific bugs in rustc. To bridge this gap, this work conducts a comprehensive and systematic study of Rust-specific bugs in rustc, with a particular focus on the components that support its unique language features. Our analysis examines issues and fixes reported between 2022 and 2024, with a manual review of 301 valid issues. We categorize these bugs based on their causes, symptoms, affected compilation stages, and test case characteristics. Additionally, we evaluate existing rustc testing tools to assess their effectiveness and limitations. Our key findings include: (1) rustc bugs primarily arise from Rust's type system and lifetime model, with frequent errors in the High-Level Intermediate Representation (HIR) and Mid-Level Intermediate Representation (MIR) modules due to complex checkers and optimizations; (2) bug-revealing test cases often involve unstable features, advanced trait usages, lifetime annotations, standard APIs, and specific optimization levels; (3) while both valid and invalid programs can trigger bugs, existing testing tools struggle to detect non-crash errors, underscoring the need for further advancements in rustc testing.

cs.PL↗

arXiv2025

Analysis of Stable Vertex Values: Fast Query Evaluation Over An Evolving Graph

Evaluating a query over a large, irregular graph is inherently challenging. This challenge intensifies when solving a query over a sequence of snapshots of an evolving graph, where changes occur through the addition and deletion of edges. We carried out a study that shows that due to the gradually changing nature of evolving graphs, when a vertex-specific query (e.g., SSSP) is evaluated over a sequence of 25 to 100 snapshots, for 53.2% to 99.8% of vertices, the query results remain unchanged across all snapshots. Therefore, the Unchanged Vertex Values (UVVs) can be computed once and then minimal analysis can be performed for each snapshot to obtain the results for the remaining vertices in that snapshot. We develop a novel intersection-union analysis that very accurately computes lower and upper bounds of vertex values across all snapshots. When the lower and upper bounds for a vertex are found to be equal, we can safely conclude that the value found for the vertex remains the same across all snapshots. Therefore, the rest of our query evaluation is limited to computing values across snapshots for vertices whose bounds do not match. We optimize this latter step evaluation by concurrently performing incremental computations on all snapshots over a significantly smaller subgraph. Our experiments with several benchmarks and graphs show that we need to carry out per snapshot incremental analysis for under 42% vertices on a graph with under 32% of edges. Our approach delivers speedups of 2.01-12.23x when compared to the state-of-the-art RisGraph implementation of the KickStarter-based incremental algorithm for 64 snapshots.

cs.PF↗

arXiv2020

Temporal Logic of Composable Distributed Components

Distributed systems are critical to reliable and scalable computing; however, they are complicated in nature and prone to bugs. To modularly manage this complexity, network middleware has been traditionally built in layered stacks of components. We present a novel approach to compositional verification of distributed stacks to verify each component based on only the specification of lower components. We present TLC (Temporal Logic of Components), a novel temporal program logic that offers intuitive inference rules for verification of both safety and liveness properties of functional implementations of distributed components. To support compositional reasoning, we define a novel transformation on the assertion language that lowers the specification of a component to be used as a subcomponent. We prove the soundness of TLC and the lowering transformation with respect to the operational semantics for stacks of distributed components. We successfully apply TLC to compose and verify a stack of fundamental distributed components.

cs.PL↗