Improved error message for taint analysis

Reviewed By: sblackshear

Differential Revision: D2658030

fb-gh-sync-id: 7979a57

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;
     }
 }

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 =

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.

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 =

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

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 pn1, Ataint pn2 -> Procname.compare pn1 pn2
-  | Ataint, _ -> -1
+  | Ataint _, _ -> -1
-  | _, 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 ->

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

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))

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 ->