Séminaire du 3 octobre 2014


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: transparentsModel 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".

Abstract: transparentsNous présenterons les nouveautés de la plateforme CosyVerif pour l'année 2014-2015, ) savoir:

  • Comptes utilisateurs
  • Dépôt de formalismes & modèles
  • Interface Web
  • Éditeur graphique collaboratif de modèles
  • Accès par protocole REST et WebSocket

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