# Theis: A Booster for Building Safer Systems Using the Rust Programming Language
## Background
### Rust Language Safety Improvement Study  
To reduce the vulnerabilities caused by unsafe fragments, researchers have conducted various studies, including code suggestions/specifications [15; 25; 26], formal verification [27; 28; 29], fuzzy testing [30; 31; 32], symbolic execution [33; 34; 35], and static analysis [36; 37; 38]. [PERSON] et al. [15] proposed six suggestions for learning and programming Rust, allowing programmers to better understand Rust's safety mechanisms and develop safer systems. [PERSON] et al. [25; 26] performed the first empirical study of Rust and proposed an important concept known as _Interior Unsafe_. _Interior Unsafe_ is defined as a pattern with a function (or an interface implementation) containing a piece of unsafe code, while the function (or interface itself) can be called safe. Regarding _Interior Unsafe_, two helpful insights were mentioned in the paper: (1) _Interior Unsafe_ is a good way to encapsulate unsafe code, and developers should first try to properly encapsulate unsafe code in _Interior Unsafe_ functions before exposing them as unsafe, and (2) _Interior Unsafe_ functions often rely on the preparation of correct inputs and/or execution environments for their internal unsafe code to be safe. Using std::sync::Mutex as an example [39] (see Listing 4), the mutex provides an encapsulated lock() API, adopting the _Interior Unsafe_ concept. Although these studies provide suggestions for building safer Rust coding specifications, they are all empirical studies, and the approaches therein depend on the developer's own familiarity with Rust and development experience. They do not effectively relieve the burden on developers. ```
impl<T:?Sized>Mutex<T>{ pubfnlock(&self)->LockResult<MutexGuard<'_,T>>{ //InteriorUnsafefunction unsafe{ self.inner.raw_lock(); MutexGuard::new(self) } } }
```  
**Listing 4**. _Interior Unsafe_ functions in the standard library. Formal verification is a method of proving the correctness of operating systems using theorems. For example, RustBelt [27] is the first formal safety proof for Rust, but it can only verify a subset rather than all of Rust's features. [PERSON] et al. [37] proposed formalization as a way of detecting defects, but since the amount of code is so large, it cannot detect all defects. [PERSON] et al. [40] proposed that due to kernel function dependencies and the global nature of verification, formal verification is very difficult. They also pointed out that verifying one line of C code requires, on average, about twenty-five lines of proof code. Therefore, as code size and dependencies increase, the complexity of verification increases, requiring a lot of manual work to perform the transformation, which reduces the efficiency. Miri [41] detects common undefined behavior in Rust code, such as out-of-bounds memory accesses, use of uninitialized data, and data races, by generating a Rust intermediate representation called MIR. However, using this tool for detection results in a significant number of false negatives and false positives. The fuzzy testing tool libPuzzer [30] requires analysis of the situation to design fuzzing targets, making it unsuitable for direct use in library APIs. LibFuzzer was further improved by RULF [31] but still infers specific types of dependencies. Therefore, this method is unsuitable for trait operations. Solutions like symbolic execution methods [33; 34] also suffer from the same issues. Rudra [36] detects memory issues in unsafe fragments through static analysis. However, it can only analyze certain problems. According to [PERSON]'s theorem [42], any nontrivial property of a language recognized by a Turing machine is undecidable. This means that a program can be considered a function that maps inputs to outputs, and there is no generic algorithm that can detect the non-trivial properties (i.e., properties that are not true or false for all programs) of this function. Therefore, there is no perfect static analysis that addresses all safety issues.