# 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
\begin{table}
\begin{tabular}{c c c c c c} \hline \hline \multirow{2}{*}{**Name**} & **Dereferencing Raw** & **Calling Unsafe Unsafe** & **Unsafe Traits** & **Unions** & **Mutable Static Variables** \\  & **Pointers** & **Functions** & **Traits** & **Variables** \\ \hline Redox [10] & 1086 & 4129 & 513 & 454 & 321 \\ KatoOS [55] & 28 & 368 & 1 & 3 & 10 \\ Theses [54] & 89 & 335 & 10 & 1 & 12 \\ BlogOS [56] & 1 & 21 & 6 & 0 & 1 \\ ArceOS [58] & 94 & 359 & 57 & 25 & 1 \\ alloc.rs [57] & 3 & 8 & 1 & 0 & 0 \\ \hline \hline \end{tabular}
\end{table} 
Table 2: Statistics of unsafe operations. To demonstrate the flexibility of Thetis, we employed it to fix BlogOS and ArceOS. Considering the overhead of manually writing assertions and setting pre- and post-conditions, the method proposed in this paper mainly improved the axfs, axlog, and axnsnyc modules in the ArceOS modular operating system. According to the defect report, we found defects in memory.rs in BlogOS, such as the active_level_4_table() function shown in Listing 1 (in Section 2). This function was declared unsafe, and its vulnerability mainly derived from two aspects: (i) the correctness of \"physical_memory_offset\", which should map physical memory to the correct virtual memory; and (ii) the memory safety of dereferencing a raw pointer. Relying on [PERSON], we first used the _Interior Unsafe_ concept to encapsulate the unsafe operation of dereferencing a raw pointer. This reduced the range of unsafe fragments. Through static analysis, we added pre-conditions to guarantee the correctness of \"physical_memory_offset\". The repaired code is shown in Listing 8. The optimization process of unsafe _traits_ is similar to that of unsafe functions. First, the specific causes of the unsafe trait are analyzed. Then, it is encapsulated and verified using the _Interior Unsafe_ and ACSL methods. For unsafe traits that cannot be encapsulated, pre- and post-conditions are added for each of the methods. Thus, developers can be further guided in performing the subsequent checking process. ```
fnactive_level_4_table(physical_memory_offset:VirtAddr)-> &'staticmutPageTable{ let(level_4_table_frame,_)=Cr3::read(); letphys=level_4_table_frame.start_address(); //Determineifthepassedphysical_memory_offsetis correct assert!(physical_memory_offset,VirtAddr:new(boot_info. physical_memory_offset); letvirt=physical_memory_offset+phys.as_u64(); letpage_table_ptr:*mutPageTable=virt.as_mut_ptr(); //Encapsulationofdereferencearawpointers raw_usage(page_table_ptr); } pubfnraw_usage(r:&'staticmutPageTable)->&'staticmut PageTable{ assert! (!r.is_null()); unsafe{&mut*r} }
```
Listing 8: Optimize active_level_4_table(). The unsafe operation of accessing and modifying static variables was found in the source gdt.rs according to the defect report, as shown in Listing 3 (in Section 2)). Under the guidance of [PERSON], we replaced it with a mutex, and the optimized result is shown in Listing 9. Accessing static variable optimization process. ``` letSTACK=Mutex::new(vec! [0;STACK_SIZE]); letstack_guard=STACK.lock().unwrap(); letstack_start=VirtAddr::from_ptr(stack_guard.as_ptr()); \begin{table}
\begin{tabular}{c c c} \hline \hline
**System** & **Detection Method** & **Detection Accuracy** \\ \hline Hubris & Defect detection based on feature extraction & 87.8\% \\ BlogOS & Defect detection based on feature extraction & 80.6\% \\ ArceOS & Defect detection based on feature extraction & 85.4\% \\ ArceOS & Miri (Defect Detection Techniques for Rust Language) & 63.6\% \\ \hline \hline \end{tabular}
\end{table} 
Table 3: Defect detection accuracy. Since a union is not used in BlogOS and ArcoOS, the processing is not described here. We checked the repaired system again and compared it to the original one. The number of unsafe operations changed, as shown in Figure 8.  
In Figure 8, it can be seen that after using Thetis to repair the BlogOS and ArceOS modules, the overall number of unsafe operations decreased by about 41.3% and 45%, respectively.