# Theis: A Booster for Building Safer Systems Using the Rust Programming Language
## 3 Thetis Design Ideas  
As discussed in Section 1, the amount of unsafe code and dependencies are the main causes of unsafe systems and formal verification difficulties. Enhancing the safety capability of Rust and systems developed using Rust necessitates the implementation of a new methodology to (i) limit the use of unsafe fragments, and (ii) minimize the occurrence of unplanned interactions between safe and unsafe code. Regarding (i), we have observed that the specification-like solutions [15; 25; 26] introduce a lot of subjective randomness, the test-like solutions [33; 37; 38] all lack accuracy due to the existence of false positives and false negatives, and the formal-like solutions [27; 31; 34] mostly prove a subset of the language due to state explosions and heavily depend on a lot of experts' efforts. Therefore, the key idea for addressing this challenge is to balance the trade-off between test efficiency and proof complexity by minimizing the use of unsafe code as much as possible. The limited types of unsafe code in Rust provide a means to achieve this. Regarding (ii), the Rust programming specification suggests encapsulating unsafe operations with a safe interface [15; 25; 26]. _Interior Unsafe_ functions are an effective way to realize this. Using _Interior Unsafe_ functions to encapsulate unsafe fragments may provide a safe calling interface for developers. It significantly reduces the scope of unsafe fragments and the interactions between unsafe and safe code. These implementations are generally subjected to rigorous manual checks, so the safe code interfaces built on top of these implementations can be assumed to be safe. We note the second insight about _Interior Unsafe_ functions in [25] and develop a novel idea to use ACSL to enhance their safety. This idea partially addresses the problem of the preparation of correct inputs and/or execution environments, and it can also reduce the state space of the formal verification. With this in mind, we propose a new methodology, known as Thetis. The overall design of Thetis is based on the idea of minimizing the use of unsafe fragments and follows four principles:  
* **Principle 1: Functionally equivalent replacement. ** For finite-type unsafe operations, Thetis first replaces them with functionally equivalent safe Rust functions where possible. This principle directly eliminates the vulnerabilities of unsafe fragments. * **Principle 2: _Interior Unsafe_ encapsulation. For unavoidable unsafe operations, Thetis encapsulates those that cannot be replaced within _Interior Unsafe_ functions. This principle reduces the scope of unsafe effects, thus indirectly reducing the vulnerabilities of unsafe fragments. * **Principle 3: Adding the ACSL formal specification. ** New ACSL formal specifications are presented to constrain the potential vulnerabilities of _Interior Unsafe_ encapsulated functions. This principle provides lifetime support and partial verification to the variables or operations in the _Interior Unsafe_ section. * **Principle 4: Automatic defect detection and revision. ** Thetis introduces an automatic detection technique for extracting defects based on unsafe features, and the generated defect report provides guidance for minimizing unsafe fragments. Thetis can automatically provide the suggested safe code to replace the unsafe code, with the same functionality. The basic Thetis framework is shown in Figure 2. Specifically, Thetis manages five types of unsafe operations in a flexible, safe, and efficient manner, as discussed in Section 2. Thetis is designed based on a finite type of unsafe operations, reducing the complexity of optimization and the possibility of false positives and false negatives and ensuring that the system is as safe and reliable as possible. Firstly, it tries to directly replace the mutable static variables and _union_ types with safe implementations to eliminate unsafe fragments. Before diving into the specific design details, we reiterate the necessity and reasons for the replacement.