Tracker.Makemodule Machine : Bap_primus.Std.Primus.Machine.SThe 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)
val attach :
Bap_primus.Std.Primus.value ->
Rel.t ->
Object.Set.t ->
unit Machine.tattach 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:
val lookup : Bap_primus.Std.Primus.value -> Rel.t -> Object.Set.t Machine.tlookup 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:
val detach :
Bap_primus.Std.Primus.value ->
Rel.t ->
Object.Set.t ->
unit Machine.tdetach 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:
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.
val new_direct : Bap_primus.Std.Primus.value -> Kind.t -> Object.t Machine.tnew_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
val new_indirect :
addr:Bap_primus.Std.Primus.value ->
len:Bap_primus.Std.Primus.value ->
Kind.t ->
Object.t Machine.tnew_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.tTaint.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))now affects all values not only v.
val objects : Core_kernel.Set.M(Object).t Machine.tobjects the set taint objects that are currently tracked.