Research And Application Of Symbolic Execution In Software Security

Symbolic execution is an important formal method and software analysis technique,which represents the input of a program as a symbolic value,and represents the value and output of a variable in the program as a symbolic value and constant.Symbolic execution is mainly divided into static symbolic execution and dynamic symbolic execution.It is widely used in many aspects of software security,such as automatic generation of test cases,detection of code security and so on.Software security ensures that the software can continue to run correctly and the software is legally used within the scope of authorization.The field of software security mainly includes reverse engineering,vulnerability mining,authorized encryption,and illegal tampering.Code obfuscation is one of the main techniques against the analyst in reverse engineering.Usually,malware uses the method of code obfuscation to prolong its life cycle.Among them,control flow flattening and opaque predication obfuscation are two common methods of code obfuscation.This thesis has studied these two kinds of obfuscating methods,and has proposed the de-obfuscating algorithm that obfuscates these two kinds of codes at the same time.In addition,as more and more software emerges in people's lives,if a malicious attacker finds loopholes in the software and uses it to peek user privacy,steal personal property,etc.,this will have a serious negative impact on the entire society.Therefore,it is very important to discover the vulnerabilities quickly.This thesis has studied the automated vulnerabilities mining for this problem,and has proposed an automated vulnerabilities mining system that combines fuzzing and symbolic execution.This thesis first proposes a control-flow flattening de-obfuscating algorithm based on dynamic symbolic execution.Compared to the de-obfuscating algorithm based on the abstract syntax tree,the algorithm can directly disambiguate the binary program without the source code,and the restored code is basically consistent with that before the obfuscation.The Coreutils 8.28 software focused on the LS program function of the experiment.The experimental results showed that the average de-obfuscating rate of the algorithm is 93%.Then,an algorithm based on the analysis of path incompatibility of dynamic symbolic execution to de-obfuscate opaque predicate obfuscation is presented.Compared with the static analysis method of data stream analysis,the algorithm has better adaptability to complex operation expressions.In addition,the Coreutils 8.28 software set was used as a test set.The experimental results showed that the average de-obfuscating rate of the algorithm is 81%.Finally,an automatic vulnerability mining system combining fuzzing and symbolic execution is proposed.The system fully utilizes the advantages of fuzzing and symbolic execution.Fuzzing can quickly generate test cases and execute on the cases.Symbolic execution can generate test cases that meet complex inspections.The system combines the advantages of fuzzing and symbolic execution to quickly generate test cases with higher path coverage.At the same time,we use the system to mine the CGC test set.The number of vulnerabilities discovered by the system is 17% more than the number of vulnerabilities discovered by using fuzzing.