Binary code analysis for Security

BINSEC is an open-source toolset to help improve software security at the binary level. It relies on cutting-edge research in binary code analysis, at the intersection of formal methods, program analysis, security and software engineering. It is powered up by state-of-the-art techniques such as binary-level formal methods, symbolic execution, abstract interpretation, SMT solving and fuzzing.

BINSEC has been successfully applied in a number of security-related contexts, such as vulnerability finding, (malware) deobfuscation, decompilation, formal verification of assembly code or even binary-level formal verification.

It is developed at the CEA List institute of Université Paris-Saclay in collaboration with Verimag and LORIA.

An overview of some BINSEC features can be found in our tutorial. Further examples are bundled in our Docker image and OPAM package.

We have frequent job openings for postdoc, PhD student and intern positions. Check up the news for ongoing calls or contact us if you believe that you could be a good match.


Manh-Dung has graduated
March 30, 2021

Congratulations to our new Dr. Manh-Dung Nguyen! After leaving the team, Manh-Dung has joined Montimage as a research engineer.

Open doctoral positions for 2021
February 08, 2021

We have multiple doctoral positions open in Software Security through Program Analysis, Formal Methods and Fuzzing at Université Paris-Saclay, CEA List institute, France.

Paper accepted at RTAS'21
February 07, 2021

Proud that our paper “No Crash, No Exploit: Automatic Verification of Embedded Kernels” has been accepted at RTAS’21.

Paper accepted at NDSS'21
January 06, 2021

Proud that our paper “Hunting the Haunter – Efficient Relational Symbolic Execution for Spectre with Haunted RelSE” has been accepted at NDSS’21. Download the tool and benchmarks.

Charles joins the team
January 05, 2021

We are happy to welcome Charles B Mamidisetti as a new PhD student in the team, to work on self-adaptation for adversarial code analysis. Check out his previous TACAS’20 paper on C code verification.


Former Senior

  • Richard Bonichon (to Tweag I/O)

Former Juniors

  • Robin David (PhD, to Quarkslab)
  • Adel Djoudi (PhD, to SystemX)
  • Benjamin Farinier (PhD, to TU Wien)
  • Josselin Feist (PhD, to Trail of Bits)
  • Manh-Dung Nguyen (PhD, to Montimage)
  • Mathilde Ollivier (PhD Student)