diff --git a/infer/src/IR/sil.ml b/infer/src/IR/sil.ml index d71296158..a90962756 100644 --- a/infer/src/IR/sil.ml +++ b/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 diff --git a/infer/src/IR/sil.mli b/infer/src/IR/sil.mli index 01c7bf4e8..1f38e4c37 100644 --- a/infer/src/IR/sil.mli +++ b/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; diff --git a/infer/src/backend/localise.ml b/infer/src/backend/localise.ml index 1dd14ee39..1249daf00 100644 --- a/infer/src/backend/localise.ml +++ b/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) diff --git a/infer/src/backend/modelBuiltins.ml b/infer/src/backend/modelBuiltins.ml index e2e24685c..81c7bff44 100644 --- a/infer/src/backend/modelBuiltins.ml +++ b/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}) | _ -> diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 943d464c6..efbd99292 100644 --- a/infer/src/backend/symExec.ml +++ b/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 diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index 9678bc592..14df513cc 100644 --- a/infer/src/backend/tabulation.ml +++ b/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 - 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 }) - |> Prop.expose in - (prop', path) in - IList.map taint_retval posts - else posts in + 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; }) + |> Prop.expose in + (prop', path) in + IList.map taint_retval posts + | None -> posts in let posts' = if Config.idempotent_getters && !Config.curr_language = Config.Java then mk_getter_idempotent posts diff --git a/infer/src/backend/taint.ml b/infer/src/backend/taint.ml index 0f9e0d9e7..ceb74fd6d 100644 --- a/infer/src/backend/taint.ml +++ b/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 ret_annot, _ = attrs_opt_get_annots callee_attrs_opt in - Annotations.ia_is_privacy_source ret_annot || - Annotations.ia_is_integrity_source ret_annot + 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 + 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 diff --git a/infer/src/backend/taint.mli b/infer/src/backend/taint.mli index d665b7d56..de7ce9f89 100644 --- a/infer/src/backend/taint.mli +++ b/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 diff --git a/infer/src/checkers/patternMatch.ml b/infer/src/checkers/patternMatch.ml index 97bac6061..0c6a8be8c 100644 --- a/infer/src/checkers/patternMatch.ml +++ b/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 } diff --git a/infer/src/checkers/patternMatch.mli b/infer/src/checkers/patternMatch.mli index b63b57632..ed0bf5bac 100644 --- a/infer/src/checkers/patternMatch.mli +++ b/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 }