Treffer: Thetis: A Booster for Building Safer Systems Using the Rust Programming Language.

Rust is a new system-level programming language that prioritizes performance, safety, and productivity. However, as evidenced in many previous works, unsafe code fragments broadly exist in Rust projects. The use of these unsafe fragments can fundamentally violate the safety of systems developed using the programming language. In response to this problem, we propose a novel methodology (Thetis) to enhance the safety capability of Rust. The core idea of Thetis is to reduce unsafe code, encapsulate unsafe code using safety rules, and make it easier to verify unsafe code through formal means. The proposed methodology involves three main components. In the context of Rust itself, Thetis combines replacement and encapsulation for Interior Unsafe segments, minimizing unsafe fragments and reducing unsafe operations and their range. For systems developed using Rust, new ACSL formal statutes are applied to reduce the unsafe potential of the encapsulated Interior Unsafe segments, enhancing the safety of the system. Regarding the development life cycle in Rust, Thetis introduces automatic defect detection and optimization based on feature extraction, improving engineering efficiency. We demonstrate the effectiveness of Thetis by using it to fix defects in BlogOS and ArceOS. The experimental results reveal that Thetis reduces the number of unsafe operations in these OSs by 40% and 45%, respectively. The use of Miri to detect and eliminate defects in ArceOS reduces the likelihood of undefined behavior by about 50%, which effectively demonstrates that the proposed method can improve the safety of the Rust system. In addition, performance test results from LMbench show that the performance loss caused by Thetis is only 1.076%, thereby maintaining the high-performance characteristics of the Rust system. [ABSTRACT FROM AUTHOR]

Copyright of Applied Sciences (2076-3417) is the property of MDPI and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)