1. Home
  2. agenda
  3. BINSEC: Binary-level Semantic Analysis to the Rescue
Contacts
doyen+sem [at] lsv.ens-cachan.fr (Laurent Doyer et Stefan Göller)
Useful links
See the seminary on the LSV's website

BINSEC: Binary-level Semantic Analysis to the Rescue

Several major classes of security analysis have to be performed on raw executable files, such as vulnerability analysis of mobile code or commercial off-the-shelf, deobfuscation or malware inspection.
Le 02/05/2017 : 11:00 à 13:00
Ajouter à mon agenda 2025-05-13 00:05:34 2025-05-13 00:05:34 BINSEC: Binary-level Semantic Analysis to the Rescue Several major classes of security analysis have to be performed on raw executable files, such as vulnerability analysis of mobile code or commercial off-the-shelf, deobfuscation or malware inspection. Pavillon des Jardin - Salle des conférences ENS-PARIS-SACLAY webmaster@ens-paris-saclay.fr Europe/Paris public

These analysis are very challenging, due to the very low-level and intricate nature of binary code, and they are still relatively poorly tooled -- essentially syntactic static analysis (disassembly) which is easy to fool, or dynamic analysis (fuzzing, monitoring) which may miss subtle behaviors. On the other hand, source-level program analysis and formal methods have made tremendous progress in the past decade, and they are now an industrial reality for safety-critical applications.

The open-source BINSEC platform humbly tries to fulfill part of this gap, by providing state-of-the-art binary-level semantic analyses. The platform is built around a concise and generic Intermediate Representation, making it easy to support new architectures and add new analyses. The main analyses so far include a dynamic symbolic execution engine enabling to discover new subtle behaviors in an executable file, and a semantic static analysis engine able to reason about all paths of a portion of the code under analysis.

In this this talk, we will present the benefits & challenges of binary-level formal methods as well as the BINSEC platform and the underlying key technologies, through a few examples taken from deobfuscation and vulnerability analysis.

Speakers : Sébastien Bardin and Richard Bonichon

Print page