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.7.1 from 02/2023.
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.
Some time ago, BINSEC symbolic and relational engines took different paths…
Both grew, but they are meant to grow together! So, we are making it happen, paving the way to let them be one yet again. The first step already gives us a warm feeling.
The Xyntia black-box deobfuscator is now released. Check out its features and how you can use it for research and practical reverse engineering.
We are happy to welcome Dimitri Kokkonis as a new Ph.D. student in the team, to work on fuzzing for advanced vulnerability detection.
Like butchers , we cut and sliced through code. Like Dr. Frankenstein we took what was looking promising.
You know, this kind of experiment is not really popular… Yet the result is so abnormally beautiful that we can not help but share it with you.
We have several open positions to hire postdocs, PhD students and research interns in software security and program analysis. Successful candidates will work in our BINSEC team, on topics like vulnerablity detection and analysis, software reverse engineering and deobfuscation, binary-level formal verification and code protection. All positions are fully-funded.