The global aim of the BINSEC project is to fill part of the gap between formal methods over executable code on one side, and binary-level security analyses currently used in the security in- dustry. We target two main applicative domains: vulnerability analysis and virus detection. Two other closely related applications will also be investigated: crash analysis and program deobfusca- tion. For malware detection, we want to design signature methods robust to mutations and able to overcome obfuscation, especially self-modifying code. For vulnerability analysis, we want to de- velop techniques able to locate potential vulnerabilies in an executable file, and able to distinguish between simple crash bugs and exploitable bugs (exploitability). While a priori distinct, we claim that the different fields addressed in BINSEC share common basic problems and could benefit from similar advances in automated binary code analysis, such as precise recovery of control-flow or data-flow information, or low-level type inference. Finally, we will develop a common (lightweight) open-source infrastructure to ease the development of binary-level analysers and to allow commu- nication between prototypes through a common formal model.
Consortium: CEA LIST, EADS IW, INRIA Rennes Celtique, LORIA Carte, Vérimag PACSS, VUPEN Security
Vérimag people involved: Laurent Mounier,Marie-Laure Potet, Roland Groz (LIG), Josselin Feist
