supporting new @PrivacySource/PrivacySink annotations

Reviewed By: jeremydubreil

Differential Revision: D3180486

fb-gh-sync-id: 32f719e
fbshipit-source-id: 32f719e

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 *)

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)
+    add_tainting_att_param_list
-        (Taint.accepts_sensitive_params callee_pname) formal_params (Sil.Auntaint) in
+      (Prop.normalize pre)
-    (Prop.expose 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
+    exe_spec
-      spec actual_params formal_params in
+      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
 

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
 

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 =
+let returns_tainted callee_pname callee_attrs_opt =
-  IList.exists (fun pname -> Procname.equal pname callee_pname) sources
+  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 =
+let accepts_sensitive_params callee_pname callee_attrs_opt =
-  find_callee sinks callee_pname
+  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 *)

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 *)

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

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
 

infer/tests/build.xml

@@ -13,6 +13,7 @@
             <classpath>
               <pathelement location="../../dependencies/java/jackson/jackson-2.2.3.jar"/>
               <pathelement location="../lib/java/models.jar"/>
+              <pathelement location="../annotations//annotations.jar"/>
             </classpath>
         </javac>
     </target>

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",

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",

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(

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
+  }
+
 }

infer/tests/endtoend/java/infer/TaintTest.java

@@ -54,7 +54,10 @@ public class TaintTest {
         "interprocTaintErrorWithModelMethodsUndefined1",
         "interprocTaintErrorWithModelMethodsUndefined2",
         "interprocTaintErrorWithModelMethodsUndefined3",
-        "contentValuesPutWithTaintedString"
+        "contentValuesPutWithTaintedString",
+        "testPrivacySourceAnnot",
+        "testPrivacySinkAnnot1",
+        "testPrivacySinkAnnot3"
     };
 
     assertThat(