diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index cace1ed2a..0bcb3baa9 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -838,7 +838,7 @@ let add_constraints_on_retval pdesc prop ret_exp typ callee_pname callee_loc = (* 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 then + 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'' else prop'' else add_ret_non_null ret_exp typ prop @@ -1331,7 +1331,7 @@ and unknown_or_scan_call ~is_scan ret_type_option IList.fold_left do_exp prop actual_pars in let add_tainted_pre prop actuals caller_pname callee_pname = if !Config.taint_analysis then - match Taint.accepts_sensitive_params callee_pname with + match Taint.accepts_sensitive_params callee_pname None with | [] -> prop | param_nums -> let check_taint_if_nums_match (prop_acc, param_num) (actual_exp, _actual_typ) = @@ -1524,13 +1524,14 @@ and proc_call summary {Builtin.pdesc; tenv; prop_= pre; path; ret_ids; args= act check_return_value_ignored (); (* In case we call an objc instance method we add and extra spec *) (* were the receiver is null and the semantics of the call is nop*) + let callee_attrs = Specs.get_attributes summary in if (!Config.curr_language <> Config.Java) && !Config.objc_method_call_semantics && (Specs.get_attributes summary).ProcAttributes.is_objc_instance_method then handle_objc_method_call actual_pars actual_params pre tenv ret_ids pdesc callee_pname loc - path Tabulation.exe_function_call + path (Tabulation.exe_function_call callee_attrs) else (* non-objective-c method call. Standard tabulation *) Tabulation.exe_function_call - tenv ret_ids pdesc callee_pname loc actual_params pre path + callee_attrs tenv ret_ids pdesc callee_pname loc actual_params pre path end (** perform symbolic execution for a single prop, and check for junk *) diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index fba02fb07..74c9c8791 100644 --- a/infer/src/backend/tabulation.ml +++ b/infer/src/backend/tabulation.ml @@ -826,14 +826,16 @@ let add_param_taint proc_name formal_params prop param_nums = 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 = +let mk_pre pre formal_params callee_pname callee_attrs = if !Config.taint_analysis then - let pre' = add_tainting_att_param_list (Prop.normalize pre) - (Taint.accepts_sensitive_params callee_pname) formal_params (Sil.Auntaint) in - (Prop.expose pre') + add_tainting_att_param_list + (Prop.normalize pre) + (Taint.accepts_sensitive_params callee_pname (Some callee_attrs)) + formal_params + Sil.Auntaint + |> Prop.expose else pre - (** Construct the actual precondition: add to the current state a copy of the (callee's) formal parameters instantiated with the actual parameters. *) @@ -864,7 +866,7 @@ let mk_actual_precondition prop actual_params formal_params = let actual_pre = Prop.prop_sigma_star prop instantiated_formals in Prop.normalize actual_pre -let mk_posts ret_ids prop callee_pname posts = +let mk_posts ret_ids prop callee_pname callee_attrs posts = match ret_ids with | [ret_id] -> let mk_getter_idempotent posts = @@ -891,7 +893,7 @@ let mk_posts ret_ids prop callee_pname posts = IList.filter (fun (prop, _) -> not (returns_null prop)) posts else posts in let mk_retval_tainted posts = - if Taint.returns_tainted callee_pname then + if Taint.returns_tainted callee_pname (Some callee_attrs) then let taint_retval (prop, path) = let prop_normal = Prop.normalize prop in let prop' = @@ -1004,12 +1006,13 @@ let check_uninitialize_dangling_deref callee_pname actual_pre sub formal_params (** Perform symbolic execution for a single spec *) let exe_spec - tenv ret_ids (n, nspecs) caller_pdesc callee_pname loc prop path_pre + tenv ret_ids (n, nspecs) caller_pdesc callee_pname callee_attrs loc prop path_pre (spec : Prop.exposed Specs.spec) actual_params formal_params : abduction_res = let caller_pname = Cfg.Procdesc.get_proc_name caller_pdesc in - let posts = mk_posts ret_ids prop callee_pname spec.Specs.posts in + let posts = mk_posts ret_ids prop callee_pname callee_attrs spec.Specs.posts in let actual_pre = mk_actual_precondition prop actual_params formal_params in - let spec_pre = mk_pre (Specs.Jprop.to_prop spec.Specs.pre) formal_params callee_pname in + let spec_pre = + mk_pre (Specs.Jprop.to_prop spec.Specs.pre) formal_params callee_pname callee_attrs in L.d_strln ("EXECUTING SPEC " ^ string_of_int n ^ "/" ^ string_of_int nspecs); L.d_strln "ACTUAL PRECONDITION ="; L.d_increase_indent 1; Prop.d_prop actual_pre; L.d_decrease_indent 1; L.d_ln (); @@ -1262,7 +1265,8 @@ let exe_call_postprocess ret_ids trace_call callee_pname loc results = | _ -> res (** Execute the function call and return the list of results with return value *) -let exe_function_call tenv ret_ids caller_pdesc callee_pname loc actual_params prop path = +let exe_function_call + callee_attrs tenv ret_ids caller_pdesc callee_pname loc actual_params prop path = let caller_pname = Cfg.Procdesc.get_proc_name caller_pdesc in let trace_call res = match Specs.get_summary caller_pname with @@ -1280,8 +1284,19 @@ let exe_function_call tenv ret_ids caller_pdesc callee_pname loc actual_params p L.d_strln ("START EXECUTING SPECS FOR " ^ Procname.to_string callee_pname ^ " from state"); Prop.d_prop prop; L.d_ln (); let exe_one_spec (n, spec) = - exe_spec tenv ret_ids (n, nspecs) caller_pdesc callee_pname loc prop path - spec actual_params formal_params in + exe_spec + tenv + ret_ids + (n, nspecs) + caller_pdesc + callee_pname + callee_attrs + loc + prop + path + spec + actual_params + formal_params in let results = IList.map exe_one_spec spec_list in exe_call_postprocess ret_ids trace_call callee_pname loc results diff --git a/infer/src/backend/tabulation.mli b/infer/src/backend/tabulation.mli index 8879d0397..6764c23bb 100644 --- a/infer/src/backend/tabulation.mli +++ b/infer/src/backend/tabulation.mli @@ -44,7 +44,7 @@ val d_splitting : splitting -> unit (** Execute the function call and return the list of results with return value *) val exe_function_call: - Tenv.t -> Ident.t list -> Cfg.Procdesc.t -> Procname.t -> Location.t -> + ProcAttributes.t -> Tenv.t -> Ident.t list -> Cfg.Procdesc.t -> Procname.t -> Location.t -> (Sil.exp * Sil.typ) list -> Prop.normal Prop.t -> Paths.Path.t -> (Prop.normal Prop.t * Paths.Path.t) list diff --git a/infer/src/backend/taint.ml b/infer/src/backend/taint.ml index e6e1c3348..dbac185d2 100644 --- a/infer/src/backend/taint.ml +++ b/infer/src/backend/taint.ml @@ -216,15 +216,21 @@ let mk_pname_param_num methods = (fun (mname, param_num) -> method_str_to_pname mname, param_num) methods -let sinks = +let taint_sinks = mk_pname_param_num sinks let func_with_tainted_params = mk_pname_param_num functions_with_tainted_params +let attrs_opt_get_annots = function + | Some attrs -> attrs.ProcAttributes.method_annotation + | None -> Sil.method_annotation_empty + (** returns true if [callee_pname] returns a tainted value *) -let returns_tainted callee_pname = - IList.exists (fun pname -> Procname.equal pname callee_pname) sources +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 let find_callee methods callee_pname = try @@ -232,8 +238,15 @@ let find_callee methods callee_pname = with Not_found -> [] (** returns list of zero-indexed argument numbers of [callee_pname] that may be tainted *) -let accepts_sensitive_params callee_pname = - find_callee sinks callee_pname +let accepts_sensitive_params callee_pname callee_attrs_opt = + match find_callee taint_sinks callee_pname with + | [] -> + let _, param_annots = attrs_opt_get_annots callee_attrs_opt in + let offset = if Procname.java_is_static callee_pname then 0 else 1 in + IList.mapi (fun param_num attr -> (param_num + offset, attr)) param_annots + |> IList.filter (fun (_, attr) -> Annotations.ia_is_privacy_sink attr) + |> IList.map fst + | tainted_params -> tainted_params (** returns list of zero-indexed parameter numbers of [callee_pname] that should be considered tainted during symbolic execution *) diff --git a/infer/src/backend/taint.mli b/infer/src/backend/taint.mli index 3462c4f35..10ead5e0c 100644 --- a/infer/src/backend/taint.mli +++ b/infer/src/backend/taint.mli @@ -10,10 +10,10 @@ open! Utils (** returns true if [callee_pname] returns a tainted value *) -val returns_tainted : Procname.t -> bool +val returns_tainted : Procname.t -> ProcAttributes.t option -> bool (** returns list of zero-indexed argument numbers of [callee_pname] that may be tainted *) -val accepts_sensitive_params : Procname.t -> int list +val accepts_sensitive_params : Procname.t -> ProcAttributes.t option -> int list (** returns list of zero-indexed parameter numbers of [callee_pname] that should be considered tainted during symbolic execution *) diff --git a/infer/src/checkers/annotations.ml b/infer/src/checkers/annotations.ml index dc5059a3a..89ddbd701 100644 --- a/infer/src/checkers/annotations.ml +++ b/infer/src/checkers/annotations.ml @@ -126,6 +126,8 @@ let performance_critical = "PerformanceCritical" let no_allocation = "NoAllocation" let ignore_allocations = "IgnoreAllocations" let suppress_warnings = "SuppressWarnings" +let privacy_source = "PrivacySource" +let privacy_sink = "PrivacySink" let ia_is_nullable ia = ia_ends_with ia nullable @@ -201,6 +203,11 @@ let ia_is_ignore_allocations ia = let ia_is_suppress_warnings ia = ia_ends_with ia suppress_warnings +let ia_is_privacy_source ia = + ia_ends_with ia privacy_source + +let ia_is_privacy_sink ia = + ia_ends_with ia privacy_sink type annotation = | Nullable diff --git a/infer/src/checkers/annotations.mli b/infer/src/checkers/annotations.mli index 97a579848..49ada3600 100644 --- a/infer/src/checkers/annotations.mli +++ b/infer/src/checkers/annotations.mli @@ -89,6 +89,8 @@ val ia_is_performance_critical : Sil.item_annotation -> bool val ia_is_no_allocation : Sil.item_annotation -> bool val ia_is_ignore_allocations : Sil.item_annotation -> bool val ia_is_suppress_warnings : Sil.item_annotation -> bool +val ia_is_privacy_source : Sil.item_annotation -> bool +val ia_is_privacy_sink : Sil.item_annotation -> bool val ia_iter : (Sil.annotation -> unit) -> Sil.item_annotation -> unit diff --git a/infer/tests/build.xml b/infer/tests/build.xml index 4ff63505d..ea55d3672 100644 --- a/infer/tests/build.xml +++ b/infer/tests/build.xml @@ -13,6 +13,7 @@ + diff --git a/infer/tests/build_systems/expected_outputs/ant_report.json b/infer/tests/build_systems/expected_outputs/ant_report.json index 47990ee44..468c291f7 100644 --- a/infer/tests/build_systems/expected_outputs/ant_report.json +++ b/infer/tests/build_systems/expected_outputs/ant_report.json @@ -109,6 +109,21 @@ "file": "codetoanalyze/java/infer/TaintExample.java", "procedure": "InputStream TaintExample.taintingShouldNotPreventInference2(SSLSocketFactory)" }, + { + "bug_type": "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION", + "file": "codetoanalyze/java/infer/TaintExample.java", + "procedure": "void TaintExample.testPrivacySinkAnnot1()" + }, + { + "bug_type": "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION", + "file": "codetoanalyze/java/infer/TaintExample.java", + "procedure": "void TaintExample.testPrivacySinkAnnot3()" + }, + { + "bug_type": "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION", + "file": "codetoanalyze/java/infer/TaintExample.java", + "procedure": "void TaintExample.testPrivacySourceAnnot()" + }, { "bug_type": "NULL_DEREFERENCE", "file": "codetoanalyze/java/infer/NullPointerExceptions.java", diff --git a/infer/tests/build_systems/expected_outputs/buck_report.json b/infer/tests/build_systems/expected_outputs/buck_report.json index 22574d881..95815ac36 100644 --- a/infer/tests/build_systems/expected_outputs/buck_report.json +++ b/infer/tests/build_systems/expected_outputs/buck_report.json @@ -109,6 +109,21 @@ "file": "infer/tests/codetoanalyze/java/infer/TaintExample.java", "procedure": "InputStream TaintExample.taintingShouldNotPreventInference2(SSLSocketFactory)" }, + { + "bug_type": "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION", + "file": "infer/tests/codetoanalyze/java/infer/TaintExample.java", + "procedure": "void TaintExample.testPrivacySinkAnnot1()" + }, + { + "bug_type": "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION", + "file": "infer/tests/codetoanalyze/java/infer/TaintExample.java", + "procedure": "void TaintExample.testPrivacySinkAnnot3()" + }, + { + "bug_type": "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION", + "file": "infer/tests/codetoanalyze/java/infer/TaintExample.java", + "procedure": "void TaintExample.testPrivacySourceAnnot()" + }, { "bug_type": "NULL_DEREFERENCE", "file": "infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java", diff --git a/infer/tests/codetoanalyze/java/infer/BUCK b/infer/tests/codetoanalyze/java/infer/BUCK index b8920e7dc..388a14acf 100644 --- a/infer/tests/codetoanalyze/java/infer/BUCK +++ b/infer/tests/codetoanalyze/java/infer/BUCK @@ -3,7 +3,8 @@ sources = glob(['**/*.java']) dependencies = [ '//infer/lib/java/android:android', '//dependencies/java/jackson:jackson', - '//infer/lib/java:models' + '//infer/lib/java:models', + '//infer/annotations:annotations', ] java_library( diff --git a/infer/tests/codetoanalyze/java/infer/TaintExample.java b/infer/tests/codetoanalyze/java/infer/TaintExample.java index 541c4ef1f..df2bcc810 100644 --- a/infer/tests/codetoanalyze/java/infer/TaintExample.java +++ b/infer/tests/codetoanalyze/java/infer/TaintExample.java @@ -25,6 +25,8 @@ import android.content.ContentValues; import android.content.SharedPreferences; import com.facebook.infer.models.InferTaint; +import com.facebook.infer.annotation.PrivacySource; +import com.facebook.infer.annotation.PrivacySink; public class TaintExample { @@ -170,4 +172,39 @@ public class TaintExample { values.put(key, value); } + @PrivacySource("") + public String privacySource() { + return "source"; + } + + public void testPrivacySourceAnnot() { + InferTaint.inferSensitiveSinkUndefined(privacySource()); // should report + } + + public void instancePrivacySink(@PrivacySink("") String s1, String s2) { + } + + public static void staticPrivacySink(@PrivacySink("") String s1, String s2) { + } + + public void testPrivacySinkAnnot1() { + String source = privacySource(); + instancePrivacySink(source, ""); // should report + } + + public void testPrivacySinkAnnot2() { + String source = privacySource(); + instancePrivacySink("", source); // should not report + } + + public void testPrivacySinkAnnot3() { + String source = privacySource(); + staticPrivacySink(source, ""); // should report + } + + public void testPrivacySinkAnnot4() { + String source = privacySource(); + staticPrivacySink("", source); // should not report + } + } diff --git a/infer/tests/endtoend/java/infer/TaintTest.java b/infer/tests/endtoend/java/infer/TaintTest.java index 65e0d4a10..a3890e062 100644 --- a/infer/tests/endtoend/java/infer/TaintTest.java +++ b/infer/tests/endtoend/java/infer/TaintTest.java @@ -54,7 +54,10 @@ public class TaintTest { "interprocTaintErrorWithModelMethodsUndefined1", "interprocTaintErrorWithModelMethodsUndefined2", "interprocTaintErrorWithModelMethodsUndefined3", - "contentValuesPutWithTaintedString" + "contentValuesPutWithTaintedString", + "testPrivacySourceAnnot", + "testPrivacySinkAnnot1", + "testPrivacySinkAnnot3" }; assertThat(