Binary code analysis for security – BINSEC

Software security is one of the very major concern of modern societies, since insecure systems can affect
people, organisations and even states. A few major software-level security analyses must be performed on executable codes, for example
vulnerability detection and malware detection. These essential tasks are poorly addressed by current industrial tools.
Vulnerability detection is mainly based on the art of the security expert,
while industrial (syntactic) malware detectors are very easy to fool with obfuscation and mutation methods.
It may look surprising that such important issues are so poorly tooled,
while formal methods in general and automatic program verification in particular have made tremendous progress in the past decade,
resulting in many impressive industrial applications and demonstrating their strength both in bug finding and safety validation.

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 industry. We target two main applicative domains:
vulnerability analysis and virus detection. Two other closely related applications will also be investigated:
crash analysis and program deobfuscation. 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. Finally, we will develop a common (lightweight) open-source infrastructure to ease the development of binary-level analysers and to allow communication between prototypes through a common formal model.

Binary-level security analysis is a very promising but challenging research field, necessitating theoretical developments as well as substantial implementation and experiments. The consortium can stand upon strong anterior results (including prototypes) and complementary competencess in order to meet the project's very ambitious goals. Potential future impact includes more automated methods and tools for the security industry, more secure digital infrastructures (privacy, e-commerce, e-voting) for the citizen and more effective cyberdefense abilities for the state.