diff --git a/infer/models/java/src/java/net/URL.java b/infer/models/java/src/java/net/URL.java index 90b711aee..7638d70c1 100644 --- a/infer/models/java/src/java/net/URL.java +++ b/infer/models/java/src/java/net/URL.java @@ -66,29 +66,33 @@ public final class URL implements java.io.Serializable { return openConnection(null); } - String tainted_string() { + public String getHost() { String res = new String(); InferBuiltins.__set_taint_attribute(res); return res; } - public String getHost() { - return tainted_string(); - } - public String getAuthority() { - return tainted_string(); + String res = new String(); + InferBuiltins.__set_taint_attribute(res); + return res; } public String getProtocol() { - return tainted_string(); + String res = new String(); + InferBuiltins.__set_taint_attribute(res); + return res; } public String toExternalForm() { - return tainted_string(); + String res = new String(); + InferBuiltins.__set_taint_attribute(res); + return res; } public String toString() { - return tainted_string(); + String res = new String(); + InferBuiltins.__set_taint_attribute(res); + return res; } } diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml index 57ce0e8a6..a54370d35 100644 --- a/infer/src/backend/errdesc.ml +++ b/infer/src/backend/errdesc.ml @@ -974,12 +974,13 @@ let explain_retain_cycle prop cycle loc = Localise.desc_retain_cycle prop cycle loc (** Explain a tainted value error *) -let explain_tainted_value_reaching_sensitive_function e loc = +let explain_tainted_value_reaching_sensitive_function e taint_fun sensitive_fun loc = let var_desc = match e with | Sil.Lvar pv -> Sil.pvar_to_string pv | _ -> " of some parameter " in - Localise.desc_tainted_value_reaching_sensitive_function var_desc loc + Localise.desc_tainted_value_reaching_sensitive_function var_desc + (Procname.to_string taint_fun) (Procname.to_string 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 85bee57c3..cb0a26c3e 100644 --- a/infer/src/backend/errdesc.mli +++ b/infer/src/backend/errdesc.mli @@ -112,7 +112,8 @@ val explain_unary_minus_applied_to_unsigned_expression : Sil.exp -> Sil.typ -> Cfg.Node.t -> Location.t -> Localise.error_desc (** Explain a tainted value error *) -val explain_tainted_value_reaching_sensitive_function : Sil.exp -> Location.t -> Localise.error_desc +val explain_tainted_value_reaching_sensitive_function : + Sil.exp -> Procname.t -> 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 c66abbd7a..dbaf465c4 100644 --- a/infer/src/backend/localise.ml +++ b/infer/src/backend/localise.ml @@ -734,13 +734,18 @@ let desc_stack_variable_address_escape expr_str addr_dexp_str loc = (at_line tags loc) in [description], None, !tags -let desc_tainted_value_reaching_sensitive_function expr_str loc = +let desc_tainted_value_reaching_sensitive_function 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 can be tainted and is reaching sensitive function %s" + "Value %s could be insecure (tainted) due to call to function %s %s %s %s. Function %s %s" expr_str - (at_line tags loc) in + tainting_fun + "and is reaching sensitive function" + sensitive_fun + (at_line tags loc) + sensitive_fun + "requires its input to be verified or sanitized." in [description], None, !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 c63c68b77..39ad6eec4 100644 --- a/infer/src/backend/localise.mli +++ b/infer/src/backend/localise.mli @@ -231,6 +231,7 @@ val desc_inherently_dangerous_function : Procname.t -> error_desc val desc_unary_minus_applied_to_unsigned_expression : string option -> string -> Location.t -> error_desc -val desc_tainted_value_reaching_sensitive_function : string -> Location.t -> error_desc +val desc_tainted_value_reaching_sensitive_function : + string -> string -> string -> Location.t -> error_desc val desc_uninitialized_dangling_pointer_deref : deref_str -> string -> Location.t -> error_desc diff --git a/infer/src/backend/sil.ml b/infer/src/backend/sil.ml index b18bb23aa..fba5eef30 100644 --- a/infer/src/backend/sil.ml +++ b/infer/src/backend/sil.ml @@ -614,7 +614,7 @@ and attribute = | Adangling of dangling_kind (** dangling pointer *) (** undefined value obtained by calling the given procedure *) | Aundef of Procname.t * Location.t * path_pos - | Ataint + | Ataint of Procname.t (** Procname is the source of the taint *) | Auntaint (** value appeared in second argument of division at given path position *) | Adiv0 of path_pos @@ -1129,7 +1129,7 @@ let attribute_to_category att = match att with | Aresource _ | Adangling _ -> ACresource - | Ataint + | Ataint _ | Auntaint -> ACtaint | Aautorelease -> ACautorelease | Adiv0 _ -> ACdiv0 @@ -1358,9 +1358,9 @@ and attribute_compare (att1 : attribute) (att2 : attribute) : int = | Adangling _, _ -> - 1 | _, Adangling _ -> 1 | Aundef (pn1, _, _), Aundef (pn2, _, _) -> Procname.compare pn1 pn2 - | Ataint, Ataint -> 0 - | Ataint, _ -> -1 - | _, Ataint -> 1 + | Ataint pn1, Ataint pn2 -> Procname.compare pn1 pn2 + | Ataint _, _ -> -1 + | _, Ataint _ -> 1 | Auntaint, Auntaint -> 0 | Auntaint, _ -> -1 | _, Auntaint -> 1 @@ -1942,7 +1942,7 @@ and attribute_to_string pe = function | Aundef (pn, loc, _) -> "UND" ^ (str_binop pe Lt) ^ Procname.to_string pn ^ (str_binop pe Gt) ^ ":" ^ (string_of_int loc.Location.line) - | Ataint -> "TAINTED" + | Ataint pn -> "TAINTED[" ^ (Procname.to_string pn) ^ "]" | Auntaint -> "UNTAINTED" | Adiv0 (pn, nd_id) -> "DIV0" | Aobjc_null exp -> diff --git a/infer/src/backend/sil.mli b/infer/src/backend/sil.mli index accba19c6..1868460dd 100644 --- a/infer/src/backend/sil.mli +++ b/infer/src/backend/sil.mli @@ -254,7 +254,7 @@ and attribute = | Adangling of dangling_kind (** dangling pointer *) (** undefined value obtained by calling the given procedure *) | Aundef of Procname.t * Location.t * path_pos - | Ataint + | Ataint of Procname.t (** Procname is the source of the taint *) | Auntaint (** value appeared in second argument of division at given path position *) | Adiv0 of path_pos diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 0af319e92..90aa464e3 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -1805,7 +1805,8 @@ module ModelBuiltins = struct let prop' = match Prop.get_taint_attribute prop n_lexp with | _ -> let check_attr_change att_old att_new = () in - let p'= Prop.add_or_replace_exp_attribute check_attr_change prop n_lexp (Sil.Ataint) in + let p'= Prop.add_or_replace_exp_attribute check_attr_change + prop n_lexp (Sil.Ataint pname) in p' in [(prop', path)] | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x)) diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index 8f2320473..2006710fd 100644 --- a/infer/src/backend/tabulation.ml +++ b/infer/src/backend/tabulation.ml @@ -765,7 +765,7 @@ let inconsistent_actualpre_missing actual_pre split_opt = let rec get_taint_untaint pi = let get_att_exp p e (t,u) = match Prop.get_taint_attribute p e with - | Some(Sil.Ataint) -> + | Some(Sil.Ataint _) -> L.d_str " ---->Found TAINTED exp: "; Sil.d_exp e; L.d_ln (); (e::t, u) | Some(Sil.Auntaint) -> @@ -783,7 +783,7 @@ let rec get_taint_untaint pi = (* perform the taint analysis check by comparing in a function call the actual calling state and the missing pi computed by abduction *) -let do_taint_check caller_pname calling_prop missing_pi sub prop = +let do_taint_check caller_pname callee_pname calling_prop missing_pi sub prop = (* Note: returns only the first element in the intersection*) let rec intersection_taint_untaint taint untaint = match taint with @@ -804,7 +804,11 @@ let do_taint_check caller_pname calling_prop missing_pi sub prop = let e' = match Errdesc.find_pvar_with_exp prop e with | Some (pv, _) -> Sil.Lvar pv | None -> e in - let err_desc = Errdesc.explain_tainted_value_reaching_sensitive_function e' (State.get_loc ()) in + let tainting_fun = match Prop.get_taint_attribute prop e with + | Some (Sil.Ataint tf) -> tf + | _ -> Procname.empty (* by definition of e, we should not get to this case *) in + let err_desc = Errdesc.explain_tainted_value_reaching_sensitive_function e' tainting_fun + callee_pname (State.get_loc ()) in let exn = Exceptions.Tainted_value_reaching_sensitive_function (err_desc, try assert false with Assert_failure x -> x) in @@ -904,7 +908,7 @@ let exe_spec begin IList.iter log_check_exn checks; if !Config.taint_analysis then - do_taint_check caller_pname actual_pre missing_pi sub2 prop; + do_taint_check caller_pname callee_pname actual_pre missing_pi sub2 prop; let subbed_pre = (Prop.prop_sub sub1 actual_pre) in match check_dereferences callee_pname subbed_pre sub2 spec_pre formal_params with | Some (Deref_undef _, _) when !Config.angelic_execution ->