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.

Current release is version 0.3.0 from 12/2019 (next release expected by 12/2021).

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.


Best PhD award for Benjamin
June 16, 2021

Benjamin Farinier, a former PhD student in the team and now a postdoc at TUVienna, has won the GDR GPL 2020 best PhD award for his work on Decision Procedures for Vulnerability Analysis.

Paper accepted at CAV'21
June 02, 2021

Proud that our paper “Not All Bugs Are Created Equal, But Robust Reachability Can Tell The Difference” has been accepted at CAV’21.

Paper accepted at CCS'21
May 31, 2021

Proud that our paper “Search-based Local Blackbox Deobfuscation: Understand, Improve and Mitigate” has been accepted at CCS’21.

Paper awards at ICSE and RTAS
May 31, 2021

We are honoured and happy to have received a distinguished paper award at ICSE’21 and the best paper award at RTAS’21.

Bernard joins the team
May 03, 2021

We are happy to welcome Bernard Nongpoh as a new postdoc in the team, to work on fuzzing for vulnerability detection. Check out his great Ph.D. work on approximate computing.


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)