diff --git a/src/plugins/value/domains/taint_domain.ml b/src/plugins/value/domains/taint_domain.ml
index ae137312ca71732afc9d0a420e23fdd51aca29c4..a8eaf9900a164049d70e4a928ecf5b94f39b0efc 100644
--- a/src/plugins/value/domains/taint_domain.ml
+++ b/src/plugins/value/domains/taint_domain.ml
@@ -34,8 +34,11 @@ type taint = {
(* Set of assume statements over a tainted expression. This set is needed to
implement control-dependency: all left-values appearing in statements whose
evaluation depends on at least one of the assume expressions is to be
- tainted. *)
+ tainted. This set is restricted to statements of the current function. *)
assume_stmts: Stmt.Set.t;
+ (* Whether the current call depends on a tainted assume statement: if true,
+ all assignments in the current call should be control tainted. *)
+ dependent_call: bool;
}
let dkey = Value_parameters.register_category "d-taint"
@@ -59,10 +62,12 @@ module LatticeTaint = struct
Format.fprintf fmt
"@[<v 2>Locations (data):@ @[<hov>%a@]@]@\n\
@[<v 2>Locations (control):@ @[<hov>%a@]@]@\n\
- @[<v 2>Assume statements:@ @[<hov>%a@]@]"
+ @[<v 2>Assume statements:@ @[<hov>%a@]@\n\
+ @[<v 2>Dependent call:@ %b@]"
Zone.pretty t.locs_data
Zone.pretty t.locs_control
Stmt.Set.pretty t.assume_stmts
+ t.dependent_call
(* Frama-C "datatype" for type [taint]. *)
include Datatype.Make_with_collections(struct
@@ -75,20 +80,18 @@ module LatticeTaint = struct
let reprs =
[ { locs_data = List.hd Zone.reprs;
locs_control = List.hd Zone.reprs;
- assume_stmts = Stmt.Set.empty; } ]
+ assume_stmts = Stmt.Set.empty;
+ dependent_call = false; } ]
let structural_descr =
Structural_descr.t_abstract (* TODO *)
let compare t1 t2 =
- let c = Zone.compare t1.locs_data t2.locs_data in
- if c <> 0
- then c
- else
- let c = Zone.compare t1.locs_data t2.locs_data in
- if c <> 0
- then c
- else Stmt.Set.compare t1.assume_stmts t2.assume_stmts
+ let (<?>) c (cmp,x,y) = if c = 0 then cmp x y else c in
+ Zone.compare t1.locs_data t2.locs_data
+ <?> (Zone.compare, t1.locs_control, t2.locs_control)
+ <?> (Stmt.Set.compare, t1.assume_stmts, t2.assume_stmts)
+ <?> (Datatype.Bool.compare, t1.dependent_call, t2.dependent_call)
let equal = Datatype.from_compare
@@ -101,7 +104,8 @@ module LatticeTaint = struct
Hashtbl.hash
(Zone.hash t.locs_data,
Zone.hash t.locs_control,
- Stmt.Set.hash t.assume_stmts)
+ Stmt.Set.hash t.assume_stmts,
+ t.dependent_call)
let copy c = c
@@ -112,6 +116,7 @@ module LatticeTaint = struct
locs_data = Zone.bottom;
locs_control = Zone.bottom;
assume_stmts = Stmt.Set.empty;
+ dependent_call = false;
}
(* Top state: everything is tainted. *)
@@ -119,13 +124,15 @@ module LatticeTaint = struct
locs_data = Zone.top;
locs_control = Zone.top;
assume_stmts = Stmt.Set.empty;
+ dependent_call = false;
}
(* Join: keep pointwise over-approximation. *)
let join t1 t2 =
{ locs_data = Zone.join t1.locs_data t2.locs_data;
locs_control = Zone.join t1.locs_control t2.locs_control;
- assume_stmts = Stmt.Set.union t1.assume_stmts t2.assume_stmts; }
+ assume_stmts = Stmt.Set.union t1.assume_stmts t2.assume_stmts;
+ dependent_call = t1.dependent_call || t2.dependent_call; }
(* The memory locations are finite, so the ascending chain property is
already verified. We simply use a join. *)
@@ -136,6 +143,7 @@ module LatticeTaint = struct
locs_data = Zone.narrow t1.locs_data t2.locs_data;
locs_control = Zone.narrow t1.locs_control t2.locs_control;
assume_stmts = Stmt.Set.inter t1.assume_stmts t2.assume_stmts;
+ dependent_call = t1.dependent_call && t2.dependent_call;
}
(* Inclusion testing: pointwise, on locs only. *)
@@ -192,7 +200,7 @@ module TransferTaint = struct
(* Control-dependency: taint the left-value of an assign statement whose
execution depends on the value of a tainted assume statement. *)
let state =
- if Stmt.Set.is_empty state.assume_stmts
+ if not state.dependent_call && Stmt.Set.is_empty state.assume_stmts
then
(* No active tainted assume statement means that there is no
control-dependecy that applies on [lv]. *)
@@ -225,7 +233,7 @@ module TransferTaint = struct
let to_loc = loc_of_lval valuation in
let exp_zone = Value_util.zone_of_expr to_loc exp in
let state =
- if LatticeTaint.intersects state exp_zone
+ if not state.dependent_call && LatticeTaint.intersects state exp_zone
then { state with assume_stmts = Stmt.Set.add stmt state.assume_stmts; }
else state
in
@@ -233,6 +241,10 @@ module TransferTaint = struct
let start_call stmt call _recursion valuation state =
let state = filter_active_tainted_assumes stmt state in
+ let dependent_call =
+ state.dependent_call || not (Stmt.Set.is_empty state.assume_stmts)
+ in
+ let state = { state with assume_stmts = Stmt.Set.empty; dependent_call } in
let state =
(* Add tainted actual parameters in [state]. *)
let to_loc = loc_of_lval valuation in
@@ -251,7 +263,8 @@ module TransferTaint = struct
let finalize_call _stmt _call _recursion ~pre ~post =
(* Recover assume statements from the [pre] abstract state: we assume the
control-dependency does not extended beyond the function scope. *)
- `Value { post with assume_stmts = pre.assume_stmts; }
+ `Value { post with assume_stmts = pre.assume_stmts;
+ dependent_call = pre.dependent_call; }
let show_expr valuation state fmt exp =
let to_loc = loc_of_lval valuation in
@@ -326,14 +339,14 @@ module TaintDomain = struct
let enter_scope _kind _vars state = state
+ let remove_bases bases state =
+ let remove = Zone.filter_base (fun b -> not (Base.Hptset.mem b bases)) in
+ { state with locs_data = remove state.locs_data;
+ locs_control = remove state.locs_control; }
+
let leave_scope _kf vars state =
- let remove_unscoped_bases =
- let bases = Base.Set.of_list (List.map Base.of_varinfo vars) in
- Zone.filter_base (fun b -> not (Base.Set.mem b bases))
- in
- { state with
- locs_data = remove_unscoped_bases state.locs_data;
- locs_control = remove_unscoped_bases state.locs_control; }
+ let bases = Base.Hptset.of_list (List.map Base.of_varinfo vars) in
+ remove_bases bases state
(* Initial state: initializers are singletons, so we store nothing. *)
@@ -342,8 +355,18 @@ module TaintDomain = struct
let initialize_variable_using_type _ _ state = state
- (* Misc. *)
+ (* MemExec cache. *)
let relate _kf _bases _state = Base.SetLattice.empty
+
+ let filter _kf _kind bases state =
+ let filter_base = Zone.filter_base (fun b -> Base.Hptset.mem b bases) in
+ { state with locs_data = filter_base state.locs_data;
+ locs_control = filter_base state.locs_control;
+ assume_stmts = Stmt.Set.empty; }
+
+ let reuse _kf bases ~current_input ~previous_output =
+ let state = remove_bases bases current_input in
+ join state previous_output
end
include TaintDomain