Ibisc: salle 05 (RdC) du bâtiment IBGBI, 23 boulevard de France, 91037 Évry - comment y aller
Abstract: Model checking software consists of two steps: model generation and model checking. A model for a high-level programming language is often started as a control flow graph, and sometimes refined iteratively. However, model generation is not easy for a binary code, since binary code is parsed dynamically and has no clear distinction between code and data. Polymorphic virus utilizes this feature for control flow obfuscation, e.g., indirect jumps, self-modification, and exceptions.
We present an on-the-fly pushdown model generation of x86 binaries based on concolic testing, which traces precise control flow against these obfuscation techniques. Its implementation BE-PUM (Binary Emulation for PUshdown Model generation) supports 64 x86 (32bit) instructions and 45 Win32 APIs, which are the most frequently ocurring in VX Heaven.We compare BE-PUM with JakStab and IDA Pro as the statistics and detailed observation on typical obfuscation techniques on real-world malware examples. We also manually compare the source codes and generated models by BE-PUM to confirm their accuracy.
La version présentée est toujours en version béta, et sera finalisée dans le courant de l'année scolaire 2014-2015.