Analysis Of Malicious Behavior Based On Model Checking

With the rapid development of the Internet the relationship between people's lives and the Internet is getting closer and closer,and the government has also launched the "Internet Plus" strategy to promote social development.Ensuring that the security of the Internet has become a problem countries and individuals attach great importance to,and the most serious threat to the Internet is malicious code.Due to the rapid increase in the number of malicious code and the continuous updating of malicious code technology,malicious code analysis becomes increasingly difficult.Therefore,the analysis and detection of malicious code can reduce the harm caused by malicious code as much as possible,but also make people's lives more convenient and comfortable.Model Checking is a reasonable and effective method to detect malicious code.Because it is difficult to get the source code of malicious programs for behavioral analysis,the analysis of malicious code is carried out on its executable samples.Analyze the executable samples by disassembly and summarize the behavioral characteristics of malicious codes,and then use the temporal logic to convert the behavioral characteristics into a property formula to be checked to facilitate the detection of the model.Finally,the corresponding pushdown system model is established for the program to be analyzed,and then the model detection is carried out to verify whether the model satisfies the property formula.The above process is the use of model checking for malicious code detection process.This paper studies the problem of malware behavior recognition from the aspects of model establishment,disassembly analysis and the design of malicious code decision algorithm.The main work and innovation of the paper include the following points:1.Analyze malicious binary programs by disassembly and then summarize their common characteristics.In this paper the tool IDA Pro is used to disassemble a large number of malicious binary programs so that the system API function sequence and its parameters with the same characteristics can be extracted.Finally,Stack Computation Tree Predicate Logic is used to describe the API sequences of these common features.2.Binary programs are modeled by pushdown system.This paper uses the disassembly results of Jakstab to establish a pushdown system model for the binary program to be detected,and state transition rules in the model are defined according to the types of instructions in the disassembly result.As the model needs to detect the content of the stack frame,the transition rules need to be described according to whether the instruction changes the contents of the stack frame.3.This paper proposes a model checking algorithm based on the whole content of stack frame to detect malicious code.If the model checking algorithm only considers the top of the stack,it is necessary to ensure that the content of the stack are not affected in the detection process to make the detection result of the algorithm correct.This leads to the fact that the range of the detectable models based on the top of the stack is limited and the algorithm is defective.In order to attack this defect,this paper proposes a model checking algorithm based on the whole content of stack frame.The improved algorithm uses the content of the stack frame to detect the problem caused by the change of the top of the stack,and the detection speed is improved by reducing the size of the model.In this paper,the model detection algorithm based on the whole content of the stack frame has been implemented.The experimental results illustrate the correctness and effectiveness of the algorithm.