using taint kind in taint sink specifications

Reviewed By: jeremydubreil

Differential Revision: D3288789

fbshipit-source-id: 952a7a2

infer/src/IR/Sil.re

@@ -693,7 +693,7 @@ and attribute =
   /** undefined value obtained by calling the given procedure, plus its return value annots */
   | Aundef of Procname.t item_annotation Location.t path_pos
   | Ataint of taint_info
-  | Auntaint
+  | Auntaint of taint_info
   | Alocked
   | Aunlocked
   /** value appeared in second argument of division at given path position */
@@ -1276,7 +1276,7 @@ let attribute_to_category att =>
   | Aresource _
   | Adangling _ => ACresource
   | Ataint _
-  | Auntaint => ACtaint
+  | Auntaint _ => ACtaint
   | Alocked
   | Aunlocked => AClock
   | Aautorelease => ACautorelease
@@ -1539,9 +1539,9 @@ and attribute_compare (att1: attribute) (att2: attribute) :int =>
   | (Ataint ti1, Ataint ti2) => taint_info_compare ti1 ti2
   | (Ataint _, _) => (-1)
   | (_, Ataint _) => 1
-  | (Auntaint, Auntaint) => 0
+  | (Auntaint ti1, Auntaint ti2) => taint_info_compare ti1 ti2
-  | (Auntaint, _) => (-1)
+  | (Auntaint _, _) => (-1)
-  | (_, Auntaint) => 1
+  | (_, Auntaint _) => 1
   | (Alocked, Alocked) => 0
   | (Alocked, _) => (-1)
   | (_, Alocked) => 1
@@ -2236,7 +2236,7 @@ and attribute_to_string pe =>
       ":" ^
       string_of_int loc.Location.line
   | Ataint {taint_source} => "TAINTED[" ^ Procname.to_string taint_source ^ "]"
-  | Auntaint => "UNTAINTED"
+  | Auntaint _ => "UNTAINTED"
   | Alocked => "LOCKED"
   | Aunlocked => "UNLOCKED"
   | Adiv0 (_, _) => "DIV0"

infer/src/IR/Sil.rei

@@ -266,7 +266,7 @@ and attribute =
   /** undefined value obtained by calling the given procedure */
   | Aundef of Procname.t item_annotation Location.t path_pos
   | Ataint of taint_info
-  | Auntaint
+  | Auntaint of taint_info
   | Alocked
   | Aunlocked
   /** value appeared in second argument of division at given path position */

infer/src/backend/interproc.ml

@@ -541,6 +541,19 @@ let forward_tabulate tenv wl =
       let summary = Specs.get_summary_unsafe "forward_tabulate" proc_name in
       let timestamp = Specs.get_timestamp summary in
       F.sprintf "[%s:%d] %s" phase_string timestamp (Procname.to_string proc_name) in
+    let add_taint_attrs proc_name prop =
+      match Taint.tainted_params proc_name with
+      | [] -> prop
+      | tainted_param_nums ->
+          let formal_params' =
+            IList.map (fun (p, _) -> Pvar.mk p proc_name) formal_params in
+          Taint.get_params_to_taint tainted_param_nums formal_params'
+          |> IList.fold_left
+            (fun prop_acc (param, taint_kind) ->
+               let attr =
+                 Sil.Ataint { taint_source = proc_name; taint_kind; } in
+               Taint.add_tainting_attribute attr param prop_acc)
+            prop in
     let doit () =
       handled_some_exception := false;
       check_prop_size pathset_todo;
@@ -566,9 +579,9 @@ let forward_tabulate tenv wl =
           exe_iter
             (fun prop path cnt num_paths ->
                try
-                 let prop = if Config.taint_analysis then
+                 let prop =
-                     let tainted_params = Taint.tainted_params proc_name in
+                   if Config.taint_analysis
-                     Tabulation.add_param_taint proc_name formal_params prop tainted_params
+                   then add_taint_attrs proc_name prop
                    else prop in
                  L.d_strln
                    ("Processing prop " ^ string_of_int cnt ^ "/" ^ string_of_int num_paths);

infer/src/backend/modelBuiltins.ml

@@ -380,7 +380,7 @@ let execute___check_untainted
   | [(lexp, _)], _ ->
       let caller_pname = Cfg.Procdesc.get_proc_name pdesc in
       let n_lexp, prop = check_arith_norm_exp caller_pname lexp prop_ in
-      [(check_untainted n_lexp caller_pname callee_pname prop, path)]
+      [(check_untainted n_lexp Sil.Tk_unknown caller_pname callee_pname prop, path)]
   | _ -> raise (Exceptions.Wrong_argument_number __POS__)
 
 (** take a pointer to a struct, and return the value of a hidden field in the struct *)
@@ -644,6 +644,18 @@ let execute___set_taint_attribute
       (* note: we can also get this if [taint_kind] is not a string literal *)
       raise (Exceptions.Wrong_argument_number __POS__)
 
+(** Set the attibute of the value as tainted *)
+let execute___set_untaint_attribute
+    ({ Builtin.pdesc; args; prop_; path; })
+  : Builtin.ret_typ =
+  match args with
+  | (exp, _) :: [] ->
+      let taint_source = Cfg.Procdesc.get_proc_name pdesc in
+      let taint_kind = Sil.Tk_unknown in (* TODO: change builtin to specify taint kind *)
+      set_attr pdesc prop_ path exp (Sil.Auntaint { Sil.taint_source; taint_kind})
+  | _ ->
+      raise (Exceptions.Wrong_argument_number __POS__)
+
 let execute___objc_cast { Builtin.pdesc; prop_; path; ret_ids; args; }
   : Builtin.ret_typ =
   match args with
@@ -1070,7 +1082,7 @@ let _ = Builtin.register
     "__set_taint_attribute" execute___set_taint_attribute
 let _ = Builtin.register
     (* set the attribute of the parameter as untainted *)
-    "__set_untaint_attribute" (execute___set_attr Sil.Auntaint)
+    "__set_untaint_attribute" execute___set_untaint_attribute
 let __set_locked_attribute = Builtin.register
     (* set the attribute of the parameter as locked *)
     "__set_locked_attribute" execute___set_locked_attribute

infer/src/backend/symExec.ml

@@ -1358,24 +1358,25 @@ and add_constraints_on_actuals_by_ref tenv prop actuals_by_ref callee_pname call
       replace_actual_hpred actual actual_pt_havocd_var prop in
     IList.fold_left (fun p var -> havoc_actual_by_ref var p) prop actuals_by_ref
 
-and check_untainted exp caller_pname callee_pname prop =
+and check_untainted exp taint_kind caller_pname callee_pname prop =
   match Prop.get_taint_attribute prop exp with
-  | Some (Sil.Ataint source_pname) ->
+  | Some (Sil.Ataint taint_info) ->
       let err_desc =
         Errdesc.explain_tainted_value_reaching_sensitive_function
           prop
           exp
-          source_pname
+          taint_info
           callee_pname
           (State.get_loc ()) in
       let exn =
         Exceptions.Tainted_value_reaching_sensitive_function
           (err_desc, __POS__) in
       Reporting.log_warning caller_pname exn;
-      Prop.add_or_replace_exp_attribute prop exp (Sil.Auntaint)
+      Prop.add_or_replace_exp_attribute prop exp (Sil.Auntaint taint_info)
   | _ ->
       if !Config.footprint then
-        let untaint_attr = Sil.Const (Sil.Cattribute (Sil.Auntaint)) in
+        let taint_info = { Sil.taint_source = callee_pname; taint_kind; } in
+        let untaint_attr = Sil.Const (Sil.Cattribute (Sil.Auntaint taint_info)) in
         (* add untained(n_lexp) to the footprint *)
         Prop.conjoin_neq ~footprint:true exp untaint_attr prop
       else prop
@@ -1400,9 +1401,10 @@ and unknown_or_scan_call ~is_scan ret_type_option ret_annots
       | param_nums ->
           let check_taint_if_nums_match (prop_acc, param_num) (actual_exp, _actual_typ) =
             let prop_acc' =
-              if IList.exists (fun num -> num = param_num) param_nums
+              try
-              then check_untainted actual_exp caller_pname callee_pname prop_acc
+                let _, taint_kind = IList.find (fun (num, _) -> num = param_num) param_nums in
-              else prop_acc in
+                check_untainted actual_exp taint_kind caller_pname callee_pname prop_acc
+              with Not_found -> prop_acc in
             prop_acc', param_num + 1 in
           IList.fold_left
             check_taint_if_nums_match

infer/src/backend/symExec.mli

@@ -31,7 +31,7 @@ val unknown_or_scan_call : is_scan:bool -> Sil.typ option -> Sil.item_annotation
 val check_variadic_sentinel : ?fails_on_nil:bool -> int -> int * int -> Builtin.t
 
 val check_untainted :
-  Sil.exp -> Procname.t -> Procname.t -> Prop.normal Prop.t -> Prop.normal Prop.t
+  Sil.exp -> Sil.taint_kind -> Procname.t -> Procname.t -> Prop.normal Prop.t -> Prop.normal Prop.t
 
 (** Check for arithmetic problems and normalize an expression. *)
 val check_arith_norm_exp :

infer/src/backend/tabulation.ml

@@ -819,21 +819,19 @@ let add_tainting_att_param_list prop param_nums formal_params att =
                " to be set as tainted/untainted ");
     prop
 
-(* Set Ataint attribute to list of parameters in a prop *)
+(* Add Auntaint attribute to a callee_pname precondition *)
-let add_param_taint proc_name formal_params prop param_nums =
-  let formal_params' = IList.map
-      (fun (p, _) -> Pvar.mk p proc_name) formal_params in
-  let taint_info = { Sil.taint_source = proc_name; taint_kind = Tk_unknown; } in
-  add_tainting_att_param_list prop param_nums formal_params' (Sil.Ataint taint_info)
-
-(* add Auntaint attribute to a callee_pname precondition *)
 let mk_pre pre formal_params callee_pname callee_attrs =
-  if Config.taint_analysis then
+  if Config.taint_analysis
-    add_tainting_att_param_list
+  then
+    match Taint.accepts_sensitive_params callee_pname (Some callee_attrs) with
+    | [] -> pre
+    | tainted_param_nums ->
+        Taint.get_params_to_taint tainted_param_nums formal_params
+        |> IList.fold_left
+          (fun prop_acc (param, taint_kind) ->
+             let attr = Sil.Auntaint { taint_source = callee_pname; taint_kind; } in
+             Taint.add_tainting_attribute attr param prop_acc)
           (Prop.normalize pre)
-      (Taint.accepts_sensitive_params callee_pname (Some callee_attrs))
-      formal_params
-      Sil.Auntaint
         |> Prop.expose
   else pre
 
@@ -858,7 +856,7 @@ let check_taint_on_variadic_function callee_pname caller_pname actual_params cal
       | _::lst' -> n_tail lst' (n-1) in
   let tainted_params = Taint.accepts_sensitive_params callee_pname None in
   match tainted_params with
-  | [tp] when tp<0 ->
+  | [(tp, _)] when tp < 0 ->
       (* All actual params from abs(tp) should not be tainted. If we find one we give the warning *)
       let tp_abs = abs tp in
       L.d_strln ("Checking tainted actual parameters from parameter number "^ (string_of_int tp_abs) ^ " onwards.");
@@ -970,7 +968,7 @@ let do_taint_check caller_pname callee_pname calling_prop missing_pi sub actual_
     | Some (e, Sil.Ataint _) ->
         let taint_atoms, untaint_atoms = try Sil.ExpMap.find e acc_map with Not_found -> ([], []) in
         Sil.ExpMap.add e (atom :: taint_atoms, untaint_atoms) acc_map
-    | Some (e, Sil.Auntaint) ->
+    | Some (e, Sil.Auntaint _) ->
         let taint_atoms, untaint_atoms = try Sil.ExpMap.find e acc_map with Not_found -> ([], []) in
         Sil.ExpMap.add e (taint_atoms, atom :: untaint_atoms) acc_map
     | _ -> acc_map in

infer/src/backend/tabulation.mli

@@ -47,8 +47,3 @@ val exe_function_call:
   ProcAttributes.t -> Tenv.t -> Ident.t list -> Cfg.Procdesc.t -> Procname.t -> Location.t ->
   (Sil.exp * Sil.typ) list -> Prop.normal Prop.t -> Paths.Path.t ->
   (Prop.normal Prop.t * Paths.Path.t) list
-
-(* Set Ataint attribute to list of parameteres in a prop *)
-val add_param_taint :
-  Procname.t -> (Mangled.t * Sil.typ) list -> Prop.normal Prop.t ->
-  int list -> Prop.normal Prop.t

infer/src/backend/taint.ml

@@ -320,29 +320,37 @@ let returns_tainted callee_pname callee_attrs_opt =
 
 let find_callee taint_infos callee_pname =
   try
-    IList.find
+    Some
+      (IList.find
          (fun (taint_info, _) -> Procname.equal taint_info.Sil.taint_source callee_pname)
-      taint_infos
+         taint_infos)
-    |> snd
+  with Not_found -> None
-  with Not_found -> []
 
 (** returns list of zero-indexed argument numbers of [callee_pname] that may be tainted *)
 let accepts_sensitive_params callee_pname callee_attrs_opt =
   match find_callee taint_sinks callee_pname with
-  | [] ->
+  | None ->
       let _, param_annots = attrs_opt_get_annots callee_attrs_opt in
       let offset = if Procname.java_is_static callee_pname then 0 else 1 in
-      IList.mapi (fun param_num attr  -> (param_num + offset, attr)) param_annots
+      let indices_and_annots =
-      |> IList.filter
+        IList.mapi (fun param_num attr  -> param_num + offset, attr) param_annots in
-        (fun (_, attr) ->
+      let tag_tainted_indices acc (index, attr) =
-           Annotations.ia_is_integrity_sink attr || Annotations.ia_is_privacy_sink attr)
+        if Annotations.ia_is_integrity_sink attr
-      |> IList.map fst
+        then (index, Sil.Tk_privacy_annotation) :: acc
-  | tainted_params -> tainted_params
+        else if Annotations.ia_is_privacy_sink attr
+        then (index, Sil.Tk_privacy_annotation) :: acc
+        else acc in
+      IList.fold_left tag_tainted_indices [] indices_and_annots
+  | Some (taint_info, tainted_param_indices) ->
+      IList.map (fun param_num -> param_num, taint_info.Sil.taint_kind) tainted_param_indices
 
 (** returns list of zero-indexed parameter numbers of [callee_pname] that should be
     considered tainted during symbolic execution *)
 let tainted_params callee_pname =
-  find_callee func_with_tainted_params callee_pname
+  match find_callee func_with_tainted_params callee_pname with
+  | Some (taint_info, tainted_param_indices) ->
+      IList.map (fun param_num -> param_num, taint_info.Sil.taint_kind) tainted_param_indices
+  | None -> []
 
 let has_taint_annotation fieldname struct_typ =
   let fld_has_taint_annot (fname, _, annot) =
@@ -350,3 +358,28 @@ let has_taint_annotation fieldname struct_typ =
     (Annotations.ia_is_privacy_source annot || Annotations.ia_is_integrity_source annot) in
   IList.exists fld_has_taint_annot struct_typ.Sil.instance_fields ||
   IList.exists fld_has_taint_annot struct_typ.Sil.static_fields
+
+(* add tainting attributes to a list of paramenters *)
+let get_params_to_taint tainted_param_nums formal_params =
+  let get_taint_kind index =
+    try Some (IList.find (fun (taint_index, _) -> index = taint_index) tainted_param_nums)
+    with Not_found -> None in
+  let collect_params_to_taint params_to_taint_acc (index, param) =
+    match get_taint_kind index with
+    | Some (_, taint_kind) -> (param, taint_kind) :: params_to_taint_acc
+    | None -> params_to_taint_acc in
+  let numbered_params = IList.mapi (fun i param -> (i, param)) formal_params in
+  IList.fold_left collect_params_to_taint [] numbered_params
+
+(* add tainting attribute to a pvar in a prop *)
+let add_tainting_attribute att pvar_param prop =
+  IList.fold_left
+    (fun prop_acc hpred ->
+       match hpred with
+       | Sil.Hpointsto (Sil.Lvar pvar, (Sil.Eexp (rhs, _)), _)
+         when Pvar.equal pvar pvar_param ->
+           L.d_strln ("TAINT ANALYSIS: setting taint/untaint attribute of parameter " ^
+                      (Pvar.to_string pvar));
+           Prop.add_or_replace_exp_attribute prop_acc rhs att
+       | _ -> prop_acc)
+    prop (Prop.get_sigma prop)

infer/src/backend/taint.mli

@@ -13,11 +13,16 @@ open! Utils
 val returns_tainted : Procname.t -> ProcAttributes.t option -> Sil.taint_kind option
 
 (** returns list of zero-indexed argument numbers of [callee_pname] that may be tainted *)
-val accepts_sensitive_params : Procname.t -> ProcAttributes.t option -> int list
+val accepts_sensitive_params : Procname.t -> ProcAttributes.t option -> (int * Sil.taint_kind) list
 
 (** returns list of zero-indexed parameter numbers of [callee_pname] that should be
     considered tainted during symbolic execution *)
-val tainted_params : Procname.t -> int list
+val tainted_params : Procname.t -> (int * Sil.taint_kind) list
 
-(** returns true if [fieldname] has a taint source annotation *)
+(** returns the taint_kind of [fieldname] if it has a taint source annotation *)
 val has_taint_annotation : Ident.fieldname -> Sil.struct_typ -> bool
+
+val add_tainting_attribute : Sil.attribute -> Pvar.t -> Prop.normal Prop.t -> Prop.normal Prop.t
+
+val get_params_to_taint :
+  (int * Sil.taint_kind) list -> Pvar.t list -> (Pvar.t * Sil.taint_kind) list