From 15f0c7e384897a14e8fbd85219f3e021479232f7 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Tue, 8 Mar 2016 18:17:47 -0800 Subject: [PATCH] adding "kind" for taint attribute Reviewed By: jvillard Differential Revision: D3024758 fb-gh-sync-id: 8d3ac70 shipit-source-id: 8d3ac70 --- .../facebook/infer/models/InferBuiltins.java | 2 +- infer/models/java/src/java/net/URL.java | 29 ------------------ .../java/src/javax/net/SocketFactory.java | 2 +- infer/src/backend/errdesc.ml | 11 +++++-- infer/src/backend/errdesc.mli | 2 +- infer/src/backend/sil.ml | 29 ++++++++++++++++-- infer/src/backend/sil.mli | 12 +++++++- infer/src/backend/symExec.ml | 30 ++++++++++++------- infer/src/backend/tabulation.ml | 14 +++++---- 9 files changed, 76 insertions(+), 55 deletions(-) diff --git a/infer/models/java/src/com/facebook/infer/models/InferBuiltins.java b/infer/models/java/src/com/facebook/infer/models/InferBuiltins.java index ffa378911..fcd8bd968 100644 --- a/infer/models/java/src/com/facebook/infer/models/InferBuiltins.java +++ b/infer/models/java/src/com/facebook/infer/models/InferBuiltins.java @@ -38,7 +38,7 @@ public class InferBuiltins { public native static String __split_get_nth(String s, String sep, int n); - public native static void __set_taint_attribute(Object o); + public native static void __set_taint_attribute(Object o, String taintKind); public native static void __set_untaint_attribute(Object o); diff --git a/infer/models/java/src/java/net/URL.java b/infer/models/java/src/java/net/URL.java index c88f23aff..e3a699075 100644 --- a/infer/models/java/src/java/net/URL.java +++ b/infer/models/java/src/java/net/URL.java @@ -66,33 +66,4 @@ public final class URL implements java.io.Serializable { return openConnection(null); } - public String getHost() { - String res = new String(); - InferBuiltins.__set_taint_attribute(res); - return res; - } - - public String getAuthority() { - String res = new String(); - InferBuiltins.__set_taint_attribute(res); - return res; - } - - public String getProtocol() { - String res = new String(); - InferBuiltins.__set_taint_attribute(res); - return res; - } - - public String toExternalForm() { - String res = new String(); - InferBuiltins.__set_taint_attribute(res); - return res; - } - - public String toString() { - String res = new String(); - InferBuiltins.__set_taint_attribute(res); - return res; - } } diff --git a/infer/models/java/src/javax/net/SocketFactory.java b/infer/models/java/src/javax/net/SocketFactory.java index 4c54ec5cc..b590cfcac 100644 --- a/infer/models/java/src/javax/net/SocketFactory.java +++ b/infer/models/java/src/javax/net/SocketFactory.java @@ -36,7 +36,7 @@ public class SocketFactory { public Socket createSocket() { Socket socket = returnAllocatedSocket(); - InferBuiltins.__set_taint_attribute(socket); + InferBuiltins.__set_taint_attribute(socket, "UnverifiedSSLSocket"); return socket; } diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml index a1e29873d..7596ddda5 100644 --- a/infer/src/backend/errdesc.ml +++ b/infer/src/backend/errdesc.ml @@ -956,13 +956,18 @@ 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 taint_fun sensitive_fun loc = +let explain_tainted_value_reaching_sensitive_function e { Sil.taint_source } sensitive_fun loc = let var_desc = match e with | Sil.Lvar pv -> Sil.pvar_to_string pv - | _ -> " of some parameter " in + | exp -> + begin + match exp_rv_dexp (State.get_node ()) exp with + | Some dexp -> Sil.dexp_to_string dexp + | None -> Sil.exp_to_string exp + end in Localise.desc_tainted_value_reaching_sensitive_function var_desc - (Procname.to_string taint_fun) (Procname.to_string sensitive_fun) loc + (Procname.to_string taint_source) (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 6ec76ce6d..ceaac5ce3 100644 --- a/infer/src/backend/errdesc.mli +++ b/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 -> Procname.t -> Procname.t -> Location.t -> Localise.error_desc + 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. diff --git a/infer/src/backend/sil.ml b/infer/src/backend/sil.ml index c359e5534..b01332920 100644 --- a/infer/src/backend/sil.ml +++ b/infer/src/backend/sil.ml @@ -601,6 +601,16 @@ and res_action = ra_vpath: vpath; (** vpath of the resource value *) } +and taint_kind = + | UnverifiedSSLSocket + | SharedPreferencesData + | Unknown + +and taint_info = { + taint_source : Procname.t; + taint_kind : taint_kind; +} + (** Attributes *) and attribute = | Aresource of res_action (** resource acquire/release *) @@ -608,7 +618,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 of Procname.t (** Procname is the source of the taint *) + | Ataint of taint_info | Auntaint | Alocked | Aunlocked @@ -1164,6 +1174,19 @@ let dangling_kind_compare dk1 dk2 = match dk1, dk2 with | _, DAaddr_stack_var -> 1 | 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 + +let taint_info_compare { taint_source=ts1; taint_kind=tk1; } { taint_source=ts2; taint_kind=tk2; } = + taint_kind_compare tk1 tk2 + |> next Procname.compare ts1 ts2 + let attribute_category_compare (ac1 : attribute_category) (ac2 : attribute_category) : int = Pervasives.compare ac1 ac2 @@ -1372,7 +1395,7 @@ and attribute_compare (att1 : attribute) (att2 : attribute) : int = | Adangling _, _ -> - 1 | _, Adangling _ -> 1 | Aundef (pn1, _, _), Aundef (pn2, _, _) -> Procname.compare pn1 pn2 - | Ataint pn1, Ataint pn2 -> Procname.compare pn1 pn2 + | Ataint ti1, Ataint ti2 -> taint_info_compare ti1 ti2 | Ataint _, _ -> -1 | _, Ataint _ -> 1 | Auntaint, Auntaint -> 0 @@ -1943,7 +1966,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 pn -> "TAINTED[" ^ (Procname.to_string pn) ^ "]" + | Ataint { taint_source; } -> "TAINTED[" ^ (Procname.to_string taint_source) ^ "]" | Auntaint -> "UNTAINTED" | Alocked -> "LOCKED" | Aunlocked -> "UNLOCKED" diff --git a/infer/src/backend/sil.mli b/infer/src/backend/sil.mli index d703b616a..59e35cca6 100644 --- a/infer/src/backend/sil.mli +++ b/infer/src/backend/sil.mli @@ -237,6 +237,16 @@ and res_action = ra_vpath: vpath; (** vpath of the resource value *) } +and taint_kind = + | UnverifiedSSLSocket + | SharedPreferencesData + | Unknown + +and taint_info = { + taint_source : Procname.t; + taint_kind : taint_kind; +} + (** Attributes *) and attribute = | Aresource of res_action (** resource acquire/release *) @@ -244,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 of Procname.t (** Procname is the source of the taint *) + | Ataint of taint_info | Auntaint | Alocked | Aunlocked diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 7ac45aec5..91afc5b4d 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -883,7 +883,7 @@ let add_constraints_on_retval pdesc prop ret_exp typ callee_pname callee_loc = 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_secret callee_pname then - add_tainted_post ret_exp callee_pname prop'' + add_tainted_post ret_exp { Sil.taint_source = callee_pname; taint_kind = Unknown } prop'' else prop'' else add_ret_non_null ret_exp typ prop @@ -2259,14 +2259,16 @@ module ModelBuiltins = struct IList.fold_left call_release [(prop_without_attribute, path)] autoreleased_objects else execute___no_op prop_ path + let set_attr pdesc prop path exp attr = + let pname = Cfg.Procdesc.get_proc_name pdesc in + let n_lexp, prop = exp_norm_check_arith pname prop exp in + [(Prop.add_or_replace_exp_attribute prop n_lexp attr, path)] + (** Set attibute att *) - let execute___set_attr att { Builtin.pdesc; prop_; path; args; } + let execute___set_attr attr { Builtin.pdesc; prop_; path; args; } : Builtin.ret_typ = match args with - | [(lexp, _)] -> - let pname = Cfg.Procdesc.get_proc_name pdesc in - let n_lexp, prop = exp_norm_check_arith pname prop_ lexp in - [(Prop.add_or_replace_exp_attribute prop n_lexp att, path)] + | [(lexp, _)] -> set_attr pdesc prop_ path lexp attr | _ -> raise (Exceptions.Wrong_argument_number __POS__) (** Set the attibute of the value as resource/locked*) @@ -2297,13 +2299,21 @@ module ModelBuiltins = struct ra_vpath = None; } in execute___set_attr (Sil.Aresource ra) builtin_args - (** Set the attibute of the value as tainted *) let execute___set_taint_attribute - ({ Builtin.pdesc; } as builtin_args) + ({ Builtin.pdesc; args; prop_; path; }) : Builtin.ret_typ = - let pname = Cfg.Procdesc.get_proc_name pdesc in - execute___set_attr (Sil.Ataint pname) builtin_args + match args with + | (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 + | other_str -> failwith ("Unrecognized taint kind " ^ other_str) in + set_attr pdesc prop_ path exp (Sil.Ataint { Sil.taint_source; taint_kind}) + | _ -> + (* note: we can also get this if [taint_kind] is not a string literal *) + raise (Exceptions.Wrong_argument_number __POS__) let execute___objc_cast { Builtin.pdesc; prop_; path; ret_ids; args; } : Builtin.ret_typ = diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index b3429d5bf..7b110aa7d 100644 --- a/infer/src/backend/tabulation.ml +++ b/infer/src/backend/tabulation.ml @@ -757,11 +757,13 @@ let add_tainting_att_param_list prop param_nums formal_params att = " to be set as tainted/untainted "); prop -(* Set Ataint attribute to list of parameteres in a prop *) +(* Set Ataint attribute to list of parameters in a prop *) let add_param_taint proc_name formal_params prop param_nums = let formal_params' = IList.map (fun (p, _) -> Sil.mk_pvar p proc_name) formal_params in - add_tainting_att_param_list prop param_nums formal_params' (Sil.Ataint proc_name) + (* TODO: add taint_kind as part of specification format in taint.ml *) + let taint_info = { Sil.taint_source = proc_name; taint_kind = Unknown; } in + add_tainting_att_param_list prop param_nums formal_params' (Sil.Ataint taint_info) (* add Auntaint attribute to a callee_pname precondition *) let mk_pre pre formal_params callee_pname = @@ -825,7 +827,7 @@ let mk_posts ret_ids prop callee_pname posts = let prop' = Prop.add_or_replace_exp_attribute prop_normal (Sil.Var ret_id) - (Sil.Ataint callee_pname) + (Sil.Ataint { Sil.taint_source = callee_pname; taint_kind = Unknown }) |> Prop.expose in (prop', path) in IList.map taint_retval posts @@ -874,10 +876,10 @@ let do_taint_check caller_pname callee_pname calling_pi missing_pi sub = the untaint atoms *) let report_taint_errors e (taint_atoms, _untaint_atoms) = let report_one_error taint_atom = - let tainting_fun = match Prop.atom_get_exp_attribute taint_atom with - | Some (_, Sil.Ataint pname) -> pname + 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 tainting_fun + let err_desc = Errdesc.explain_tainted_value_reaching_sensitive_function e taint_info callee_pname (State.get_loc ()) in let exn = Exceptions.Tainted_value_reaching_sensitive_function