Ibisc: salle 05 (RdC) du bâtiment IBGBI, 23 boulevard de France, 91037 Évry - comment y aller
14h00-15h00: Mizuhito Ogawa - JAIST/Kanazawa, "Pushdown model generation for binary code",
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.
15h00-15h30 : Alban LInard - LSV, ENS de Cachan et Inria, "CosyVerif, nouveautés pour 2014/2015".
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.
15h30-16h00: pause café
16h00-16h30: vie du groupe