Research On Recongnition Of Malicious Behavior For Binary Executables Based On Model Checking

Information system security is an important component of national security, malicious code is one of main threats to information system security. Attackers could use malicious codes to achieve network penetration, continuous control, and information theft and other illegal purposes, bringing huge losses to the nations and individuals. On the one hand, as the number of malicious codes grows rapidly, persons who responsible for security are struggling to cope with; on the other hand, malicious codes are continuously integrate code confusion and code distortion to resist detection and analysis of security software, making malicious code analysis and detection more difficult. Therefore, timely and accurate identification of malicious code and its variants is of great significance for protecting information system security and reducing national and personal losses.Model checking is a temporal logic-based formal verification technique, with a high degree of automation, which is widely used in hardware designs, communication protocols and procedure verification and other fields. This thesis applies model checking technique to detect malicious code behavior identification, and focuses on automated extraction methods of behavioral description and characteristics, construction of software behavior model, optimization of detection algorithm, and API anti-obfuscation technology. The main work and innovations of this thesis are as follows:1. An AEDG graph-based automatically extraction method of behavioral characteristics is proposed. The description of behavioral characteristics is inaccurate and the extraction of behavioral characteristics need too much manual intervention. To solve the above problems, this thesis proposes a AEDG graph-based description and automatically extraction method of behavioral characteristics. This method uses dynamic taint analysis technique to track API’s dependencies, construct AEDG graph to accurately describe program behaviors, which overcomes negative effects generated by code obfuscation; and utilizes direction and label features of AEDG graph to optimize minimal contrast subgraph algorithm to reduce the complexity of common subgraph matching and improve the automatically construction efficiency of behavioral characteristics.2. An optimal weight oriented path search method is proposed. The path coverage of dynamic execution based programming model is low, and the program behaviors are incomplete, at the same time, the efficiency of path traversal method based on dynamic symbolic execution, which can easily lead to large-scale problem, is low. To solve the above problems, this thesis presents an optimal weight oriented path search method, which identifies critical API calls through static analysis technique, determine target domains and set the weights, lead program fastly approaching target domains, which can effectively improve the efficiency of covered malicious behaviors.3. A large-scale CTL model checking algorithm is proposed and implemented. Current model detectors can only verify a formula’s satisfiability once a time, unable to meet the fast matching requirements of large-scale behavior characteristics. Based on in-depth study on the CTL marker algorithm, a formula based on common sub-matching algorithm is proposed, which overcome repeated verification problem by identifying common sub-formulas and binding common sub-formulas in states which can meet during the validation process. This method effectively improves the efficiency of the CTL formula verification and the usability of model checking system.4. A static and dynamic API anti-obfuscation method is proposed and implemented anti-aliasing method. The information of API call is an important basis for understanding, describing and modeling program behaviors. To prevent parsing API information from the program, malicious codes commonly use API obfuscation techniques. This thesis studies various API obfuscation and anti-obfuscation methods, focuses on ways to confuse dynamic and encrypted API calls, and proposes a static and dynamic recognition method, which uses decryption routine identification and context automatic acquisition technologies, tracks customized simulator to follow execution, and performs automatically restore of encrypted API functions.5. To verify the feasibility of our research results, this thesis designs and implements a model checking based malicious behavior recognition system, named MBDS. MBDS system uses predicate temporal logic formulas to characterize malicious behaviors, construct predicate tagged Kripke structure according to API call trajectory, and finally validate the model for the formula satisfiability through a large-scale CTL detection algorithm. Experimental results verify the reasonableness, correctness and effectiveness of our framework and algorithms.