Abstract
Abstract-An approach is presented for the detection of software vulnerabilities using the widely known SPIN model checker. Classes of vulnerabilities in C programs that can be detected using the presented approach are discussed. We present the results of experiments on detecting vulnerabilities in student made software tools implementing array processing algorithms.
INTRODUCTION
Ensuring software security is becoming an extremely important topic, especially for software used in critical systems (communication systems, health protection, a number of protocols in communication systems, etc.), where a lot of programming is done in the C language. Secure software is often defined as software without vulnerabilities, that is why a lot of attention is paid now to methods of vulnerability detection in C programs.
There are two trends in vulnerability detection. The first trend is analyzing the software code without actually executing the software (static vulnerability detection); the second trend, in turn, demands the actual execution of the software code (dynamic vulnerability detection) [1] . Methods of static vulnerabil ity detection are already deeply investigated, and today we have quite a range of software code analyzers in free distribution [2] . The majority of known methods for dynamic vulnerability detection are in general limited to random search based testing [3] . That is why we are especially interested in those methods for dynamic vulnerability detection that provide not random input data but only the data able to cause the incorrect operation of the software.
One of the possible options of automatized collection of input data for dynamic vulnerability detection is to use model checkers [4, 5] . Model checkers actually check whether there are such input data for the software that the properties corresponding to the existence of the tested vulnerability hold. If such data are found, a model checker provides the necessary counterexample. Then, on the basis of the counterexam ple, input data are formed and fed to the software being checked. If the software operates incorrectly, then the vulnerability is found. If the opposite is true, then we can state that the model checking was done incorrectly. In this paper, we show how some vulnerability classes can be detected using the widely known SPIN model checker. SPIN is a freely distributed model checker; thus, this software is accessible via the official SPIN website [5] . Experiments were performed with student made software implementing array processing algorithms (the calculation of the average value, sorting, searching for minimal and maximal elements) that are widely used in a number of applications. Considering the fact that the efficiency of the counterexample search essentially depends on the algorithm of the input data generation, we devoted a separate section of the present paper to reviewing the possible methods of such generation for SPIN model checkers. 
A SPIN based

VULNERABILITIES IN C PROGRAMS AND METHODS FOR THEIR DETECTION USING THE SPIN MODEL CHECKER
As already noted, a vulnerability is a property of a C program, and, in order to check whether the pro gram possesses this property, we use the SPIN model checker [5] , which allows performing dynamic vul nerability detection in the program. To use SPIN, one should create a model of the original software with the special PROMELA language; the PROMELA program serves as the input for the SPIN model checker. Consequently, there is a problem of translating the C instructions into PROMELA instructions. The PROMELA language is developed to work with distributed systems, and, instead of the operators and functions used in the C language, it has processes with one main process (similar to the main() function in C). The processes are executed simultaneously. If the software has a vulnerability in its PROMELA model, then, as any model checker, the SPIN outputs the counterexample with the corresponding values of the local variables or input data. In this case, it is possible to perform a test injection, i.e., to feed "bad" data to the software in order to demonstrate the erroneous code to the programmer. However, as PROMELA is a modeling (not programming) language, the constructed PROMELA specification as a rule is not equivalent to the original C program; generally, a counterexample generated by SPIN cannot at once demonstrate a vulnerability after a test injection. Thus, a test injection is also necessary to check the correctness of translating C to PROMELA translation.
In this paper, we consider a vulnerability as a property of software that allows a user to violate its con fidentiality, integrity, and/or accessibility. Consider a set of vulnerabilities in a C program. If the C pro gram does not possess any property from this set, it is considered to be secure w.r.t. the given set of vulner abilities; otherwise, it is considered to be insecure. In this paper, we discuss three vulnerability types: buffer overflow, arithmetic underflow, and double free vulnerability. For buffer overflow, which is very typical for C programs, we discuss three independent cases: type overflow, type conversion overflow, and array over flow. We also pay attention to so called string overflow, which sometimes happens while copying a string to another string in C code. We note that the proposed methods of vulnerability detection are applicable only to a narrow class of software written in C. In particular, this paper does not consider C++ software employing object oriented programming. Moreover, the software being checked should not contain nested calls of functions.
On the one hand, such restrictions reduce the class of software to which a proposed method is appli cable; on the other hand, as a rule, vulnerability detection is performed not for the application as a whole but for some of its parts (e.g., a function or a block of instructions).
Type Overflow
Type overflow can happen in a C program in the case when the value of an expression e is assigned to a variable v; i.e., v = e. If the variablev is of the type t and the value of the expression e exceeds the maxi mum value for this type (max_t), then this C program possesses a vulnerability of type overflow. Such a vulnerability can be demonstrated using a simple example when e = n1 + n2. In this case, in the corre sponding C code, there can be the following instructions:
To describe this case in the PROMELA language (create a PROMELA specification), we describe three PROMELA processes. Two of them are used to model the input data (n1 and n2), while the third one is used to perform model checking the property n1 + n2 < (max_t + 1). This property is described in PROMELA as an assertion that must not be violated. In the case that SPIN detects this assertion viola tion, as a rule, one concludes that there is a type overflow vulnerability in the original C program. An example of the translation of C code into PROMELA code is in Table 1 . In should be noted that, for the sake of simplicity, the variable max_t in the corresponding code has the value 256 (the maximum for the unsigned_char type increased by 1).
If SPIN detects the violation of the assertion n1 + n2 < max_t, then it outputs the corresponding coun terexample (the values of the variables n1 and n2). In this example, where the variable v is of unsigned_char type, the model checker outputs a counterexample where n1 = 205 and n2 = 200. If the n1 and n2 variables are not immediate input data for the software, then, while generating the counterexam ple, SPIN outputs all the values of the variables that influence the n1 and n2 values; thus, there is a possi bility to observe the values of both internal and external variables that can provoke the corresponding vul nerability in the original C program. To confirm the existence of vulnerability, the counterexample data are sent to the software input (test injection). In the example above, we illustrated the detection of type overflow vulnerability when working with bytes (unsigned_char type). In this case, we were checking whether the value of the variable v can happen to be more than 255. This approach is naturally applicable to other C variable types, such as int, short, and unsigned short with the corresponding max_t boundary and the corresponding variable types in PROMELA. For the C types, the bool, int, and short PROMELA types are identical; to work in PROMELA with the unsigned short type one may describe the unsigned type, which is used for storing 16 bit variables.
Type Conversion Overflow
Similarly to type overflow vulnerability, one can detect type conversion overflow. Such vulnerability can happen in the C code when the variable v1 of the type t1 is assigned the value of the variable v2 of the type t2, and max_t1 < max_t2. As an example, consider the variable t1 of the int type and the variable t2 of the char type. Assume that v2 is an input variable of a C program. In this case, the C program contains the following instructions: char v1; int v2; scanf(''%d'', &v2); v1 = v2;
To derive a PROMELA model of such program, similar to Case 1, we describe a special process input to generate the value of variable v2, and a separate process is used to check the corresponding property. The last process, where the variable max_t1 is increased by 1, will be the following:
init { max_t1 = 256; run input(); done == 1; assert(v2 < max_t1); } As can be seen from the example above, type overflow and type conversion overflow vulnerabilities are very similar and their detection is performed in the same way. That is why these vulnerabilities are often combined into one notion of "type overflow."
Array Overflow
Array overflow vulnerability can happen when a programmer works with an array a of size size_a and utilizes the variable a[i] such that i >= size_a. We consider a simple example when i is an input parameter for the program. In order to detect this vulnerability, we again describe two PROMELA processes, the first of which is used to model the i value, and the second is for checking the corresponding property. Below in Table 2 there is an example of the translation of the C code into the PROMELA code. For this example, SPIN outputs violation of i < size_a for i = 1 073 741 824.
Arithmetic Underflow
Arithmetic underflow vulnerability is very similar to the buffer overflow vulnerability, and sometimes it is even considered as its special case. Arithmetic underflow can happen in a C program in the case when the value of an expression e is assigned to a variable v; i.e., v = e. If the variable v is of the type t and the value of the expression e is less than the minimal value for this type (min_t), then this C program possesses a vulnerability of arithmetic underflow. In order to detect this vulnerability, we derive PROMELA speci fication similar to the one in Section 2.1. The difference is in the assertion to check the property. In this case, the assertion required by PROMELA looks like assert((min_t -1) < e).
String Overflow
String overflow vulnerability can happen in the C program when a programmer copies one string into another. As an example of this vulnerability, we can discuss the well known function strcpy(char * dest, const char * src) from the string.h library. String overflow occurs when a programmer uses this function and the size of the src string (size_src) exceeds the size of the dest string (size_dest). It should be noted that this vulnerability is easily detected by the SPIN model checker. In this case, the corresponding PROMELA assertion looks like assert(size_src <= size_dest).
Double Free Vulnerability
Incorrect memory use can also be the cause of vulnerabilities. Double free vulnerability appears when the * p pointer is declared in the C program and a programmer repeats freeing memory allocated for * p. It should be noted that working with pointers through new and delete operators is possible only in the C++ language (not in "pure" C), but the related double free vulnerability is comparatively easily detected with the help of the proposed method, that is why it is presented in this paper.
In order to detect this vulnerability, we declare the variable v in the PROMELA program and initially assign its value to zero. Then, we "scan" the original C program instruction by instruction; each time we find a new operator in the C (C++) code, we increase the value of v by 1 in the corresponding PROMELA program and, vice versa, each time we find a delete operator in the C (C++) code, we decrease the value of v by 1. If the original C program does not possess double free vulnerability, the variable v in the PROMELA code has the value 0 or 1, so the corresponding assertion looks like assert((-1 < v)&&(v < 2)). Below in Table 3 there is the corresponding translation of the C code in the PROMELA code for the case when elements of the array p are of the type int.
The proposed methods of vulnerability detection were implemented as software. However, the task of deriving the PROMELA model from the C program is rather labor intensive; some PROMELA models were completed "by hand" in the process of performing experiments on detecting vulnerabilities in C pro grams. Moreover, as the model does not reflect all the characteristics of the modeled object, we check that the counterexamples of the PROMELA program really correspond to "bad" input data for the original C program. The check is done by test injection from the counterexample into the original C program. In our experiments, all the vulnerabilities detected through the PROMELA model corresponded to vulnerabili ties in the original programs. It should also be noted that the counterexample generation is a separate task, which seriously influences the result of the vulnerability detection. Thus, in the next section, we briefly discuss the possible methods for the input data generation. 
INPUT DATA GENERATION
The time consumed by the SPIN model checker for the generation of counterexamples essentially depends on the algorithm of the input data generation defined in the PROMELA model. In this section, we briefly discuss various options for such generation. It should be noted that the SPIN model checker and the PROMELA modeling language have an advantage of the nondeterministic instruction execution, in particular because of the parallel execution of PROMELA processes. Consequently, the input data gen eration will be done not strictly according to the defined algorithm and the demanded counterexample can be faster found. During the next step, in turn, the SPIN can randomly choose a process to execute. Accordingly with the generated input data, several processes are executed in order to use this nondeter minism. Below, we briefly describe some ways of generating input data that can be implemented in the PROMELA model for the original C program. We further assume that n is a variable of type t which value should be generated; min_t and max_t are the lower and upper boundaries of the type t.
Generating Input Data in Steps
We now discuss how input data to check the software can be generated using the example of a program with input parameter n. The method starts with the variable n, which is assigned a lower boundary of type t; i.e., n = min_t. As a rule, after preliminary experiments, the value step is determined that corresponds to the step size. The next value of the variable n is defined as the sum of the current value and the step; i.e., n = n + step. This process is repeated until a counterexample is found or n exceeds max_t. A counterexample will not always be found with such generation, but the smaller step is, the higher is the probability of its detection.
Step wise Input Data Generation
Similar to the first method, the initial value of the n coincides with the lower boundary min_t. Then, we choose two steps: step1 and step2. The first step step1 is "big" and defines the movement of the value of the variable n from the lower boundary to the upper one, i.e., n = n + step1. This increase continues until a counterexample is found or the next value of n exceeds the upper boundary max_t. The second step step2 value is "small" and is used for the movement from the upper boundary to the lower one; i.e., n = n -step2. For example, the input data n1 and n2 generation in the Section "type overflow" starts with the initial value zero. One hundred is added to the next generated value; then, the value is multiplied by two (step1 = n). Increasing the n1 and n2 continues until the generated number exceeds the maximum value for the byte type, i.e., 255. If the 255 limit is reached, five is iteratively subtracted from the generated integer. This step wise process consisting of adding a "big" (close to the type boundary) number and subtracting a "small" one allows to find a counterexample for the type overflow vulnerability equal to n1 = 205 and n2 = 200 fast enough (it takes a second or less). 
Generation of Boundary Values
Several authors noted that, in some cases, boundary testing turns out to be rather efficient [7, 8] . In this case, the value of the variable n is assumed to be equal to min_t, and then with a "small" step size step (1 in the majority of cases) we increase the current value of n. The process n = n + step is finished after k itera tions with k being rather small. If a counterexample is not found, the variable n is assigned as max_t. Then, n is decreased not more than k times with the same step size step until a counterexample is found (if it is possible).
It should be noted that usually a combination of the above mentioned methods is the most efficient way. Besides, in particular tasks, the method of input data generation for the scanf function in the PROMELA model and other input functions is selected depending on the problem to be solved and/or on the basis of the preliminary investigation. In the future, the authors plan to conduct experimental research where the proposed methods of the input data generation will be implemented and used to test the security of student C programs implementing various algorithms.
EXPERIMENTAL RESULTS OF VULNERABILITY DETECTION IN C PROGRAMS
In this Section, we present the results of experiments on the detection of vulnerabilities in C programs. Student made software functions developed in the C language are taken as examples for experimental evaluation. Such software tools include programs containing various operations with arrays: the search for the minimal and maximal items of an array, a number of array sorting, and the calculation of the average value. We note that these examples are rather small and easy to develop but are widely used in the real world, because, in general, array items can contain not just basic data types but abstract types on which various relations can be specified, particularly, order relations. To check for a vulnerability in a C program with the help of the method described in Section 1, the program's instructions are translated into PROMELA instructions, and then the corresponding assertions are inserted where necessary. Type over flow vulnerabilities were detected in student made programs developed for finding the average item value in the array. After feeding data from the generated counterexamples, the programs did not output any alerts about incorrect data; moreover, before this testing, the programs were considered to be operating correctly.
As a result of the experiments, array overflow vulnerability was also detected in other C programs where the memory for an array is allocated statically and then the user enters the real array size. Below are some of them:
1. Software to find the minimal (maximal) element in an array; 2. Software to sort an array using the bubble sort method; 3. Software to sort array using the insertion method; 4. Software to find prime integers within the interval [1, n] for a given n (Eratosthenes sieve). It should also be noted that for all the tested programs, there was no need to generate another SPIN counterexample. This proves the correctness of translating C to PROMELA translation and the efficiency of the proposed method for dynamic vulnerability detection in software.
Thus, as a result of the conducted experiments with the available implementations of widely used algo rithms for array processing, we detected type overflow and array overflow vulnerabilities in this software. As is stated in [9] , such vulnerabilities sometimes are not detected by static code analyzers. This proves the necessity to use dynamic methods for vulnerability detection. Besides, in all the programs from Section 1 into which the vulnerabilities in question were inserted intentionally, all these vulnerabilities were detected.
CONCLUSION
This paper is devoted to a SPIN based approach for detecting vulnerabilities in C programs, since the disadvantages of static code analyzers cause the need to develop new approach for dynamic vulnerability detection. As SPIN accepts programs written in PROMELA language, this paper also provides a number of rules for translating C instructions into PROMELA instructions. Experiments with student made soft ware prove the known fact that it is necessary to check software both with static and dynamic methods and also prove the possibility of using SPIN to test the security of C programs. Because it is rather labor inten sive to translate C programs into the Promela language, in the future we plan to improve this approach through getting rid of the translation operation. In particular, we plan to evaluate the possibility to use an intermediate language, e.g., C Intermediate Language or CIL [10] . The possibility to use SPIN to model KUSHIK et al. check C programs based on CIL is described in [11] . On the other hand, one can avoid the translation of C instructions into PROMELA by analyzing the security of the software in other languages, such as Java, and using the corresponding model checker, e.g., JPF [4] .

{'paper_id': '14362127', 'title': 'A SPIN-based approach for detecting vulnerabilities in C programs', 's2_url': 'https://api.semanticscholar.org/CorpusID:14362127', 'source': 'S2ORC'}