bap-taint

BAP Taint Analysis Framework
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library taint
Module Bap_taint . Std . Taint . Tracker . Make

Parameters

Signature

The low-level interface

The low-level interface defines three primitives in terms of which we can express a more convenient high-level interface. It is recommended to get acquainted with these three primitives, to understand how the tracker works, however it is better to use the high level interface, whenever it is possible.

To denote the concrete semantics of these primitives we will use the taint ternary relation T that establishes a relation between a value and an object, e.g., T(v,r,x) is the relation r between the value v and an object x.

Conceptually, the state of the tracker can be seen as a set of such relations. Since tracker operations may affect this set of relations we will denote relations that existed just before an operation with pre, e.g., pre(T(v,r,x) means that before the operation there was the relation T(v,r,x)

attach v r xs establishes the relation r between the value v and every object x in the set of objects xs. All other relations, as well as relations with other values are unaffected.

Post conditions:

  • forall x, x in xs -> T(v,r,x);
  • forall u,s,x, pre(T(u,s,x)) -> T(u,s,x);
  • forall u,s,x, T(v,s,x) -> pre(T(v,s,x)) \// s = r /\\ v = u.

lookup v r returns a set xs of objects that are related with the value v by the relation r. The operation doesn't change the state of the tracker.

Post conditions:

  • x in xs iff T(v,r,x);
  • forall u,s,y, Pre(T(u,s,y)) iff T(u,s,y);

detach v r xs removes all relations of type r between the value v and elements of the set of objects xs. Relations of other types as well as relations between other objects and values are unaffected.

Post conditions:

  • forall x, x in xs -> not (T(v,r,x));
  • forall u,s,y, v <> u \// s <> r, pre(T(u,s,y)) -> T(u,s,y)

High-level interface

The high-level interface provides a set of easy to use (and sometimes more efficient) functions. All these functions could be expressed in terms of the three primitive operations.

new_direct v k introduces a new direct relation between the value v and a freshly created object of the given kind k. The object is returned.

Essentially: attach v direct (add (lookup v k) (Object.create k as r)); r

new_indirect ~addr:v ~len:n k establishes a new indirect relation between a set of addresses, denoted by interval [v,v+n-1], and a freshly created object of specified kind.

val sanitize : Bap_primus.Std.Primus.value -> Rel.t -> Kind.t -> unit Machine.t

Taint.sanitize v r k detaches all objects related to the value v by the relation r that has the given kind k from all values tracked by the taint engine.

In terms of the low-level operations:

               for all v' in objects:
                 detach v' r (filter (has_kind k) (lookup v r))
  • since 2.2.0 the semantics has changed: the sanitization

now affects all values not only v.

objects the set taint objects that are currently tracked.

  • since 2.2.0