Séminaires
Séminaire du 3 octobre 2014
Lieu
Ibisc: salle 05 (RdC) du bâtiment IBGBI, 23 boulevard de France, 91037 Évry - comment y aller
Programme
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".
Abstract: Nous 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.