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.
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.
What a follow up,rising new opportunities! The legacy symbolic engine is overwhelmed while the new one opens with the greatest number. We are glad to announce BINSEC is now supporting plugin extensions.
We have a fully funded open position for a 3 years PhD student, to work on security-oriented binary-level symbolic execution.