binsec

Semantic analysis of binary executables
Description

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 verification

BINSEC 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.

Install
binary code analysis symbolic execution deductive program verification formal specification automated theorem prover plugins abstract interpretation dataflow analysis linking disassembly
Documentation binsec.github.io Changelog LGPL-2.1-or-later License Edit opam file
Published
10 Nov 2022
Authors
Maintainers
Sources
binsec-0.6.2.tbz
sha256=11c5335f413cca0773ec8fd7804adeb2ae960fff834c35f7eb510c43dad51092 sha512=7d706de9c98a97017ef07d317552917f76ff771b95d1cf76ad6986558244a822ea72bdc89981689fb9b63837468ef378f30ff659a7e2578d0285ce5f037b6022
Dependencies
odoc with-doc
qcheck with-test & >= "0.7"
ounit2 with-test & >= "2"
toml >= "6"
dune-site
zarith >= "1.4"
ocamlgraph >= "1.8.5"
menhir build & >= "20181113"
ocaml >= "4.09" & < "5"
dune >= "3.0"
Reverse Dependencies
Conflicts
bitwuzla < "1.0.1"
llvm >= "13.0.0"
llvm < "6.0.0"