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.
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.