LSV Seminar
The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
Past Seminars
BINSEC: Binary-level Semantic Analysis to the Rescue
- Date
- Tuesday, May 02 2017 at 11:00AM
- Place
- Salle de Conférence (Pavillon des Jardins)
- Speaker
- Sébastien Bardin (CEA, Paris-Saclay)
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. 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.