diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml index 7596ddda5..cde23da68 100644 --- a/infer/src/backend/errdesc.ml +++ b/infer/src/backend/errdesc.ml @@ -871,7 +871,8 @@ let explain_nth_function_parameter use_buckets deref_str prop n pvar_off = let find_pvar_with_exp prop exp = let res = ref None in let found_in_pvar pv = - res := Some (pv, Fpvar) in + if not (Sil.pvar_is_abducted pv) && not (Sil.pvar_is_this pv) then + res := Some (pv, Fpvar) in let found_in_struct pv fld_lst = (* found_in_pvar has priority *) if !res = None then res := Some (pv, Fstruct (IList.rev fld_lst)) in let rec search_struct pv fld_lst = function @@ -956,18 +957,25 @@ let explain_retain_cycle prop cycle loc dotty_str = Localise.desc_retain_cycle prop cycle loc dotty_str (** Explain a tainted value error *) -let explain_tainted_value_reaching_sensitive_function e { Sil.taint_source } sensitive_fun loc = +let explain_tainted_value_reaching_sensitive_function + prop e { Sil.taint_source; taint_kind } sensitive_fun loc = let var_desc = match e with | Sil.Lvar pv -> Sil.pvar_to_string pv - | exp -> + | _ -> begin - match exp_rv_dexp (State.get_node ()) exp with - | Some dexp -> Sil.dexp_to_string dexp - | None -> Sil.exp_to_string exp + match find_pvar_with_exp prop e with + | Some (pvar, pvar_off) -> + let dexp = dexp_apply_pvar_off (Sil.Dpvar pvar) pvar_off in + Sil.dexp_to_string dexp + | None -> Sil.exp_to_string e end in - Localise.desc_tainted_value_reaching_sensitive_function var_desc - (Procname.to_string taint_source) (Procname.to_string sensitive_fun) loc + Localise.desc_tainted_value_reaching_sensitive_function + taint_kind + var_desc + taint_source + sensitive_fun + loc (** explain a return statement missing *) let explain_return_statement_missing loc = diff --git a/infer/src/backend/errdesc.mli b/infer/src/backend/errdesc.mli index ceaac5ce3..bebf0c426 100644 --- a/infer/src/backend/errdesc.mli +++ b/infer/src/backend/errdesc.mli @@ -111,7 +111,7 @@ val explain_unary_minus_applied_to_unsigned_expression : (** Explain a tainted value error *) val explain_tainted_value_reaching_sensitive_function : - Sil.exp -> Sil.taint_info -> Procname.t -> Location.t -> Localise.error_desc + Prop.normal Prop.t -> Sil.exp -> Sil.taint_info -> Procname.t -> Location.t -> Localise.error_desc (** Produce a description of a leak by looking at the current state. If the current instruction is a variable nullify, blame the variable. diff --git a/infer/src/backend/localise.ml b/infer/src/backend/localise.ml index 76afb9326..37b359289 100644 --- a/infer/src/backend/localise.ml +++ b/infer/src/backend/localise.ml @@ -794,18 +794,36 @@ let desc_stack_variable_address_escape expr_str addr_dexp_str loc = (at_line tags loc) in { no_desc with descriptions = [description]; tags = !tags } -let desc_tainted_value_reaching_sensitive_function expr_str tainting_fun sensitive_fun loc = +let desc_tainted_value_reaching_sensitive_function + taint_kind expr_str tainting_fun sensitive_fun loc = let tags = Tags.create () in Tags.add tags Tags.value expr_str; - let description = Format.sprintf - "Value %s could be insecure (tainted) due to call to function %s %s %s %s. Function %s %s" - expr_str - tainting_fun - "and is reaching sensitive function" - sensitive_fun - (at_line tags loc) - sensitive_fun - "requires its input to be verified or sanitized." in + let description = + match taint_kind with + | Sil.UnverifiedSSLSocket -> + Format.sprintf + "The hostname of SSL socket `%s` (returned from %s) has not been verified! Reading from the socket via the call to %s %s is dangerous. You should verify the hostname of the socket using a HostnameVerifier before reading; otherwise, you may be vulnerable to a man-in-the-middle attack." + expr_str + (format_method tainting_fun) + (format_method sensitive_fun) + (at_line tags loc) + | Sil.SharedPreferencesData -> + Format.sprintf + "`%s` holds sensitive data read from a SharedPreferences object (via call to %s). This data may leak via the call to %s %s." + expr_str + (format_method tainting_fun) + (format_method sensitive_fun) + (at_line tags loc) + | Sil.Unknown -> + Format.sprintf + "Value `%s` could be insecure (tainted) due to call to function %s %s %s %s. Function %s %s" + expr_str + (format_method tainting_fun) + "and is reaching sensitive function" + (format_method sensitive_fun) + (at_line tags loc) + (format_method sensitive_fun) + "requires its input to be verified or sanitized." in { no_desc with descriptions = [description]; tags = !tags } let desc_uninitialized_dangling_pointer_deref deref expr_str loc = diff --git a/infer/src/backend/localise.mli b/infer/src/backend/localise.mli index f11ee3f96..224690479 100644 --- a/infer/src/backend/localise.mli +++ b/infer/src/backend/localise.mli @@ -244,6 +244,6 @@ val desc_unary_minus_applied_to_unsigned_expression : string option -> string -> Location.t -> error_desc val desc_tainted_value_reaching_sensitive_function : - string -> string -> string -> Location.t -> error_desc + Sil.taint_kind -> string -> Procname.t -> Procname.t -> Location.t -> error_desc val desc_uninitialized_dangling_pointer_deref : deref_str -> string -> Location.t -> error_desc diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 91afc5b4d..2c3cdf373 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -1359,8 +1359,12 @@ and check_untainted exp caller_pname callee_pname prop = match Prop.get_taint_attribute prop exp with | Some (Sil.Ataint source_pname) -> let err_desc = - Errdesc.explain_tainted_value_reaching_sensitive_function exp source_pname - callee_pname (State.get_loc ()) in + Errdesc.explain_tainted_value_reaching_sensitive_function + prop + exp + source_pname + callee_pname + (State.get_loc ()) in let exn = Exceptions.Tainted_value_reaching_sensitive_function (err_desc, __POS__) in diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index 7b110aa7d..bea98ebcc 100644 --- a/infer/src/backend/tabulation.ml +++ b/infer/src/backend/tabulation.ml @@ -851,7 +851,8 @@ let inconsistent_actualpre_missing actual_pre split_opt = (* perform the taint analysis check by comparing the taint atoms in [calling_pi] with the untaint atoms required by the [missing_pi] computed during abduction *) -let do_taint_check caller_pname callee_pname calling_pi missing_pi sub = +let do_taint_check caller_pname callee_pname calling_prop missing_pi sub = + let calling_pi = Prop.get_pi calling_prop in (* get a version of [missing_pi] whose var names match the names in calling pi *) let missing_pi_sub = Prop.pi_sub sub missing_pi in let combined_pi = calling_pi @ missing_pi_sub in @@ -879,8 +880,13 @@ let do_taint_check caller_pname callee_pname calling_pi missing_pi sub = let taint_info = match Prop.atom_get_exp_attribute taint_atom with | Some (_, Sil.Ataint taint_info) -> taint_info | _ -> failwith "Expected to get taint attr on atom" in - let err_desc = Errdesc.explain_tainted_value_reaching_sensitive_function e taint_info - callee_pname (State.get_loc ()) in + let err_desc = + Errdesc.explain_tainted_value_reaching_sensitive_function + calling_prop + e + taint_info + callee_pname + (State.get_loc ()) in let exn = Exceptions.Tainted_value_reaching_sensitive_function (err_desc, __POS__) in @@ -947,7 +953,7 @@ let exe_spec let do_split () = let missing_pi' = if !Config.taint_analysis then - do_taint_check caller_pname callee_pname (Prop.get_pi actual_pre) missing_pi sub2 + do_taint_check caller_pname callee_pname actual_pre missing_pi sub2 else missing_pi in process_splitting actual_pre sub1 sub2 frame missing_pi' missing_sigma frame_fld missing_fld frame_typ missing_typ in let report_valid_res split =