adding taint kind to taint source specifications

Reviewed By: jeremydubreil

Differential Revision: D3288728

fbshipit-source-id: c3f68e6

infer/src/IR/sil.ml

@@ -603,9 +603,11 @@ and res_action =
   }
 
 and taint_kind =
-  | UnverifiedSSLSocket
-  | SharedPreferencesData
-  | Unknown
+  | Tk_unverified_SSL_socket
+  | Tk_shared_preferences_data
+  | Tk_privacy_annotation
+  | Tk_integrity_annotation
+  | Tk_unknown
 
 and taint_info = {
   taint_source : Procname.t;
@@ -1125,13 +1127,19 @@ let dangling_kind_compare dk1 dk2 = match dk1, dk2 with
   | DAminusone, DAminusone -> 0
 
 let taint_kind_compare tk1 tk2 = match tk1, tk2 with
-  | UnverifiedSSLSocket, UnverifiedSSLSocket -> 0
-  | UnverifiedSSLSocket, _ -> - 1
-  | _, UnverifiedSSLSocket -> 1
-  | SharedPreferencesData, SharedPreferencesData -> 0
-  | SharedPreferencesData, _ -> 1
-  | _, SharedPreferencesData -> - 1
-  | Unknown, Unknown -> 0
+  | Tk_unverified_SSL_socket, Tk_unverified_SSL_socket -> 0
+  | Tk_unverified_SSL_socket, _ -> - 1
+  | _, Tk_unverified_SSL_socket -> 1
+  | Tk_shared_preferences_data, Tk_shared_preferences_data -> 0
+  | Tk_shared_preferences_data, _ -> 1
+  | _, Tk_shared_preferences_data -> - 1
+  | Tk_privacy_annotation, Tk_privacy_annotation -> 0
+  | Tk_privacy_annotation, _ -> 1
+  | _, Tk_privacy_annotation -> - 1
+  | Tk_integrity_annotation, Tk_integrity_annotation -> 0
+  | Tk_integrity_annotation, _ -> 1
+  | _, Tk_integrity_annotation -> - 1
+  | Tk_unknown, Tk_unknown -> 0
 
 let taint_info_compare { taint_source=ts1; taint_kind=tk1; } { taint_source=ts2; taint_kind=tk2; } =
   taint_kind_compare tk1 tk2

infer/src/IR/sil.mli

@@ -240,9 +240,11 @@ and res_action =
   }
 
 and taint_kind =
-  | UnverifiedSSLSocket
-  | SharedPreferencesData
-  | Unknown
+  | Tk_unverified_SSL_socket
+  | Tk_shared_preferences_data
+  | Tk_privacy_annotation
+  | Tk_integrity_annotation
+  | Tk_unknown
 
 and taint_info = {
   taint_source : Procname.t;

infer/src/backend/localise.ml

@@ -816,22 +816,36 @@ let desc_tainted_value_reaching_sensitive_function
   Tags.add tags Tags.value expr_str;
   let description =
     match taint_kind with
-    | Sil.UnverifiedSSLSocket ->
-        Format.sprintf
+    | Sil.Tk_unverified_SSL_socket ->
+        F.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
+    | Sil.Tk_shared_preferences_data ->
+        F.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
+    | Sil.Tk_privacy_annotation ->
+        F.sprintf
+          "`%s` holds privacy-sensitive data (source: 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.Tk_integrity_annotation ->
+        F.sprintf
+          "`%s` holds untrusted user-controlled data (source: call to %s). This data may flow into a security-sensitive sink via the call to %s %s."
+          expr_str
+          (format_method tainting_fun)
+          (format_method sensitive_fun)
+          (at_line tags loc)
+    | Sil.Tk_unknown ->
+        F.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)

infer/src/backend/modelBuiltins.ml

@@ -652,8 +652,8 @@ let execute___set_taint_attribute
   | (exp, _) :: [(Sil.Const (Sil.Cstr taint_kind_str), _)] ->
       let taint_source = Cfg.Procdesc.get_proc_name pdesc in
       let taint_kind = match taint_kind_str with
-        | "UnverifiedSSLSocket" -> Sil.UnverifiedSSLSocket
-        | "SharedPreferenceData" -> Sil.SharedPreferencesData
+        | "UnverifiedSSLSocket" -> Sil.Tk_unverified_SSL_socket
+        | "SharedPreferenceData" -> Sil.Tk_shared_preferences_data
         | other_str -> failwith ("Unrecognized taint kind " ^ other_str) in
       set_attr pdesc prop_ path exp (Sil.Ataint { Sil.taint_source; taint_kind})
   | _ ->

infer/src/backend/symExec.ml

@@ -842,8 +842,11 @@ let add_constraints_on_retval pdesc prop ret_exp ~has_nullable_annot typ callee_
             (* bind return id to the abducted value pointed to by the pvar we introduced *)
             bind_exp_to_abducted_val ret_exp abducted_ret_pv prop in
         let prop'' = add_ret_non_null ret_exp typ prop' in
-        if Config.taint_analysis && Taint.returns_tainted callee_pname None then
-          add_tainted_post ret_exp { Sil.taint_source = callee_pname; taint_kind = Unknown } prop''
+        if Config.taint_analysis then
+          match Taint.returns_tainted callee_pname None with
+          | Some taint_kind ->
+              add_tainted_post ret_exp { Sil.taint_source = callee_pname; taint_kind; } prop''
+          | None -> prop''
         else prop''
     else add_ret_non_null ret_exp typ prop
 
@@ -851,7 +854,7 @@ let add_taint prop lhs_id rhs_exp pname tenv  =
   let add_attribute_if_field_tainted prop fieldname struct_typ =
     if Taint.has_taint_annotation fieldname struct_typ
     then
-      let taint_info = { Sil.taint_source = pname; taint_kind = Unknown; } in
+      let taint_info = { Sil.taint_source = pname; taint_kind = Tk_unknown; } in
       Prop.add_or_replace_exp_attribute prop (Sil.Var lhs_id) (Sil.Ataint taint_info)
     else
       prop in

infer/src/backend/tabulation.ml

@@ -818,8 +818,7 @@ let add_tainting_att_param_list prop param_nums formal_params att =
 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
-  (* TODO: add taint_kind as part of specification format in taint.ml *)
-  let taint_info = { Sil.taint_source = proc_name; taint_kind = Unknown; } 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 *)
@@ -890,17 +889,18 @@ let mk_posts ret_ids prop callee_pname callee_attrs posts =
           IList.filter (fun (prop, _) -> not (returns_null prop)) posts
         else posts in
       let mk_retval_tainted posts =
-        if Taint.returns_tainted callee_pname (Some callee_attrs) then
+        match Taint.returns_tainted callee_pname (Some callee_attrs) with
+        | Some taint_kind ->
             let taint_retval (prop, path) =
               let prop_normal = Prop.normalize prop in
               let prop' =
                 Prop.add_or_replace_exp_attribute prop_normal
                   (Sil.Var ret_id)
-                (Sil.Ataint { Sil.taint_source = callee_pname; taint_kind = Unknown })
+                  (Sil.Ataint { Sil.taint_source = callee_pname; taint_kind; })
                 |> Prop.expose in
               (prop', path) in
             IList.map taint_retval posts
-        else posts in
+        | None -> posts in
       let posts' =
         if Config.idempotent_getters && !Config.curr_language = Config.Java
         then mk_getter_idempotent posts

infer/src/backend/taint.ml

@@ -22,6 +22,7 @@ let sources = [
     ret_type = "java.lang.Object";
     params = [];
     is_static = true;
+    taint_kind = Sil.Tk_unknown;
     language = Config.Java;
   };
   {
@@ -30,6 +31,7 @@ let sources = [
     ret_type = "java.lang.Object";
     params = [];
     is_static = true;
+    taint_kind = Sil.Tk_unknown;
     language = Config.Java
   };
   (* actual specs *)
@@ -39,6 +41,7 @@ let sources = [
     ret_type = "java.lang.String";
     params = ["java.lang.String"; "java.lang.String"];
     is_static = false;
+    taint_kind = Sil.Tk_shared_preferences_data;
     language = Config.Java
   };
 ] @ FbTaint.sources
@@ -54,6 +57,7 @@ let sinks = [
     ret_type = "void";
     params = ["java.lang.Object"];
     is_static = true;
+    taint_kind = Sil.Tk_unknown;
     language = Config.Java
   }, [0]);
   ({
@@ -62,6 +66,7 @@ let sinks = [
     ret_type = "void";
     params = ["java.lang.Object"];
     is_static = true;
+    taint_kind = Sil.Tk_unknown;
     language = Config.Java
   }, [0]);
   (* actual specs *)
@@ -71,6 +76,7 @@ let sinks = [
     ret_type = "int";
     params = ["java.lang.String"; "java.lang.String"];
     is_static = true;
+    taint_kind = Sil.Tk_privacy_annotation;
     language = Config.Java
   }, [0;1]);
   ({
@@ -79,6 +85,7 @@ let sinks = [
     ret_type = "java.io.InputStream";
     params = ["android.net.Uri"];
     is_static = false;
+    taint_kind = Sil.Tk_privacy_annotation;
     language = Config.Java;
   }, [1]);
   ({
@@ -87,6 +94,7 @@ let sinks = [
     ret_type = "java.io.OutputStream";
     params = ["android.net.Uri"];
     is_static = false;
+    taint_kind = Sil.Tk_privacy_annotation;
     language = Config.Java;
   }, [0]);
   ({
@@ -95,6 +103,7 @@ let sinks = [
     ret_type = "java.io.OutputStream";
     params = ["android.net.Uri"; "java.lang.String"];
     is_static = false;
+    taint_kind = Sil.Tk_privacy_annotation;
     language = Config.Java;
   }, [0]);
   ({
@@ -103,6 +112,7 @@ let sinks = [
     ret_type = "android.content.res.AssetFileDescriptor";
     params = ["android.net.Uri"; "java.lang.String"];
     is_static = false;
+    taint_kind = Sil.Tk_privacy_annotation;
     language = Config.Java;
   }, [0]);
   ({
@@ -111,6 +121,7 @@ let sinks = [
     ret_type = "android.content.res.AssetFileDescriptor";
     params = ["android.net.Uri"; "java.lang.String"; "android.os.CancellationSignal"];
     is_static = false;
+    taint_kind = Sil.Tk_privacy_annotation;
     language = Config.Java;
   }, [0]);
   ({
@@ -119,6 +130,7 @@ let sinks = [
     ret_type = "android.os.ParcelFileDescriptor";
     params = ["android.net.Uri"; "java.lang.String"; "android.os.CancellationSignal"];
     is_static = false;
+    taint_kind = Sil.Tk_privacy_annotation;
     language = Config.Java;
   }, [0]);
   ({
@@ -127,6 +139,7 @@ let sinks = [
     ret_type = "android.os.ParcelFileDescriptor";
     params = ["android.net.Uri"; "java.lang.String"];
     is_static = false;
+    taint_kind = Sil.Tk_privacy_annotation;
     language = Config.Java;
   }, [0]);
   ({
@@ -136,6 +149,7 @@ let sinks = [
     params = ["android.net.Uri"; "java.lang.String"; "android.os.Bundle";
               "android.os.CancellationSignal"];
     is_static = false;
+    taint_kind = Sil.Tk_privacy_annotation;
     language = Config.Java;
   }, [0]);
   ({
@@ -144,6 +158,7 @@ let sinks = [
     ret_type = "android.content.res.AssetFileDescriptor";
     params = ["android.net.Uri"; "java.lang.String"; "android.os.Bundle"];
     is_static = false;
+    taint_kind = Sil.Tk_privacy_annotation;
     language = Config.Java;
   }, [0]);
 
@@ -154,7 +169,8 @@ let sinks = [
     ret_type = "void";
     params = [];
     is_static = false;
-    language = Config.Clang
+    taint_kind = Sil.Tk_unknown;
+    language = Config.Clang;
   }, [1]); (* it's instance method *)
 ] @ FbTaint.sinks
 
@@ -166,7 +182,8 @@ let functions_with_tainted_params = [
     ret_type = "BOOL";
     params = [];
     is_static = false; (* it's instance method *)
-    language = Config.Clang
+    taint_kind = Sil.Tk_unknown;
+    language = Config.Clang;
   }, [2]);
 
   (* actual specs *)
@@ -180,7 +197,8 @@ let functions_with_tainted_params = [
     ret_type = "BOOL";
     params = [];
     is_static = false; (* it's instance method *)
-    language = Config.Clang
+    taint_kind = Sil.Tk_integrity_annotation;
+    language = Config.Clang;
   }, [2]);
 ] @ FbTaint.functions_with_tainted_params
 
@@ -208,12 +226,19 @@ let method_str_to_pname method_str =
   | Config.Java ->
       java_method_to_procname method_str
 
+let taint_spec_to_taint_info taint_spec =
+  let taint_source =
+    match taint_spec.language with
+    | Config.Clang -> objc_method_to_procname taint_spec
+    | Config.Java -> java_method_to_procname taint_spec in
+  { Sil.taint_source; taint_kind = taint_spec.taint_kind }
+
 let sources =
-  IList.map method_str_to_pname sources
+  IList.map taint_spec_to_taint_info sources
 
 let mk_pname_param_num methods =
   IList.map
-    (fun (mname, param_num) -> method_str_to_pname mname, param_num)
+    (fun (mname, param_num) -> taint_spec_to_taint_info mname, param_num)
     methods
 
 let taint_sinks =
@@ -226,16 +251,28 @@ let attrs_opt_get_annots = function
   | Some attrs -> attrs.ProcAttributes.method_annotation
   | None -> Sil.method_annotation_empty
 
+(* TODO: return a taint kind *)
 (** returns true if [callee_pname] returns a tainted value *)
 let returns_tainted callee_pname callee_attrs_opt =
-  IList.exists (fun pname -> Procname.equal pname callee_pname) sources ||
+  let procname_matches taint_info =
+    Procname.equal taint_info.Sil.taint_source callee_pname in
+  try
+    let taint_info = IList.find procname_matches sources in
+    Some taint_info.Sil.taint_kind
+  with Not_found ->
     let ret_annot, _ = attrs_opt_get_annots callee_attrs_opt in
-  Annotations.ia_is_privacy_source ret_annot ||
-  Annotations.ia_is_integrity_source ret_annot
+    if Annotations.ia_is_integrity_source ret_annot
+    then Some Sil.Tk_integrity_annotation
+    else if Annotations.ia_is_privacy_source ret_annot
+    then Some Sil.Tk_privacy_annotation
+    else None
 
-let find_callee methods callee_pname =
+let find_callee taint_infos callee_pname =
   try
-    snd (IList.find (fun (pname, _) -> Procname.equal pname callee_pname) methods)
+    IList.find
+      (fun (taint_info, _) -> Procname.equal taint_info.Sil.taint_source callee_pname)
+      taint_infos
+    |> snd
   with Not_found -> []
 
 (** returns list of zero-indexed argument numbers of [callee_pname] that may be tainted *)
@@ -247,7 +284,7 @@ let accepts_sensitive_params callee_pname callee_attrs_opt =
       IList.mapi (fun param_num attr  -> (param_num + offset, attr)) param_annots
       |> IList.filter
         (fun (_, attr) ->
-           Annotations.ia_is_privacy_sink attr || Annotations.ia_is_integrity_sink attr)
+           Annotations.ia_is_integrity_sink attr || Annotations.ia_is_privacy_sink attr)
       |> IList.map fst
   | tainted_params -> tainted_params
 

infer/src/backend/taint.mli

@@ -10,7 +10,7 @@
 open! Utils
 
 (** returns true if [callee_pname] returns a tainted value *)
-val returns_tainted : Procname.t -> ProcAttributes.t option -> bool
+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

infer/src/checkers/patternMatch.ml

@@ -14,12 +14,13 @@ open! Utils
 module L = Logging
 module F = Format
 
-type method_str = {
+type taint_spec = {
   classname : string;
   method_name : string;
   ret_type : string;
   params : string list;
   is_static : bool;
+  taint_kind : Sil.taint_kind;
   language : Config.language
 }
 

infer/src/checkers/patternMatch.mli

@@ -11,12 +11,13 @@ open! Utils
 
 (** Module for Pattern matching. *)
 
-type method_str = {
+type taint_spec = {
   classname : string;
   method_name : string;
   ret_type : string;
   params : string list;
   is_static : bool;
+  taint_kind : Sil.taint_kind;
   language : Config.language
 }