# 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 assert is used not only to check whether the state provided by the current calling environment is satisfied but also to detect the return status of the function indicated by the post-conditions if the pre-conditions are satisfied. If the function passes the detection of the pre- and post-conditions, the correctness and safety of the scheduled process will be ensured. Figure 5: Assert verification. The optimization framework for unsafe functions is illustrated in Figure 6. It is also suitable for unsafe _traits_. When all unsafe functions for a _trait_ have been optimized, the \"unsafe\" keywords can fully be removed from the _trait_. ### Defect Detection Inspection Based on Feature Analysis

Optimizing large-scale systems during development and maintenance is challenging due to the extensive manual effort required [49; 50]. To simplify these manual processes and enhance accuracy and speed, our method can automatically detect defects based on feature extraction. It also creates a log of safety checks, which provides a basis for the system to further enhance system safety. To ensure a strong correlation between the selected features and each category of Unsafe Rust operations, this paper utilizes correlation analysis methods for evaluation. We employ the SPSS data analysis tool to calculate the correlations between features and unsafe operations, which mainly fall into two categories: statistical correlations and probabilistic correlations. For statistical correlations, three calculation methods can be chosen: Pearson [51], Spearman [52], and Kendall [53]. These methods analyze the strength and direction of the relationship between two variables. For probabilistic correlations, Bayesian statistical methods can be used to analyze the degree of association between the two. After calculating the correlation coefficients for the selected features, the operations of each category of Unsafe Rust are categorized based on keywords, function names, and operations, as shown in Table 1.

Figure 6: The framework for optimizing unsafe functions or methods. Figure 7: Contract validation functions. The key information is extracted based on the lexical rules of five types of unsafe operations, e.g., keywords, function names, operators, etc., as illustrated in Table 1. The algorithm for feature recognition in defect detection is presented in Algorithm 1. This algorithm takes the operating system source code as input and uses regular expressions to classify, tag, and extract each type of unsafe operation. The output is a report containing specific defect information. ```
0: Operating system source code files;
1: Store regular expressions to describe each type of defect in regex_array[5]
2:for f in fs do
3:if ends with!-rs then
4:for i=0; i<5; i++ do
5:if regex == regex_array[i] then
6:lst = []
7:count[i]++, which is used to count occurrences
8:txt[index_1] == {_press into the stack lst.append(()
9:According to the matching item left bracket, txt[index_2] == ], out of the stack lst.pop()
10:end = index_2 - index_1, which is the defective content, is output to the txt
11:else
12:Output no match
13:endif
14:endfor
15:else
16:continue
17:endif
18:endfor
19:Defect Report
```
**Algorithm 1** Feature-based defect identification

Compared to the C language, Rust has fewer unsafe operation types, reducing the possibility of false positives and false negatives during large-scale analysis. The method proposed in this paper is based on finite-type feature extraction, which automatically addresses problems. It has the benefit of increasing the accuracy of defect detection and provides guidance for optimizing the system. ## 5 Experiments and Results

### Safety

One goal of designing and optimizing an operating system is to ensure system safety. When Unsafe Rust is unavoidable in system design, defect detection and elimination methods are important means of enhancing system safety. This section mainly tests the Theis method proposed in this paper.