binsec

Tech stack & purpose

BINSEC is an open-source binary-level analysis platform designed to improve software security through techniques such as symbolic execution, abstract interpretation, and SMT solving. The project addresses security analysis in the binary code domain, offering tools for both Static Symbolic Execution (SSE) and Backward Bounded Static Symbolic Execution (BBSSE) to solve problems ranging from finding opaque predicates to analyzing constant-time properties and solving reverse-engineering challenges. Built with OCaml and relying on external solvers like Bitwuzla, BINSEC is installable via OPAM and comes with extensive tutorials and examples demonstrating its application to real-world CTF challenges and security analysis tasks.

Community & reference links

• binsec.github.io/
• bitwuzla.github.io/
• github.com/unicorn-engine/unicorn
• polygraph.exe

Languages

Contributors

• 
  Frédéric Recoules30 commits · 8 followers
• Richard Bonichon5 commits
• 
  BINSEC development team1 commits · 43 followers
• 
  Léo1 commits · 0 followers
• 
  rrreeezzz1 commits · 19 followers
• sebastienBardin1 commits
• 
  W0nda1 commits · 2 followers
• Michaël Marcozzi1 commits
• 
  Kate1 commits · 375 followers
• 
  Sheidan1 commits · 4 followers