The global aim of the BINSEC project is to fill part of the gap between formal methods over executable code and binary-level security analyses currently used in the security industry.
We target two main applicative domains:
Two other closely related applications will also be investigated:
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 develop 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 analyzers and to allow communication between prototypes through a common formal model.