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.
Congratulations to our new Dr. Manh-Dung Nguyen! After leaving the team, Manh-Dung has joined Montimage as a research engineer.
We have multiple doctoral positions open in Software Security through Program Analysis, Formal Methods and Fuzzing at Université Paris-Saclay, CEA List institute, France.
Proud that our paper “No Crash, No Exploit: Automatic Verification of Embedded Kernels” has been accepted at RTAS’21.