diff --git a/infer/src/IR/Sil.re b/infer/src/IR/Sil.re index cbe0739d3..674de061c 100644 --- a/infer/src/IR/Sil.re +++ b/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, _) => (-1) - | (_, Auntaint) => 1 + | (Auntaint ti1, Auntaint ti2) => taint_info_compare ti1 ti2 + | (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" diff --git a/infer/src/IR/Sil.rei b/infer/src/IR/Sil.rei index eacc59b64..3cd1b9a36 100644 --- a/infer/src/IR/Sil.rei +++ b/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 */ diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 75149df31..25ec3254b 100644 --- a/infer/src/backend/interproc.ml +++ b/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 tainted_params = Taint.tainted_params proc_name in - Tabulation.add_param_taint proc_name formal_params prop tainted_params + let prop = + if Config.taint_analysis + then add_taint_attrs proc_name prop else prop in L.d_strln ("Processing prop " ^ string_of_int cnt ^ "/" ^ string_of_int num_paths); diff --git a/infer/src/backend/modelBuiltins.ml b/infer/src/backend/modelBuiltins.ml index 00e103a09..75c43d3ce 100644 --- a/infer/src/backend/modelBuiltins.ml +++ b/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 diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index efbd99292..253df711c 100644 --- a/infer/src/backend/symExec.ml +++ b/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 - then check_untainted actual_exp caller_pname callee_pname prop_acc - else prop_acc in + try + let _, taint_kind = IList.find (fun (num, _) -> num = param_num) param_nums 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 diff --git a/infer/src/backend/symExec.mli b/infer/src/backend/symExec.mli index 330808124..ea7db25cb 100644 --- a/infer/src/backend/symExec.mli +++ b/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 : diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index 503d44dd4..f21b79a15 100644 --- a/infer/src/backend/tabulation.ml +++ b/infer/src/backend/tabulation.ml @@ -819,22 +819,20 @@ 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 *) -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 *) +(* Add Auntaint attribute to a callee_pname precondition *) let mk_pre pre formal_params callee_pname callee_attrs = - if Config.taint_analysis then - add_tainting_att_param_list - (Prop.normalize pre) - (Taint.accepts_sensitive_params callee_pname (Some callee_attrs)) - formal_params - Sil.Auntaint - |> Prop.expose + if Config.taint_analysis + 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) + |> Prop.expose else pre let report_taint_error e taint_info callee_pname caller_pname calling_prop = @@ -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 diff --git a/infer/src/backend/tabulation.mli b/infer/src/backend/tabulation.mli index d19be4d75..bfb2c3e6b 100644 --- a/infer/src/backend/tabulation.mli +++ b/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 diff --git a/infer/src/backend/taint.ml b/infer/src/backend/taint.ml index faef0a193..f6364d72b 100644 --- a/infer/src/backend/taint.ml +++ b/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 - (fun (taint_info, _) -> Procname.equal taint_info.Sil.taint_source callee_pname) - taint_infos - |> snd - with Not_found -> [] + Some + (IList.find + (fun (taint_info, _) -> Procname.equal taint_info.Sil.taint_source callee_pname) + taint_infos) + with Not_found -> None (** 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 - |> IList.filter - (fun (_, attr) -> - Annotations.ia_is_integrity_sink attr || Annotations.ia_is_privacy_sink attr) - |> IList.map fst - | tainted_params -> tainted_params + let indices_and_annots = + IList.mapi (fun param_num attr -> param_num + offset, attr) param_annots in + let tag_tainted_indices acc (index, attr) = + if Annotations.ia_is_integrity_sink attr + then (index, Sil.Tk_privacy_annotation) :: acc + 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) diff --git a/infer/src/backend/taint.mli b/infer/src/backend/taint.mli index de7ce9f89..b425178dd 100644 --- a/infer/src/backend/taint.mli +++ b/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