Thetis-lathe: Guidance on Reducing Residual Safety Obstacle in System Software from Rust Source Codes

Programming languages play a crucial role in ensuring the safety of the Operating System (OS). Traditional low-level languages (e.g., C, C++), while high-performance, usually offer very limited protections on safety, and their vulnerability patches (e.g., AddressSanitizer, DangSan), while effective in mitigating some issues, are often too expensive. Rust language combines memory safety with performance, providing a fresh paradigm for constructing efficient, reliable, and dependable. However, existing Rust rely on unsafe code fragments to interface with low-level hardware and other programming languages, introducing critical issues: (1) compromised system-wide safety due to the presence of unsafe code, (2) inaccurate defect detection because of unavoidable interactions between unsafe and safe code; and (3) difficulty in finding an optimal balance between accuracy and efficiency of defect detection and elimination. In contrast to the previous work, we believe — “ prevention is always better than cure ”. Therefore, we propose a new methodology (namely Thetis) to detect and guide the minimization of unsafe fragments in Rust source code. For unsafe code detection, Thetis designs an automated inspection method based on feature extraction. For unsafe code elimination based on Unsafe Rust types and interchangeability, Thetis prop defect optimization suggestions and designs a framework to automatically provide safer code recommendations. We have designed and implemented a new tool called Thetis-lathe based on Thetis and have also ported Thetis-lathe to three mainstream Rust applications, i.e., BlogOS, rCore, and Miri Failure Set. Evaluations show that our tool improved the accuracy of defects and decreased the amount of unsafe code by 35% and undefined behavior by approximately 50%. Furthermore, Thetis-lathe speeds up the run-time about 5x compared with the sanitizer and LMbench results indicate that our approach introduces 7.6% (average) performance overhead on the entire system.

Authors

Institutions

Publication Details

Journal
ACM Transactions on Embedded Computing Systems
Published
2025-05-26
DOI
https://doi.org/10.1145/3736729
Primary Topic
Security and Verification in Computing
Type
article
Field-Weighted Citation Impact
0.00

Funders

Controls
|||
ALL TIME
JAN
FEB
MAR
APR
MAY
JUN
JUL
AUG
SEP
OCT
article

Thetis-lathe: Guidance on Reducing Residual Safety Obstacle in System Software from Rust Source Codes

Pan Dong, Yan Ding, Ran Wei, Zhe Jiang et al.
ACM Transactions on Embedded Computing Systems
Security and Verification in Computing
article

Thetis-lathe: Guidance on Reducing Residual Safety Obstacle in System Software from Rust Source Codes

Pan Dong, Yan Ding, Ran Wei, Zhe Jiang, Renshuang Jiang
article en

Abstract

Programming languages play a crucial role in ensuring the safety of the Operating System (OS). Traditional low-level languages (e.g., C, C++), while high-performance, usually offer very limited protections on safety, and their vulnerability patches (e.g., AddressSanitizer, DangSan), while effective in mitigating some issues, are often too expensive. Rust language combines memory safety with performance, providing a fresh paradigm for constructing efficient, reliable, and dependable. However, existing Rust rely on unsafe code fragments to interface with low-level hardware and other programming languages, introducing critical issues: (1) compromised system-wide safety due to the presence of unsafe code, (2) inaccurate defect detection because of unavoidable interactions between unsafe and safe code; and (3) difficulty in finding an optimal balance between accuracy and efficiency of defect detection and elimination. In contrast to the previous work, we believe — “ prevention is always better than cure ”. Therefore, we propose a new methodology (namely Thetis) to detect and guide the minimization of unsafe fragments in Rust source code. For unsafe code detection, Thetis designs an automated inspection method based on feature extraction. For unsafe code elimination based on Unsafe Rust types and interchangeability, Thetis prop defect optimization suggestions and designs a framework to automatically provide safer code recommendations. We have designed and implemented a new tool called Thetis-lathe based on Thetis and have also ported Thetis-lathe to three mainstream Rust applications, i.e., BlogOS, rCore, and Miri Failure Set. Evaluations show that our tool improved the accuracy of defects and decreased the amount of unsafe code by 35% and undefined behavior by approximately 50%. Furthermore, Thetis-lathe speeds up the run-time about 5x compared with the sanitizer and LMbench results indicate that our approach introduces 7.6% (average) performance overhead on the entire system.

ACM Transactions on Embedded Computing SystemsVol. 24(4)
National Defense University (US), National University of Defense Technology (CN), University of Cambridge (GB), Milli Savunma Üniversitesi (TR), Lancaster University (GB), Southeast University (CN)
National Natural Science Foundation of China, Basic Research Program of Jiangsu Education Department, National Key Research and Development Program of China
Openalex Percentile: Top 95%
Security and Verification in Computing
AI Navigator

Ask Laika to Summarize, Analyze, and Connect papers live on the map.

Summarize Papers & Methodologies

Extract key findings, datasets, and comparative methods across publications.

Benchmark Rankings & Visual Analytics

Rank top research institutions, authors, funders, topics, and journals by Field-Weighted Citation Impact (FWCI) and paper volume with instant charts.

Connect Distant Disciplines

Bridge topological clusters on the map to find hidden collaborative intersections.