# Theis: A Booster for Building Safer Systems Using the Rust Programming Language
## 1 Introduction  
Traditional system-level programming languages often suffer from memory and concurrency safety issues [1; 2; 3; 4], whereas memory-safe programming languages such as GO usually suffer from significant runtime overhead [5]. Rust, the most popular system-level programming language [6; 7], balances the two scenarios through its unique safety mechanisms such as ownership and lifetime [8; 9]. These mechanisms prevent many vulnerabilities caused by memory accesses (e.g., use-after-free and buffer overflow) and thread concurrency (e.g., data competition). Essentially, Rust aims to ensure safety akin to high-level languages and performance efficiency comparable to low-level languages, making it an increasingly popular choice for building fundamental software (e.g., operating systems (OSs) and browses [10; 11]). For example, the rewriting of the Firefox kernel in Rust achieved better parallelism, safety, modularity, and performance [12]. However, despite the safety mechanisms, existing projects written in Rust may still have many serious software vulnerabilities. For example, hundreds of bugs have beenidentified in the RustSec Advisory Database [13], including rulex bugs, static-type-map unmaintained bugs, etc. The main reason for this is that Rust projects for system-level operations usually contain some unsafe code fragments, which are necessary for low-level operations but lack the safety guarantees provided by the compiler. More specifically, Rust comprises two distinct programming languages: Safe Rust (denoted by safe code) and Unsafe Rust (denoted by unsafe fragments, as the number of code lines is small). Safe Rust is recommended more by the developers of Rust, as it enables the writing of high-performance applications and libraries using safety rules, so this type of Rust code constitutes the main body of the project. On the other hand, unsafe fragments distinguish themselves using the keyword \"unsafe\" to bypass strict compiler checks to support more low-level controls. Unsafe fragments are mainly used to implement five types of operations [14]: (1) dereferencing a raw pointer; (2) calling an unsafe function or method; (3) accessing or modifying a mutable static variable; (4) implementing an unsafe _trait_; and (5) accessing fields of a _union_. Previous research has verified that a program fully written in safe code can completely avoid memory errors [13; 15; 16]; however, the unavoidable unsafe fragments may introduce vulnerabilities and make the system less safe. Although Rust does not completely address the safety issues of system-level programming, it still offers many advantages over traditional languages such as C.  
How can the safety of a system be improved when unsafe fragments are unavoidable? Formal verification is a commonly used approach, which verifies a system by exploring its state space using mathematical methods [17]. However, for operating systems, the amount of code to be verified is huge, the boundaries are extensive, and the code dependencies between kernels are high. The overhead of verification is not affordable and heavily depends on the experiences of the engineers. Therefore, we focus on minimizing unsafe fragments to reduce the unsafe state space, which requires formal verification to ensure safety. To this end, in this paper, we identify three key challenges:  
* Only formal verification approaches can completely eliminate the vulnerabilities introduced by unsafe fragments. However, the complexity and dependencies within operating systems lead to an explosion of formal verification state spaces [18; 19; 20]. This results in formal methods validating only a subset of the system, which is the main reason for the low feasibility of formalization. To address this problem, new methods are needed to reduce the set of states in the verification space, thereby reducing the amount of code and interactions between code. * Unsafe fragments in Rust can fundamentally compromise the safety of developed software, especially OSs.