package binsec

  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 (21)

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.2.tbz
sha256=b758f3428b62a03103403196af99a5bb7df77a35afbcc5ce2d2b1fbe6d2ab36b
sha512=afa4fdf09ae0c2ab02530d674f9f2c1473d156e0438b4cb9c262ffea2d98c448251de55cd6fb176562edaae3897aeabe873ffa1ad47f861c75e1943792d90261

doc/binsec.symbolic/Binsec_symbolic/State/index.html

Module Binsec_symbolic.StateSource

Sourceexception Unknown

Raised by reasoning functions (S.check_sat and ENUMERATION.next) when no solution has been found within the resource budget (e.g. SetSMTSolverTimeout).

Sourceexception Undefined of Binsec_kernel.Dba.Var.t

Raised by the DATA.lookup function when the variable is not defined.

Sourceexception Undeclared of string option

Raised by the DATA.read, DATA.select, S.write and S.store functions when the memory array is not defined.

Sourceexception Non_mergeable

Raised by the S.merge function the two states can not be merged.

Extends the booleans with Unknown.

A size in bit.

Sourceand 'a operator = 'a Binsec_kernel.Term.operator =
  1. | Not : unary operator
  2. | Sext : size -> unary operator
  3. | Uext : size -> unary operator
  4. | Restrict : int interval -> unary operator
  5. | Plus : binary operator
  6. | Minus : _ operator
  7. | Mul : binary operator
  8. | Udiv : binary operator
  9. | Urem : binary operator
  10. | Sdiv : binary operator
  11. | Srem : binary operator
  12. | Or : binary operator
  13. | And : binary operator
  14. | Xor : binary operator
  15. | Concat : binary operator
  16. | Lsl : binary operator
  17. | Lsr : binary operator
  18. | Asr : binary operator
  19. | Rol : binary operator
  20. | Ror : binary operator
  21. | Eq : binary operator
  22. | Diff : binary operator
  23. | Ule : binary operator
  24. | Ult : binary operator
  25. | Uge : binary operator
  26. | Ugt : binary operator
  27. | Sle : binary operator
  28. | Slt : binary operator
  29. | Sge : binary operator
  30. | Sgt : binary operator
Sourcemodule type UID = sig ... end
Sourcemodule type VALUE = sig ... end
Sourcemodule type MODEL = sig ... end
Sourcemodule type ENUMERATION = sig ... end
Sourcemodule type DATA = sig ... end
Sourcetype ('value, 'state, 'cookie, 'a) feature = ..

A feature is a state functionality that is not part of the common interface.

A value of type 'a can be queried with the function S.more. It can be anything, including a function, and may depend on the type parameters 'value, 'state and 'cookie.

For instance, the function S.lookup can be expressed as a !type-feature as follows. type ('value, 'state, 'cookie, 'a) feature += | Lookup : ('value, 'state, 'cookie, Dba.Var.t -> 'state -> 'value) feature

Sourcemodule type S = sig ... end
Sourcetype _ value_kind = ..

A witness of the value type used by the state (S.more ValueKind).

Sourcetype feature +=
  1. | ValueKind : ('value, 'state, 'cookie, 'value value_kind) feature
  2. | SetSMTSolver : ('value, 'state, 'cookie, 'cookie -> Binsec_symbolic.Smtlib.Solver.backend -> unit) feature
  3. | SetSMTSolverTimeout : ('value, 'state, 'cookie, 'cookie -> float -> unit) feature
  4. | SetSMTDumpDir : ('value, 'state, 'cookie, 'cookie -> string -> unit) feature
  5. | SetSMTSolverMultiChecks : ('value, 'state, 'cookie, 'cookie -> bool -> unit) feature
  6. | ToFormula : ('value, 'state, 'cookie, 'state -> Binsec_symbolic.Smtlib.Formula.formula) feature