Boolean Signatures for Metamorphic Malware

This paper tries to model the code obfuscation as satisfiability problem. In this paper, we try to develop the model to represent the obfuscated code as the satisfiable problem which could be then checked by the SAT solver to check whether at certain instances the model is satisfiable. We provide the notion of converting the SSA format of the instructions to the propositional logic and then by the help of the theorem provers, we tell whether both the code snippets of obfuscated code are same or not. This can be done by converting both codes from their original code to the mathematical signature or relational encoding and then checking their logical equivalence.