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 tutorials. Further examples are bundled in our Docker image and OPAM package.
Current release is version 0.10 from 02/2025.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.
Two years ago, we reimplemented and optimized the symbolic relational engine of BINSEC, as the checkct plugin. To keep it from becoming routine and renew the sparkle, today we spring with the brand-old secret-erasure checker, together with a bunch of new improvements!
Work less, work better. Experiments tend to show it is a good way to increase the productivity. So, no shiny new feature today, but we shipped some improvements that may speed up the symbolic exploration!
We have one open position to work for 4-6 months as an intern on understanding and detecting complex software vulnerabilities.
The PreCA precondition inference framework is now released. Check out its features and how you can use it for research and code understanding.
We have one open position to work for 3 years as a PhD student on artful vulnerability detection with fuzzing.