package binsec

All checked builds pass
  1. Overview
  2. Docs
Semantic analysis of binary executables

Install 

dune-project
 Dependency

binsec.github.io Readme Changelog LGPL-2.1-or-later License Edit opam file Versions (22)

Authors

  1. A
    Adel Djoudi
  2. B
    Benoit Boero
  3. B
    Benjamin Farinier
  4. C
    Chakib Foulani
  5. D
    Dorian Lesbre
  6. F
    Frédéric Recoules
  7. G
    Guillaume Girol
  8. J
    Josselin Feist
  9. L
    Lesly-Ann Daniel
  10. M
    Mahmudul Faisal Al Ameen
  11. M
    Manh-Dung Nguyen
  12. M
    Mathéo Vergnolle
  13. M
    Matthieu Lemerre
  14. N
    Nicolas Bellec
  15. O
    Olivier Nicole
  16. R
    Richard Bonichon
  17. R
    Robin David
  18. S
    Sébastien Bardin
  19. S
    Soline Ducousso
  20. T
    Ta Thanh Dinh
  21. Y
    Yaëlle Vinçont
  22. Y
    Yanis Sellami

Maintainers

  1. B
    BINSEC <binsec@saxifrage.saclay.cea.fr>

Sources

binsec-0.11.3.tbz
sha256=93f6fe439d486b166062ef6dd92c4ce3aa0947b5e18b1c3aa7de2fc3003aa6d9
sha512=98feb2b0a3f0a33fe912e9885311dd1c051768c707437f8ef038a8489fec019960142b588c6973eb8f726a14d9b2a1b4c765d915539911cb9f6ed6da9f1e51f2

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.

Tags

binary code analysis symbolic execution deductive program verification formal specification automated theorem prover plugins abstract interpretation dataflow analysis linking disassembly

Added to opam-repository:

README

BINSEC License: LGPL

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.

Website

More information about BINSEC is available at: https://binsec.github.io/

Getting started

See install instructions. Then, have a look at user documentation for command examples.

Contributing

Found a bug or want to make a suggestion, check how to contribute improving BINSEC.

Dependencies (9)

  1. mula
  2. toml >= "6"
  3. dypgen
  4. dune-site
  5. zarith >= "1.13"
  6. ocamlgraph >= "1.8.5"
  7. menhir build & >= "20181113"
  8. ocaml >= "4.14"
  9. dune >= "3.18"

Dev Dependencies (6)

  1. odoc with-doc
  2. ocamlformat with-dev-setup & = "0.28.1"
  3. unionFind with-test
  4. ppx_inline_test with-test
  5. qcheck with-test & >= "0.90"
  6. ounit2 with-test & >= "2"

Used by

None

Conflicts (5)

  1. unisim_archisec < "0.0.6"
  2. z3 < "4.8.13"
  3. bitwuzla-cxx < "0.4"
  4. bitwuzla < "1.0.6"
  5. llvm < "6.0.0" | >= "16.0.0"

Build status

Results of building binsec with each compiler on check.ci.ocaml.org, run of against opam-repository 8a77e58. All results for this package.

Each result links to its build log. To keep crawlers from overloading the site, build logs require a GitHub sign-in (see ocurrent/opam-health-check). On your first log, GitHub asks you to “Authorize opam-health-check”, the OCurrent app that runs these checks; it sees only your public profile, not your repositories. The sign-in lasts 30 days.

Version OCaml 4.11 OCaml 4.14 OCaml 5.2 OCaml 5.4 OCaml 5.5
0.11.3 (this version) n/a good good good good
0.10.1 good good good n/a n/a
  • good Package successfully built
  • partial One of the dependencies failed to build
  • bad Package failed to build
  • n/a Package is not available in this environment
  • internal Internal failure