binsecversion Documentation on ocaml.org
Semantic analysis of binary executables
BINSEC aims at developing an open-source platform filling the gap between formal methods over executable code and binary-level security analyses currently used in the security industry.
The project targets the following applicative domains:
vulnerability analyses
malware comprehension
code protection
binary-level verificationBINSEC is developed at CEA List in scientfic collaboration with Verimag and LORIA.
An overview of some BINSEC features can be found in our SSPREW'17 tutorial.
| Tags | binary code analysis symbolic execution deductive program verification formal specification automated theorem prover plugins abstract interpretation dataflow analysis linking disassembly |
|---|---|
| Authors | Adel Djoudi, Benoit Boero, Benjamin Farinier, Chakib Foulani, Dorian Lesbre, Frédéric Recoules, Guillaume Girol, Josselin Feist, Lesly-Ann Daniel, Mahmudul Faisal Al Ameen, Manh-Dung Nguyen, Mathéo Vergnolle, Matthieu Lemerre, Nicolas Bellec, Olivier Nicole, Richard Bonichon, Robin David, Sébastien Bardin, Soline Ducousso, Ta Thanh Dinh, Yaëlle Vinçont and Yanis Sellami |
| License | LGPL-2.1-or-later |
| Published | |
| Homepage | https://binsec.github.io |
| Issue Tracker | mailto:binsec@saxifrage.saclay.cea.fr |
| Maintainer | BINSEC <binsec@saxifrage.saclay.cea.fr> |
| Available | os-family != "windows" |
| Dependencies |
|
| Optional dependencies | |
| Conflicts |
|
| Source [http] | https://github.com/binsec/binsec/releases/download/0.11.1/binsec-0.11.1.tbz sha256=bb48234a4b60a872015a88282df4873f01dcc984753d49ad2583d49c1ae7d705 sha512=e8aa47a736b83bfd47d5b5e96d0988859b4873ad4a112fee7cd21d02bc72ecec61b7de610a959e38d2f2f5eef8082a2c100c201e5eae5ae3a880c747dce6ae63 |
| Edit | https://github.com/ocaml/opam-repository/tree/master/packages/binsec/binsec.0.11.1/opam |
No package is dependent
