adding type-specific taint error messages

Summary: public Taint errors are complex, and each type requires its own specialized recommendation.

Reviewed By: jeremydubreil

Differential Revision: D3025921

fb-gh-sync-id: 8d7b45b
shipit-source-id: 8d7b45b

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 =

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.

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 =

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

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

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 =