CN105740149B - The software security detection method combined based on Vulnerability Model and semiology analysis - Google Patents

Abstract

The invention relates to a software security detection method based on a combination of a vulnerability model and symbolic execution, which includes: symbolizing the input test data interacted between a program and an external environment; determining symbolic variables for symbolic execution, starting symbolic execution and actual execution, and symbolizing Execute the collection path constraints to obtain the corresponding relationship information between the input and the program running path; according to the path constraints, check whether there is a code area that may trigger a vulnerability, calculate the constraints that can drive the program to the code area, and according to the vulnerability model, Calculate the constraints that may trigger vulnerabilities; call the STP constraint solver to calculate the path constraints that may trigger vulnerabilities, and obtain input data that may trigger vulnerabilities; get new input data and load it into the program under test for a new round of testing. The invention can analyze the program path directly to the dangerous code area at a deep level, generate relatively accurate test input data, trigger the detection of program loopholes, and improve software security.

Description

A Software Security Detection Method Based on the Combination of Vulnerability Model and Symbolic Execution

technical field

The invention relates to the technical field of computer software security testing, in particular to a software security testing method based on the combination of vulnerability model and symbolic execution.

Background technique

Software analysis is the basis for testing security issues such as software vulnerability and software malicious behavior. In order to deal with the security risks brought by software vulnerabilities, researchers have carried out research on software vulnerability analysis techniques. Existing technologies have been able to discover and repair certain vulnerabilities to a certain extent, providing an important support for the safe operation of software. In order to make up for the blindness and low test coverage caused by traditional fuzz testing, many researchers began to apply symbolic execution technology to the vulnerability mining process. Symbolic execution is an information flow analysis technique, which replaces actual input with symbolic input during program execution, symbolizes program variables, continuously collects path constraints through instrumentation during analysis, and generates test cases through constraint solver to Discovering the vulnerability of software may become the core method to solve the problem of software automation testing.

Symbolic execution technology can effectively guide the input data into a certain area of the program to be tested, and then still use the fuzzer to generate multiple samples in a local area for security testing. Although the efficiency of entering a specific area has been greatly improved, it is vulnerable to There are still deficiencies in gender mining.

Contents of the invention

Aiming at the deficiencies in the prior art, the present invention provides a software security detection method based on the combination of vulnerability model and symbolic execution, using the combination of symbolic execution and vulnerability model matching, so that the generated test data can not only quickly reach a certain test program points, and the efficiency of triggering vulnerabilities is higher.

According to the design scheme provided by the present invention, a software security detection method based on the combination of vulnerability model and symbolic execution includes the following steps:

Step 1. Load the input data into the program under test, and the input data drives the execution of the program under test to detect abnormalities;

Step 2. Determine whether the program path coverage requirement is met, and if so, end the test, otherwise, enter step 3;

Step 3. Symbolize the input data, determine the input point and the size of the input data, mark the symbolic variables in the symbolic execution, and define these symbolic variables as a set of original symbolic variables, the symbolic variables include the original symbolic variables and intermediate symbolic variables, intermediate symbols The variable is the symbolic variable represented by the original symbolic variable expression. When the program starts symbolic execution and actual execution, symbolic execution collects path constraints, obtains the corresponding relationship between input points and program running paths, and establishes according to the constraints of program jump points on symbolic variables. Program path constraints;

Step 4. According to the path constraints collected in step 3, check whether there is a code area that triggers the vulnerability in the path, and calculate the constraints that drive the program to the code area according to the path guidance algorithm; at the same time, according to the buffer overflow vulnerability Features, formalize the modeling of security vulnerabilities, and calculate the constraints that trigger the vulnerability by matching the vulnerability model with the path constraints;

Step 5. Call the STP constraint solver to solve the constraints in step 4, obtain new input data for testing, and jump to step 1 for execution.

As mentioned above, the input point in step 3 is the input function call where the program obtains input data, and is also the starting point of symbolic execution.

As mentioned above, after the input data in step 3 is read into the memory, the program enters the execution state. For each instruction to be executed, it is first judged whether symbolic variable operations are involved. If symbolic variable operations are involved, symbolic execution is performed; Execution is sufficient to maintain synchronization with symbolic execution; the program path constraints in step 3 are the equations set up by the original symbolic variables and intermediate symbolic variables.

As mentioned above, the formal modeling of the security vulnerability in the buffer overflow vulnerability in step 4 includes symbolizing the buffer content, symbolizing the buffer size, symbolizing the used length, and establishing a pointer variable The mapping relationship with the buffer, through the symbolic way to detect buffer overflow vulnerability.

As mentioned above, step 4 also includes formal modeling based on the characteristics of the integer overflow vulnerability, abstracting the integer overflow vulnerability into a source-sink problem, and calculating the constraints that trigger the vulnerability.

Beneficial effects of the present invention:

1. The present invention aims at the problem that the current symbolic execution lacks pertinence in the detection of specific security vulnerability types, formalizes the buffer overflow vulnerability and the integer overflow vulnerability, and combines the vulnerability model in the vulnerability detection aspect, Using symbolic execution and constraint solving technology, the generated test data can not only quickly reach a certain program point to be tested, but also trigger vulnerabilities more efficiently, realizing efficient software security vulnerability detection.

2. The present invention comprehensively utilizes the advantages of symbolic execution technology and vulnerability model matching, and generates relatively accurate test input data on the basis of in-depth analysis of program paths, triggers and detects program vulnerabilities, and provides help for improving software security .

Description of drawings:

Fig. 1 is a schematic flow sheet of the present invention;

Fig. 2 is a schematic representation of the symbolic representation of the buffer zone in Embodiment 2;

FIG. 3 is a schematic diagram of the integer overflow vulnerability model in the second embodiment.

detailed description:

The present invention will be described in further detail below in conjunction with the accompanying drawings and technical solutions, and the implementation of the present invention will be described in detail through preferred embodiments, but the implementation of the present invention is not limited thereto.

Embodiment 1, referring to Figure 1, a software security detection method based on the combination of vulnerability model and symbolic execution, comprising the following steps:

Step 1. Load the input data into the program under test, and the input data drives the execution of the program under test to detect abnormalities;

Step 2. Determine whether the program path coverage requirement is met, and if so, end the test, otherwise, enter step 3;

Step 3. Symbolize the input data, determine the input point and the size of the input data, mark the symbolic variables in the symbolic execution, and define these symbolic variables as a set of original symbolic variables, the symbolic variables include the original symbolic variables and intermediate symbolic variables, intermediate symbols The variable is the symbolic variable represented by the original symbolic variable expression. When the program starts symbolic execution and actual execution, symbolic execution collects path constraints, obtains the corresponding relationship between input points and program running paths, and establishes according to the constraints of program jump points on symbolic variables. Program path constraints;

Step 4. According to the path constraints collected in step 3, check whether there is a code area that triggers the vulnerability in the path, and calculate the constraints that drive the program to the code area according to the path guidance algorithm; at the same time, according to the buffer overflow vulnerability Features, formalize the modeling of security vulnerabilities, and calculate the constraints that trigger the vulnerability by matching the vulnerability model with the path constraints;

Step 5. Call the STP constraint solver to solve the constraints in step 4, obtain new input data for testing, and jump to step 1 for execution.

Embodiment 2, referring to Figures 1-3, a software security detection method based on the combination of vulnerability model and symbolic execution, including the following steps:

Step 1. Load the input data into the program under test, and the input data drives the execution of the program under test to detect abnormalities;

Step 2. Determine whether the program path coverage requirement is met, and if so, end the test, otherwise, enter step 3;

Step 3. Symbolize the input data, determine the input point and the size of the input data, mark the symbolic variables in the symbolic execution, and define these symbolic variables as a set of original symbolic variables, the symbolic variables include the original symbolic variables and intermediate symbolic variables, intermediate symbols The variable is the symbolic variable represented by the original symbolic variable expression. When the program starts symbolic execution and actual execution, symbolic execution collects path constraints, obtains the corresponding relationship between input points and program running paths, and establishes according to the constraints of program jump points on symbolic variables. Program path constraints, that is, establish a system of equations based on the original symbolic variables and intermediate symbolic variables, where the input point is the input function call where the program obtains input data, and is also the starting point of symbolic execution. After the input data is read into the memory, the program Enter the execution state, for each instruction to be executed, first judge whether it involves symbolic variable operation, if it involves symbolic variable operation, perform symbolic execution, otherwise it only needs to be actually executed to keep the synchronization with symbolic execution, the actual execution is in Execution in a real environment, as opposed to symbolic execution;

Step 4. According to the path constraints collected in step 3, check whether there is a code area that triggers the vulnerability in the path, and calculate the constraints that drive the program to the code area according to the path guidance algorithm; at the same time, according to the buffer overflow vulnerability Features, formal modeling of security vulnerabilities, through the matching of the vulnerability model and path constraints, calculate the constraints that trigger the vulnerability, the formal modeling of security vulnerabilities in the buffer overflow vulnerability includes the buffer content Symbolization, symbolize the size of the buffer, and symbolize the used length, and establish the mapping relationship between pointer variables and buffers, detect buffer overflow vulnerabilities through symbolic methods, and also include integer overflow vulnerabilities Formal modeling of the characteristics, abstracting the vulnerability of integer overflow into a source-sink problem, and calculating the constraints that trigger the vulnerability;

Step 5. Call the STP constraint solver to solve the constraints in step 4, obtain new input data for testing, and jump to step 1 for execution.

The formal modeling method of the vulnerability model is as follows:

(1) Establishment of buffer overflow vulnerability model

In order to detect buffer overflow defects, in addition to symbolic modeling of the contents of the buffer, a symbolic representation of the size (size) and the used length (length) of the buffer is also provided. In addition, it is necessary to establish a mapping relationship between pointer variables and buffers on the basis of symbolic execution testing technology. In the symbolic mapping relationship δ, a pointer variable is mapped from its specific address addr to a buffer represented by a triple (size, len, C), where size is a symbolic expression, and len represents the buffer variable allocation space C is a symbolic expression, indicating the length used by the buffer variable, that is, the position of the terminal symbol '\0' in the buffer variable, and the value C=C ₁ , C ₂ ,...C _n is A sequence is a symbolic expression of the content stored in the buffer, and the v position before the buffer variable is symbolically modeled to improve the scalability of the system. Express a pointer variable p as a tuple (addr, off), where addr is an unsigned long integer, which is the address of the pointer variable, and off is the distance from the buffer pointed to by p to the buffer A symbolic expression for the offset from the starting position, δ(addr) returns the buffer b(size, len, C) pointed to by p. Figure 2 depicts a schematic diagram of the buffer symbolic representation. In order to detect buffer overflow defects in a symbolic way during the test, it is necessary to define this type of defects.

Table 1 Buffer overflow vulnerability model

buffer zone overflow condition strcpy(p _d ,p _s ) len _s -off _s ＞= size _d -off _d strcat(p _d ,p _s ) len _s -off _s +len _d ＞= size _d *pd:=var off _d ＞ size _d

In the table p _d =(addr _d ,off _d ), b _d =(size _d ,len _d ,C _d )=d(addr _d )≠null, p _s =(addr _s ,off _s ), b _s =( size _s ,len _s ,C _s )=d(addr _d )≠null.

(2) Establishment of integer overflow vulnerability model

Once the results of arithmetic operations and shift operations in the program exceed the expressive capacity of the corresponding type, it will cause "integer overflow". In recent years, there have been more and more attacks on integer overflow vulnerabilities, which have brought many hidden dangers to the security of information systems. The characteristics of integer overflow vulnerability are as follows: 1) Calling tainted data import function: In integer overflow operations, some operands and tainted data have data dependencies, and these tainted data come from external controllable input sources, such as files, network reports, etc. Text, command line parameters, etc., and imported by special API functions, typical tainted data import functions, including read, fread, recv; 2) Improper inspection of tainted data: the program path does not check the range or range check of the number of taints Incomplete; 3) Use overflow results for sensitive operations: Not all integer overflows will cause security issues, only when the overflow results affect the program's control flow, memory allocation, memory access, etc., will further cause other security issues .

Therefore, integer overflow vulnerability can be abstracted as a special source-sink problem, as shown in Figure 3, on the path with integer overflow vulnerability, the tainted data introduction function should be called first, that is, the source node in Figure 3 , common taint sources include fread, recv, etc.; secondly, there are operations on these paths that are sensitive to overflow results, that is, the sink node in Figure 3, such as the memory allocation function malloc, etc.; finally, the constraints on this path are self- Consistent and satisfiable, that is, the path is a feasible path; in addition, the path constraint does not fully check the tainted data, and there are still operations that cause integer overflow on the path. Formal modeling is carried out according to the characteristics of integer overflow vulnerability, and integer overflow vulnerability is abstracted as a source-sink problem to detect integer overflow vulnerability.

Integer overflow vulnerability modeling method:

The abstract model of integer overflow is a six-tuple: <op, oprand, sign, width, range, result>,

1. Meaning:

op: operator, including operations such as addition, subtraction, multiplication, circular shift, and type conversion;

oprand: source operand;

sign: the signed value of the operand oprand, positive or negative or unsigned;

width: Operand width, including 8bit, 16bit, 32bit, 64bit, etc.;

range: the value range of the source operand that triggers the overflow vulnerability;

result: Integer calculation result.

2. To trigger the integer overflow vulnerability, the following constraints must be met at the same time:

1) op∈INT_OP operation belongs to integer operation;

2) oprand _range ∈ TRIGGER_COND source operand value can cause operation error;

3) oprand<-source source operand can be controlled by taint source;

4) The result-sink operation result can affect memory-sensitive access.

sign∈{<source_sign,dest_sign>|source_sign,dest_sign∈SIGN}

width∈{<source_width,dest_width>|source_width,dest_width∈WIDTH}.

The present invention is not limited to the specific embodiments described above, and those skilled in the art can also make various changes accordingly, but any changes that are equivalent or similar to the present invention should be covered within the scope of the claims of the present invention.

Claims (5)

1. A software security detection method based on a combination of vulnerability model and symbolic execution, characterized in that: comprising the following steps: Step 1. Load the input data into the program under test, and the input data drives the execution of the program under test to detect abnormalities; Step 2. Determine whether the program path coverage requirement is met, and if so, end the test, otherwise, enter step 3; Step 3. Symbolize the input data, determine the input point and the size of the input data, mark the symbolic variables in the symbolic execution, and define these symbolic variables as a set of original symbolic variables, the symbolic variables include the original symbolic variables and intermediate symbolic variables, intermediate symbols The variable is the symbolic variable represented by the original symbolic variable expression. When the program starts symbolic execution and actual execution, symbolic execution collects path constraints, obtains the corresponding relationship between input points and program running paths, and establishes according to the constraints of program jump points on symbolic variables. Program path constraints; Step 4. According to the path constraints collected in step 3, check whether there is a code area that triggers the vulnerability in the path, and calculate the constraints that drive the program to the code area according to the path guidance algorithm; at the same time, according to the buffer overflow vulnerability Features, formalize the modeling of security vulnerabilities, and calculate the constraints that trigger the vulnerability by matching the vulnerability model with the path constraints; Step 5. Call the STP constraint solver to solve the constraints in step 4, obtain new input data for testing, and jump to step 1 for execution. 2. The software security detection method based on the combination of vulnerability model and symbolic execution according to claim 1, characterized in that: the input point in step 3 is the input function call place where the program obtains the input data, and at the same time it is the place where the symbolic execution starting point. 3. The software security detection method based on the combination of vulnerability model and symbolic execution according to claim 1, characterized in that: after the input data is read into the memory in step 3, the program enters the execution state, and for each instruction to be executed , first determine whether symbolic variable operations are involved, if symbolic variable operations are involved, perform symbolic execution, otherwise only need to actually execute to keep synchronization with symbolic execution; The program path constraints in step 3 are to establish a system of equations for the original symbolic variables and intermediate symbolic variables. 4. The software security detection method based on the combination of vulnerability model and symbolic execution according to claim 1, characterized in that: the formal modeling of security vulnerability in the buffer overflow vulnerability in step 4 includes the buffer content Symbolize, symbolize the size of the buffer, and symbolize the used length, and establish the mapping relationship between the pointer variable and the buffer, and detect the vulnerability of buffer overflow through symbolization. 5. The software security detection method based on the combination of vulnerability model and symbolic execution according to claim 1, characterized in that: step 4 also includes formal modeling according to the characteristics of integer overflow vulnerability, and the integer overflow vulnerability The vulnerability is abstracted as a source-sink problem, and the constraints that trigger the vulnerability are calculated.