# Theis: A Booster for Building Safer Systems Using the Rust Programming Language
## 4 Design and Construction of Thetis
### Functionally Equivalent Replacement
#### 4.1.2 Replacement of _Union_ Types
The reason for this is that there is no way to guarantee memory safety. To address this problem, [PERSON] automates the process of locating code corresponding to operations that dereferenced raw pointers to adjust the structure of unsafe fragments through _Interior Unsafe_ encapsulation. An encapsulated function is shown in Step 2 in Figure 4.

In addition, we propose a new specification for the encapsulated library functions based on the ACSL method, further reducing the vulnerabilities of the dereferenced raw pointers. The specific design process for the encapsulated functions is as follows:

1. We use _'static_ (the standard Rust static lifetime annotation) to explicitly mark the lifetime of raw pointers. Although this method may indicate a lifetime exceeding the actual one for a raw pointer, the compiler will be able to perform borrow checking and incorporate the RAII (Resource Acquisition Is Initialization) concept [46] to automatically recycle and clean memory, thus reducing undefined behaviors. 2. We use an assert to constrain the execution state of the program at runtime. The goal of an assert in ACSL is to verify the correctness of the code (Figure 5). When the assert code is correct, it can be stated the code that runs before the assert is valid. Thetis inserts the assert before the dereferenced raw pointers, which guarantees that only legal memory can be accessed. Figure 4: Encapsulation of dereferenced raw pointers. For optimization, Thetis encapsulates the operation of dereferencing the raw pointer and provides a safe calling interface. Step 3 in Figure 4 demonstrates how to use static analysis to ensure safety after encapsulation. Also, the Thetis function is flexible and extensible. The most common way to safely use raw pointers is to ensure that the dereferenced pointer is not null and is correctly aligned with the reference target type. In our implementation, Thetis provides a more general framework to guide the elimination of unsafe states in unsafe code. Therefore, we use is_null in the assert to provide a minimum level of safety. However, it can be combined with context to incorporate checks on pointer memory addresses, which can further enhance safety. The performance cost of assertion instructions can vary depending on several factors, including the complexity of specific implementations and assertion conditions. We discuss the performance impact in Section 5.2. #### 4.2.2 Measures for Unsafe Traits/Functions

A _trait_ is unsafe when it is implemented using any method with unsafe functions (fns). Therefore, ensuring the safety of the unsafe _trait_ is equivalent to reducing the scope of the unsafe functions. Most implementations treat the entire function body of an unsafe function as a large unsafe block, which expands the scope of unsafe fragments, making it more dangerous and difficult to detect unsafe operations. Based on principles 2 and 3, Thetis takes measures to encapsulate and validate unsafe functions and _trait_ code. The method relies on the _Interior Unsafe_ concept. It adjusts the scope of the vulnerabilities in functions and then replaces them with an _Interior Unsafe_ block, as shown in Step 2 in Figure 6. This method efficiently reduces the scope of the vulnerabilities and makes it easier to check for them. With the scope of the vulnerabilities reduced, the process of improving and verifying safety is further simplified. Additionally, for some _Interior Unsafe_ functions, the safety depends on the input and the execution environment [26] so it is essential to describe the context. ACSL provides a function contract design to verify the legitimacy of the code [47; 48], which is expressed as a Hoare logic expression (_(pre-condition) function body [post-condition]_), as shown in Figure 7. Thetis annotates function calls with appropriate pre- and post-conditions for _Interior Unsafe_ functions according to the verification logic.