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_sse_stake/Binsec_sse_stake/Builtin/argument-2-E/Path/State/index.html

Module Path.State

type t = state

A symbolic state.

module Value : Binsec_symbolic.State.VALUE with type id = Uid.t with type t = value
include Binsec_symbolic.State.DATA with type t := t and type value := Value.t
val lookup : Binsec_kernel.Dba.Var.t -> t -> Value.t

lookup var s returns the value assigned to var in s.

  • raises Undefined

    if var is not in s.

val read : addr:Value.t -> int -> Binsec_kernel.Machine.endianness -> t -> Value.t * t

read ~addr len d s returns len bytes of the value stored at address addr in the main memory array @, together with the updated state s. The byte order is determined by the endianness d.

  • raises Undeclared

    None if there is no main memory in s (see S.declare).

val select : string -> addr:Value.t -> int -> Binsec_kernel.Machine.endianness -> t -> Value.t * t

select m ~addr len d s returns len bytes of the value stored at address addr in the memory array m, together with the updated state s. The byte order is determined by the endianness d.

  • raises Undeclared

    Some m if m is not in s (see S.declare).

val empty : unit -> t

empty creates an empty state.

val assign : Binsec_kernel.Dba.Var.t -> Value.t -> t -> t

assign var v s returns a copy of s with the value v assigned to the variable var.

val declare : array:string option -> int -> t -> t

declare ~array idx s returns a copy of s where array is a fresh mapping between addresses of idx bits to (first-order) constant.

The None represents the main memory @ (e.g. the RAM). The functions read and write operate on @.

The Some name represents a named array. The functions select and store operate on name.

val write : addr:Value.t -> Value.t -> Binsec_kernel.Machine.endianness -> t -> t

write ~addr v d s returns a copy of s where the value v is written at the address addr in the main memory. The byte order is determined by the endianness d.

  • raises Undeclared

    None if there is no main memory @ in s (see declare).

val store : string -> addr:Value.t -> Value.t -> Binsec_kernel.Machine.endianness -> t -> t

store m ~addr v s returns a copy of s where the value v is stored at the address addr in the memory array m. The byte order is determined by the endianness d.

  • raises Undeclared

    Some m if m is not in s (see declare).

val memcpy : string option -> addr:Value.t -> int -> Binsec_kernel.Loader_types.buffer -> t -> t

memcpy m ~addr len content s returns a copy of s where len bytes from the zero extended buffer content are copied to the memory array m at the address addr.

  • raises Undeclared

    m is not in s (see declare).

val merge : t -> t -> t

merge t1 t2 returns a new state with the values of both t1 and t2.

val assume : Value.t -> t -> t option

assume v s returns the a copy of the state s for which the boolean condition v has been added to the path predicate.

Returns None if the state s can infer that v always evaluates to false.

val predicate : t -> Value.t list

predicate s returns the state predicate as a list of value.

val is_symbolic : Value.t -> t -> bool

is_symbolic v s checks if the value v may depend on symbolic values.

is_zero v s checks if v may depend on symbolic values.

It returns True when the state implies v is false and False when the state implies v is true.

Otherwise, it returns !constructor-Unknown, that means that v syntactically depends on a symbolic value.

module Model : Binsec_symbolic.State.MODEL with type value := Value.t with type t = model
val check_sat : Cookie.t -> t -> Model.t option

check_sat c s returns a model that satisfies the predicate of s, using the configuration stored in the cookie c.

  • raises Unknown

    when no solution is found within the current resource budget (see SetSMTSolverTimeout).

val enumerate : Cookie.t -> Value.t -> ?except:Binsec_kernel.Bitvector.t list -> t -> Enumeration.t

enumerate c v ~except s returns a new enumeration for the value v, using the configuration stored in the cookie c.

The enumeration will not contain any Binsec_kernel.Bitvector present in except.

val print_smtlib : ?slice:(Value.t * string) list -> Format.formatter -> t -> unit

print_smtlib ~slice f s outputs the predicate of s in the SMTlib format in the formatter f.

If slice is given, it outputs the current mapping between values and name. Otherwise, it outputs the full mapping (variables and arrays) of s.

val pp : Format.formatter -> t -> unit

pp f s outputs the state s in the formatter f.

val more : (Value.t, t, Cookie.t, 'a) Binsec_symbolic.State.feature -> 'a option

more feature returns Some a value of type 'a; or None if the current implementation does not support the queried feature.