Research On Opaque Predicate-Based Obfuscations Against Symbolic Execution

With the booming of mobile internet,the number of applications has been growing up,while more and more reverse-engineering attacks against application programs are arising.Nowadays,symbolic execution-based program analysis can implement automatic deobfuscation attacks,which raise great challenges for current code obfuscations of opaque predicates.To overcome the drawbacks of current opaque predicates,this thesis proposes a new type of opaque predicates that is able to defeat symbolic execution.Based on this type of opaque predicates,an automatic code obfuscation framework is designed and implemented.The main work and contributions of this thesis are as follows:1.A new type of permutation-based opaque predicates is proposed.To defeat symbolic execution-based program analysis,a new method of building opaque predicates based on the injectivity of permutations is proposed.By using permutations over bit-vectors,combined with the compositions of functions,injective equations of permutations are constructed as opaque predicates.This approach only requires the compositions of simple permutations to build bits constraints of high complexity.Using complex constraints,the opaque predicates can effectively increase the solving time of the constraint solvers in symbolic execution engines,which achieves the goal of defeating symbolic execution.Permutation-based opaque predicates overcome the shortcomings of low security in existing types of opaque predicates and have the advantages of simplicity,efficiency,flexibility and concealment.2.A new automatic code obfuscation framework using the permutation-based opaque predicates is designed and implemented.The designed automatic code obfuscation framework only needs the source code of the program as the input and can automatically construct various permutation-based opaque predicates in the program.By program analysis,the obfuscation framework can automatically insert the constructed opaque predicates in the abstract syntax tree of the program,generate bogus codes and finally output the obfuscated program binary code to achieve bogus code obfuscation.The obfuscation framework is able to use other control-flow obfuscations as assistant obfuscations to increase the complexity.Using permutation-based opaque predicates,the obfuscation framework can make the obfuscated program gain resistance against symbolic execution.3.An automatic code obfuscation tool based on LLVM compiler framework is implemented.By this automatic code obfuscation tool,an evaluation is carried out using the Angr symbolic execution engine and several modern SMT solvers to test and evaluate the security and efficiency of 52 different types of opaque predicates that based on compositions of permutations.The evaluation result shows that compared to current opaque predicates,the permutation-based opaque predicate is able to increase the average analysis time of symbolic execution from 3 seconds to more than 500 seconds and increase the solving time of the SMT solvers from a minimum of 0.05 seconds to a maximum of 12 hours or more,while it only gets 5.9% extra run-time overheads and 6.2% extra code-size overheads.This evaluation shows the good security and efficiency of permutation-based opaque predicates.