diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 0bcb3baa9..b8f6bf212 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -843,6 +843,27 @@ let add_constraints_on_retval pdesc prop ret_exp typ callee_pname callee_loc = else prop'' else add_ret_non_null ret_exp typ prop +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 + Prop.add_or_replace_exp_attribute prop (Sil.Var lhs_id) (Sil.Ataint taint_info) + else + prop in + match rhs_exp with + | Sil.Lfield (_, fieldname, Tptr (Tstruct struct_typ, _)) + | Sil.Lfield (_, fieldname, Tstruct struct_typ) -> + add_attribute_if_field_tainted prop fieldname struct_typ + | Sil.Lfield (_, fieldname, Tptr (Tvar typname, _)) + | Sil.Lfield (_, fieldname, Tvar typname) -> + begin + match Tenv.lookup tenv typname with + | Some struct_typ -> add_attribute_if_field_tainted prop fieldname struct_typ + | None -> prop + end + | _ -> prop + let execute_letderef ?(report_deref_errors=true) pname pdesc tenv id rhs_exp typ loc prop_ = let execute_letderef_ pdesc tenv id loc acc_in iter = let iter_ren = Prop.prop_iter_make_id_primed id iter in @@ -860,7 +881,11 @@ let execute_letderef ?(report_deref_errors=true) pname pdesc tenv id rhs_exp typ if lookup_uninitialized then Prop.add_or_replace_exp_attribute prop' (Sil.Var id) (Sil.Adangling Sil.DAuninit) else prop' in - prop'' :: acc in + let prop''' = + if !Config.taint_analysis + then add_taint prop'' id rhs_exp pname tenv + else prop'' in + prop''' :: acc in begin match pred_insts_op with | None -> update acc_in ([],[]) diff --git a/infer/src/backend/taint.ml b/infer/src/backend/taint.ml index dbac185d2..29855310d 100644 --- a/infer/src/backend/taint.ml +++ b/infer/src/backend/taint.ml @@ -252,3 +252,10 @@ let accepts_sensitive_params callee_pname callee_attrs_opt = considered tainted during symbolic execution *) let tainted_params callee_pname = find_callee func_with_tainted_params callee_pname + +let has_taint_annotation fieldname struct_typ = + let fld_has_taint_annot (fname, _, annot) = + Ident.fieldname_equal fieldname fname && + Annotations.ia_is_privacy_source annot in + IList.exists fld_has_taint_annot struct_typ.Sil.instance_fields || + IList.exists fld_has_taint_annot struct_typ.Sil.static_fields diff --git a/infer/src/backend/taint.mli b/infer/src/backend/taint.mli index 10ead5e0c..d665b7d56 100644 --- a/infer/src/backend/taint.mli +++ b/infer/src/backend/taint.mli @@ -18,3 +18,6 @@ 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 *) val tainted_params : Procname.t -> int list + +(** returns true if [fieldname] has a taint source annotation *) +val has_taint_annotation : Ident.fieldname -> Sil.struct_typ -> bool diff --git a/infer/tests/build_systems/expected_outputs/ant_report.json b/infer/tests/build_systems/expected_outputs/ant_report.json index ae44d15c9..5417b226b 100644 --- a/infer/tests/build_systems/expected_outputs/ant_report.json +++ b/infer/tests/build_systems/expected_outputs/ant_report.json @@ -124,6 +124,21 @@ "file": "codetoanalyze/java/infer/TaintExample.java", "procedure": "void TaintExample.testPrivacySourceAnnot()" }, + { + "bug_type": "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION", + "file": "codetoanalyze/java/infer/TaintExample.java", + "procedure": "void TaintExample.testPrivacySourceFieldAnnotPropagation()" + }, + { + "bug_type": "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION", + "file": "codetoanalyze/java/infer/TaintExample.java", + "procedure": "void TaintExample.testPrivacySourceInstanceFieldAnnot()" + }, + { + "bug_type": "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION", + "file": "codetoanalyze/java/infer/TaintExample.java", + "procedure": "void TaintExample.testPrivacySourceStaticFieldAnnot()" + }, { "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 fcf8d7ec4..ce87f21f6 100644 --- a/infer/tests/build_systems/expected_outputs/buck_report.json +++ b/infer/tests/build_systems/expected_outputs/buck_report.json @@ -124,6 +124,21 @@ "file": "infer/tests/codetoanalyze/java/infer/TaintExample.java", "procedure": "void TaintExample.testPrivacySourceAnnot()" }, + { + "bug_type": "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION", + "file": "infer/tests/codetoanalyze/java/infer/TaintExample.java", + "procedure": "void TaintExample.testPrivacySourceFieldAnnotPropagation()" + }, + { + "bug_type": "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION", + "file": "infer/tests/codetoanalyze/java/infer/TaintExample.java", + "procedure": "void TaintExample.testPrivacySourceInstanceFieldAnnot()" + }, + { + "bug_type": "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION", + "file": "infer/tests/codetoanalyze/java/infer/TaintExample.java", + "procedure": "void TaintExample.testPrivacySourceStaticFieldAnnot()" + }, { "bug_type": "NULL_DEREFERENCE", "file": "infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java", diff --git a/infer/tests/codetoanalyze/java/infer/TaintExample.java b/infer/tests/codetoanalyze/java/infer/TaintExample.java index df2bcc810..ee9cd069b 100644 --- a/infer/tests/codetoanalyze/java/infer/TaintExample.java +++ b/infer/tests/codetoanalyze/java/infer/TaintExample.java @@ -207,4 +207,25 @@ public class TaintExample { staticPrivacySink("", source); // should not report } + @PrivacySource("") String mPrivacySource; + + @PrivacySource("") String sPrivacySource; + + public void testPrivacySourceInstanceFieldAnnot() { + String source = mPrivacySource; + InferTaint.inferSensitiveSinkUndefined(source); // should report + } + + public void testPrivacySourceStaticFieldAnnot() { + String source = sPrivacySource; + InferTaint.inferSensitiveSinkUndefined(source); // should report + } + + String aFieldWithoutAnnotations; + + public void testPrivacySourceFieldAnnotPropagation() { + aFieldWithoutAnnotations = mPrivacySource; + InferTaint.inferSensitiveSinkUndefined(aFieldWithoutAnnotations); // should report + } + } diff --git a/infer/tests/endtoend/java/infer/TaintTest.java b/infer/tests/endtoend/java/infer/TaintTest.java index a3890e062..cfefd4113 100644 --- a/infer/tests/endtoend/java/infer/TaintTest.java +++ b/infer/tests/endtoend/java/infer/TaintTest.java @@ -57,7 +57,10 @@ public class TaintTest { "contentValuesPutWithTaintedString", "testPrivacySourceAnnot", "testPrivacySinkAnnot1", - "testPrivacySinkAnnot3" + "testPrivacySinkAnnot3", + "testPrivacySourceInstanceFieldAnnot", + "testPrivacySourceStaticFieldAnnot", + "testPrivacySourceFieldAnnotPropagation", }; assertThat(