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

Authors

  1. A
    Adel Djoudi
  2. B
    Benjamin Farinier
  3. C
    Chakib Foulani
  4. D
    Dorian Lesbre
  5. F
    Frédéric Recoules
  6. G
    Guillaume Girol
  7. J
    Josselin Feist
  8. L
    Lesly-Ann Daniel
  9. M
    Mahmudul Faisal Al Ameen
  10. M
    Manh-Dung Nguyen
  11. M
    Mathéo Vergnolle
  12. M
    Mathilde Ollivier
  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.0.tbz
sha256=4cf70a0367fef6f33ee3165f05255914513ea0539b94ddfef0bd46fc9b42fa8a
sha512=cd67a5b7617f661a7786bef0c828ee55307cef5260dfecbb700a618be795d81b1ac49fc1a18c4904fd2eb8a182dc862b0159093028651e78e7dc743f5babf9e3

doc/binsec.smtlib/Binsec_smtlib/Formula/Model/index.html

Module Formula.Model

Internal model representation

Model types

type t
type identifier = string
val empty : t

Constructors

Empty model.

val extract : Binsec_smtlib__.Smtlib.model -> t

extract model extracts relevant information in SMT-LIB model concerning registers and memory values. This function takes into account the various "model dialects" spoken by:

  • Z3;
  • CVC4;
  • Boolector
val extract_value : Binsec_smtlib__.Smtlib.constant -> Binsec_base.Bitvector.t

extract_value value extracts the value returned by (get-value) the same * way extract returns the model returned by (get-model). * This function currently only supports bitvectors

val yices_extract : string -> t

yices_extract s extracts the same information as extract but for a yices-smt2 produced model yices-smt2 models use another syntax and are parsed on their own s is expected to be the raw string of the model and not, for example, a filename

Create from scratch

val create : ?len:int -> unit -> t
val add_var : t -> string -> Binsec_base.Bitvector.t -> unit
val add_memcell : t -> Binsec_base.Bitvector.t -> Binsec_base.Bitvector.t -> unit
val add_memory_term : t -> (Binsec_smtlib__.Smtlib.term * Binsec_smtlib__.Smtlib.term) list -> unit

Pretty-printer

val pp : Format.formatter -> t -> unit
val pp_with_sections : (Binsec_base.Virtual_address.t -> string option) -> Format.formatter -> t -> unit

Accessors

val find_variable : t -> identifier -> Binsec_base.Bitvector.t option

find_register model name finds the bitvector value of register name in the model

val find_address_contents : t -> address -> Binsec_base.Bitvector.t option

find_address_contents model addr find the (byte-sized) value of address addr from the model.

val find_address_content : t -> address -> Binsec_base.Size.Byte.t -> Binsec_base.Machine.endianness -> Binsec_base.Bitvector.t option

Not yet implemented

val variables : t -> identifier list

get_register model gets the list of registers of this model

val memory_addresses : t -> address list

get_register model gets the list of addresses with specific values of this model

val memory_bindings : t -> (address * Binsec_base.Bitvector.t) array

get_register model gets the list of pair address/value of this model

val is_memory_set : t -> address -> bool

is_memory_set model address checks if the given address is present in the memory of this model

val filter : ?keep_default:bool -> addr_p:(Binsec_base.Bitvector.t -> bool) -> var_p:(string -> bool) -> t -> t

filter ?keep_default ~addr_p ~var_p model creates a new model m with the following properties:

  • m has the same default value for memory adresses than model if keep_default is true (default is false)
  • m keeps from model all addresses verifying the predicate addr_p and all the variable names verifying var_p