Bypassing Redundant Safety Checks in Rust via Static Analysis
Rust is an emerging programming language with superior security reliability. Its safety is guaranteed by both sophisticated validations in compile time and comprehensive safety checks at runtime. Beyond safety mechanisms, Rust provides a critical keyword \texttt{unsafe}, allowing users to perform more efficient low-level memory operations while bypassing partial safety constraints. In practice, Rust provides many standard library APIs as safe/unsafe counterparts that share the same underlying safety conditions. The safe versions include runtime safety checks to ensure that arguments satisfy the required safety conditions, while the unsafe versions invoke unsafe primitives and rely on external safety guarantees. Therefore, unsafe implementations are more flexible, but also introduce greater safety risks. We compare the behavioral differences between all paired safe/unsafe counterpart implementations in the Rust standard library, and abstract their safety conditions. According to their requirements, the safety conditions of some safe API calls in real programs may already guaranteed to hold, making the corresponding runtime checks redundant. In this paper, we propose an approach based on abstract interpretation to efficiently detect such safe APIs calls and replace them with their unsafe counterparts to eliminate redundant runtime checks. The proposed approach is evaluated on real-world Rust crates, comparing performance before and after the safe-to-unsafe replacements. Experimental results indicate that after the safe replacement of all identified program sites, the substituted operators can achieve speedups of up to $36$%.
Sat 18 JulDisplayed time zone: Brisbane change
16:00 - 17:30 | Session 5: Program Analysis, Verification, and Code TransformationResearch Track / New Idea at Ballroom Chair(s): Zihan Wang The University of Queensland and CSIRO's Data61 | ||
16:00 15mTalk | Bypassing Redundant Safety Checks in Rust via Static Analysis Research Track Yunlong Yu Shandong University, Qingdan Meng Shandong University, Wei Zhang Shandong University, Lei Ju Shandong University | ||
16:15 15mTalk | Feedback-Oriented Retrieval and Guided Editing for Java Meta-Decompilation Research Track | ||
16:30 15mTalk | Value Analysis of Floating-Point Fortran Programs by Combining Interval and Zonotopic Abstractions Research Track Dengping Wei National University of Defense Technology, Banghu Yin College of Computer, National University of Defense Technology, Changsha, China, Yi Huang National University of Defense Technology, Liqian Chen National University of Defense Technology File Attached | ||
16:45 15mTalk | Editor Specialization: Deriving DSL Editors through Editing Service Lifting Research Track Ziheng Wang Peking University, Zhichao Guan Peking University, Xiaoyang Lu Purdue University, Di Wang Peking University, Hongjie Chen Peking University, Zhenjiang Hu Peking University File Attached | ||
17:00 15mTalk | Predicates with One Hole for Linked Data Structures in Separation Logic Research Track Xingpeng Liu National University of Defense Technology, Yanjun Wen National University of Defense Technology, Hengzhu Liu National University of Defense Technology, Ji Wang National University of Defense Technology | ||
17:15 15mTalk | ACSLAgent: Generation and Synthesis of Formal Specifications for C programs via LLM-based Agent New Idea Lezhi Ma Nanjing University, Han Wang Nanjing University, Shangqing Liu Nanjing University, Lei Bu Nanjing University | ||