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 usin...
| Main Authors: | , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
MDPI AG
2023-11-01
|
| Series: | Applied Sciences |
| Subjects: | |
| Online Access: | https://www.mdpi.com/2076-3417/13/23/12738 |
| _version_ | 1827592481945944064 |
|---|---|
| author | Renshuang Jiang Pan Dong Yan Ding Ran Wei Zhe Jiang |
| author_facet | Renshuang Jiang Pan Dong Yan Ding Ran Wei Zhe Jiang |
| author_sort | Renshuang Jiang |
| collection | DOAJ |
| description | 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 <i>Interior Unsafe</i> 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 <i>Interior Unsafe</i> 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. |
| first_indexed | 2024-03-09T01:55:11Z |
| format | Article |
| id | doaj.art-d1a78579e35440afb079544dfe97353c |
| institution | Directory Open Access Journal |
| issn | 2076-3417 |
| language | English |
| last_indexed | 2024-03-09T01:55:11Z |
| publishDate | 2023-11-01 |
| publisher | MDPI AG |
| record_format | Article |
| series | Applied Sciences |
| spelling | doaj.art-d1a78579e35440afb079544dfe97353c2023-12-08T15:11:34ZengMDPI AGApplied Sciences2076-34172023-11-0113231273810.3390/app132312738Thetis: A Booster for Building Safer Systems Using the Rust Programming LanguageRenshuang Jiang0Pan Dong1Yan Ding2Ran Wei3Zhe Jiang4College of Computer Science and Technology, National University of Defense Technology, Changsha 410073, ChinaCollege of Computer Science and Technology, National University of Defense Technology, Changsha 410073, ChinaCollege of Computer Science and Technology, National University of Defense Technology, Changsha 410073, ChinaDepartment of Engineering, University of Cambridge, Cambridge CB2 1PZ, UKDepartment of Computer Science and Technology, University of Cambridge, Cambridge CB3 0FD, UKRust 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 <i>Interior Unsafe</i> 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 <i>Interior Unsafe</i> 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.https://www.mdpi.com/2076-3417/13/23/12738unsafe fragmentsinterior unsafestatic analysissystem safety |
| spellingShingle | Renshuang Jiang Pan Dong Yan Ding Ran Wei Zhe Jiang Thetis: A Booster for Building Safer Systems Using the Rust Programming Language Applied Sciences unsafe fragments interior unsafe static analysis system safety |
| title | Thetis: A Booster for Building Safer Systems Using the Rust Programming Language |
| title_full | Thetis: A Booster for Building Safer Systems Using the Rust Programming Language |
| title_fullStr | Thetis: A Booster for Building Safer Systems Using the Rust Programming Language |
| title_full_unstemmed | Thetis: A Booster for Building Safer Systems Using the Rust Programming Language |
| title_short | Thetis: A Booster for Building Safer Systems Using the Rust Programming Language |
| title_sort | thetis a booster for building safer systems using the rust programming language |
| topic | unsafe fragments interior unsafe static analysis system safety |
| url | https://www.mdpi.com/2076-3417/13/23/12738 |
| work_keys_str_mv | AT renshuangjiang thetisaboosterforbuildingsafersystemsusingtherustprogramminglanguage AT pandong thetisaboosterforbuildingsafersystemsusingtherustprogramminglanguage AT yanding thetisaboosterforbuildingsafersystemsusingtherustprogramminglanguage AT ranwei thetisaboosterforbuildingsafersystemsusingtherustprogramminglanguage AT zhejiang thetisaboosterforbuildingsafersystemsusingtherustprogramminglanguage |