Home

C/C++ is a widely used programming language for operating systems, critical software, and system software (e.g., e-mail and domain name system servers on the Internet). C/C++ developers often use memory allocated arrays, which are allocated and deallocated automatically without developer intervention. Because of their convenience, memory allocated arrays are used to store data from external inputs in the Application Programming Interface (API) function (hereinafter called “function”) calls. However, memory corruption vulnerabilities (e.g., stack allocated overflow) are found most commonly in C/C++ applications[1]. Although memory corruption vulnerabilities have received substantial attention, most solutions have failed to address the problem fully[2]. Furthermore, attackers are constantly searching for new exploits[3][4]. Most solutions presume that if secure coding rules or built-in verification functions are used for a program code, then the result of that program is safe[4]-[6]. However, if certain malicious values are supplied to the sanitization function, this does not completely protect against all attacks[3][7]. In general, it is well-known that both static analysis and dynamic analysis must be used to verify software weaknesses and for test generation. Each technique provides different solutions in terms of reliability, speed, and precision. Static analysis provides all potential execution paths but requires some heuristic for selecting only the relevant paths[8]-[10]. Therefore, it can cause false negatives. Dynamic analysis incurs high computing overhead and cannot guarantee that all possible execution paths are exercised[11][12]. Therefore, it has limited defect detection coverage.

In this paper, we propose a look-ahead dynamic technique that gives first priority to program protection from inappropriate input values so that errors are exposed as they occur in the course of executing a C/C++ application. This is based on the semantic checking of whether a statement follows according to the developers’ intentions. The crux of the technique is (1) to facilitate the modification of code that causes detected errors, (2) to prevent other codes and the entire system from being damaged despite the errors occurring in some codes, and (3) to complement the security weakness that occurs during program development or application design.

Therefore, our technique first analyzes sensitive function facets to offer a vulnerability analysis strategy for an application. Next, the technique generates a function verification operation to sanitize it. API statements that have false assertions are classified as illegal and are not allowed for execution within the application. To evaluate the proposed technique, we implemented the Semantic Function Libraries (SFLs) tool and tested it on a set of empirical test suites.

The main contributions of this paper are as follows:

• We describe a predictable programming technique that models semantic function verification operations for analysis.
• We introduce a new technique that estimates semantic functions by verifying input values.

The remainder of this paper is organized as follows: Section 2 reviews previous studies, and Section 3 details our research overview with a sample program, and Section 4 presents our experimental settings. Section 5 discusses our experimental findings and, finally, Section 6 presents our conclusions.

Fig. 1 shows a sample user-logon verification C program. This sample program consists of one Boolean variable (PasswdStus) and three string variables (Passwd, Valid_Passwd, and Org_Passwd). At line 4 in the main(), the IsPassword() is called to determine whether a user is a registered user. At line 4 in the IsPassword(), gets() function reads the logon password from the user. At line 7, the supplied password is compared with the authorized user password.

Fig. 1. 
Simple C program

In Fig. 1, gets(Passwd) function in the IsPassword() is able to store a maximum of 15 bytes consisting of characters of the byte string identified by the Passwd variable (note that we ignore the string null terminator character). If 20-byte character strings are entered into the Passwd variable, then the Passwd variable is exploited by entering a string whose size is larger than the buffer assigned to hold it. Consequently, gets(Passwd) function may be exploited as an error or an invasion window.

Consider the following program fragment from Fig. 1.

Example 1: Given the input (Valid_Passwd=NULL, Org_Passwd=”EnterMyPasswordOkay”), the program generates a statement:

strcpy(Valid_Passwd, Org_Passwd);

The input is transformed into expressions:

strcpy(Valid_Passwd, "EnterMyPasswordOkay");

strcpy() function copies a maximum of 19 bytes consisting of the characters of the byte string identified by Org_Passwd into a character array identified by Valid_Passwd. Valid_Passwd is allocated 15 bytes by the input values. Therefore, Valid_Passwd is exploited.

Example 2: Continuing from Example 1, let the function for the statement be defined as follows:

SIZE_buf = 15;
strncpy(Valid_Passwd, Org_Passwd, SIZE_buf+5);

Org_Passwd is allocated 19 bytes by the input values ("EnterMyPasswordOkay"). Valid_Passwd is allocated 15 bytes by NULL. In this case, even though strncpy() function is used instead of strcpy() function to satisfy C secure coding rules[6], Valid_Passwd is exploited. Therefore, the declaration length of the variable is not an absolute evaluation element that evaluates vulnerability. Even if a semantic characteristic exists dynamically in a function, such as in Example 2, this is not detected by analyzing the static code or syntax structure[2]. Notice that string variables are compared only in terms of the structural parts of their declaration lengths. This limitation exists because static-code or syntax-aware analysis cannot detect the semantic characteristics of a function.

On the other hand, if awareness of the semantic characteristics of a function is possible, then the original code need not be modified and developed using conventional programming practices. Retrofitting an application requires manual effort proportional to the complexity of the application. Moreover, it is not necessary to hinder debugging or maintenance. To perform a semantic operation, we need to know the set of values held by functions and variables. We define a verification operation and the corresponding variable validation.

Definition 1 (Semantic verification operation associated with a control path). Let the set of function operations be denoted by M. For any function operation m, program P can take a semantic verification operation associated with the control path. Let M0 denote the set of benign and safe semantic verification operations corresponding to function operation M[3]. Let us assume that m and m0 are extracted on the same control path and that there is an associated valid function representation function Stmt_PA: M -> M0, {(m, Stmt_PA(m)) | m ∈ DOMAIN(Stmt_PA)}, and Stmt_PA (m) = m0. Let the set of variables (or parameters) be denoted by V, and for any input variable v, let us assume that m and m0 take on the same input variable (i.e., m ≈ m0).

Therefore, given a function m(v), if we know another valuation m0(v), then we can evaluate its verification operation and deduce the control path. Assertions have been used for performance verification with respect to partial correctness to ensure that a program does not produce unexpected results for valid operations, which are "expected"[18].

Definition 2 (Evaluation of verification assertions on a variable). For m0 and the corresponding input variable v, we define assertions on variable V. A condition on a variable is any Boolean assertion function F: V → {TRUE, FALSE}, {(v, F(v)) | v ∈ DOMAIN(F)}, and F(v): assert (v.maxlen >= v.len) = TRUE.

Derivation conditions of assertions are Boolean functions that are acceptable for any derivation. The role of any assertion is to indicate whether the assertion is applicable to a derivation[18]. In our approach, we can model each operation in terms of its effect on two buffer attributes: maxlen, the number of bytes declared for the buffer, and len, the number of bytes currently in use[19]. For example, after a set of string values are inputted into variables, our approach automatically calculates the length of the selected character string. This is easily implemented using the sizeof() function, which is defined in C functions and operations. Therefore, we can trace the buffer related variable size and status by analyzing a function’s corresponding assertions. Consider the following verification assertion of strncy() function in Example 2. The assertion is checked as follows:

Valid_Passwd.maxlen ⊇ min(Org_Passwd.len, SIZE_buf+5)
Valid_Passwd.maxlen >= min(Org_Passwd.len, SIZE_buf+5)

Assertion checking is used to determine whether each assertion is false or checked in a program. An assertion means that Valid_Passwd.len should be replaced by min(Org_Passwd.len, SIZE_buf+5) and if Valid_Passwd.maxlen < min (Org_Passwd.len, SIZE_buf+5) is TRUE, then this is a fault. Therefore, given input variables in a program, a potential exploitation can be considered safe if all function assertions are TRUE[20].

In this paper, we have proposed a technique that detects and prevents vulnerabilities in an application. In applications, most vulnerabilities stem from numerous unexpected input values. However, retrofitting an application requires significant resources. It is therefore necessary to predict and trace the locations of bugs throughout the course of a program's operation. It is essential to detect errors and to minimize damage when uncontrollable or unexpected errors occur. Our approach provides a technique for validating and sanitizing instrumented code through a semantic function evaluation technique from input data in C/C++ programs, which are widely used for critical software. The proposed method is based not only on information needed to check flaws in a program, but also on the verification of statements using semantic code evaluation. The results provide evidence that it is possible to verify statements prior to their execution, thereby preventing malicious attacks. Our approach is differentiated from previous published techniques in the following ways:

• (1) We attempted to verify code vulnerabilities by generating function sanitization.
• (2) Our approach is based on semantic verification operations, but differs from traditional dynamic tainting analysis, which inspects results only after the execution of a program.

We have developed a novel technique which is useful in enforcing software security monitoring. However, further studies must be conducted on sanitization quality activities to enhance our approach.