creating a framework for adding src/sink models based on method names/signatures alone

Reviewed By: jeremydubreil

Differential Revision: D2692136

fb-gh-sync-id: 12de038

infer/models/java/src/com/facebook/infer/models/InferTaint.java

@@ -0,0 +1,24 @@
+/*
+* Copyright (c) 2013 - present Facebook, Inc.
+* All rights reserved.
+*
+* This source code is licensed under the BSD style license found in the
+* LICENSE file in the root directory of this source tree. An additional grant
+* of patent rights can be found in the PATENTS file in the same directory.
+*/
+
+package com.facebook.infer.models;
+
+public class InferTaint {
+
+  public static Object inferSecretSource() {
+    Object o = InferUndefined.object_undefined();
+    InferBuiltins.assume_allocated(o);
+    return o;
+  }
+
+  public static void inferSensitiveSink(Object iMightBeTainted) {
+
+  }
+
+}

infer/src/backend/procname.mli

@@ -122,6 +122,8 @@ val is_class_initializer : t -> bool
 (** [is_infer_undefined pn] returns true if [pn] is a special Infer undefined proc *)
 val is_infer_undefined : t -> bool
 
+val split_classname : string -> string option * string
+
 (** Check if the procedure belongs to an anonymous inner class. *)
 val java_is_anonymous_inner_class : t -> bool
 

infer/src/backend/tabulation.ml

@@ -746,6 +746,35 @@ let combine
     print_results actual_pre (IList.map fst results);
     Some results
 
+let mk_pre pre formal_params callee_pname =
+  if !Config.taint_analysis then
+    match Taint.accepts_sensitive_params callee_pname with
+    | [] -> pre
+    | param_nums ->
+        let add_param_untaint prop param =
+          (* TODO: we should be able to add the taint attribute directly to the pvar. fix the taint
+             analysis so that it uses Prover.check_equal and gets the right answer here *)
+          IList.fold_left
+            (fun prop_acc hpred -> match hpred with
+               | Sil.Hpointsto (Sil.Lvar pvar, (Sil.Eexp (rhs, _)), _)
+                 when Sil.pvar_equal pvar param ->
+                   Prop.add_or_replace_exp_attribute prop_acc rhs Sil.Auntaint
+               | _ -> prop_acc)
+            prop
+            (Prop.get_sigma prop) in
+        let add_param_untaint_if_nums_match prop param_num param =
+          if IList.exists (fun num -> num = param_num) param_nums then
+            add_param_untaint prop param
+          else prop in
+        let pre', _ =
+          IList.fold_left
+            (fun (prop_acc, param_num) param ->
+               (add_param_untaint_if_nums_match prop_acc param_num param, param_num + 1))
+            (Prop.normalize pre, 0)
+            formal_params in
+        (Prop.expose pre')
+  else pre
+
 (** Construct the actual precondition: add to the current state a copy
     of the (callee's) formal parameters instantiated with the actual
     parameters. *)
@@ -766,6 +795,52 @@ 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 =
+  match ret_ids with
+  | [ret_id] ->
+      let mk_getter_idempotent posts =
+        (* if we have seen a previous call to the same function, only use specs whose return value
+           is consistent with constraints on the return value of the previous call w.r.t to
+           nullness. meant to eliminate false NPE warnings from the common
+           "if (get() != null) get().something()" pattern *)
+        let last_call_ret_non_null =
+          IList.exists
+            (fun (exp, attr) ->
+               match attr with
+               | Sil.Aretval pname when Procname.equal callee_pname pname ->
+                   Prover.check_disequal prop exp Sil.exp_zero
+               | _ -> false)
+            (Prop.get_all_attributes prop) in
+        if last_call_ret_non_null then
+          let returns_null prop =
+            IList.exists
+              (function
+                | Sil.Hpointsto (Sil.Lvar pvar, Sil.Eexp (e, _), _) when Sil.pvar_is_return pvar ->
+                    Prover.check_equal (Prop.normalize prop) e Sil.exp_zero
+                | _ -> false)
+              (Prop.get_sigma prop) in
+          IList.filter (fun (prop, _) -> not (returns_null prop)) posts
+        else posts in
+      let mk_retval_tainted posts =
+        if Taint.returns_secret callee_pname 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 callee_pname)
+              |> Prop.expose in
+            (prop', path) in
+          IList.map taint_retval posts
+        else posts in
+      let posts' =
+        if !Config.idempotent_getters && !Config.curr_language = Config.Java
+        then mk_getter_idempotent posts
+        else posts in
+      if !Config.taint_analysis then mk_retval_tainted posts' else posts'
+  | _ -> posts
+
+
 (** Check if actual_pre * missing_footprint |- false *)
 let inconsistent_actualpre_missing actual_pre split_opt =
   match split_opt with
@@ -881,34 +956,9 @@ let exe_spec
     tenv cfg ret_ids (n, nspecs) caller_pdesc callee_pname 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 =
-    match ret_ids with
-    | [ret_id] when !Config.idempotent_getters && !Config.curr_language = Config.Java ->
-        (* if we have seen a previous call to the same function, only use specs whose return value
-           is consistent with constraints on the return value of the previous call w.r.t to nullness.
-           meant to eliminate false NPE warnings from the common "if (get() != null) get().something()"
-           pattern *)
-        let last_call_ret_non_null =
-          IList.exists
-            (fun (exp, attr) ->
-               match attr with
-               | Sil.Aretval pname when Procname.equal callee_pname pname ->
-                   Prover.check_disequal prop exp Sil.exp_zero
-               | _ -> false)
-            (Prop.get_all_attributes prop) in
-        if last_call_ret_non_null then
-          let returns_null prop =
-            IList.exists
-              (function
-                | Sil.Hpointsto (Sil.Lvar pvar, Sil.Eexp (e, _), _) when Sil.pvar_is_return pvar ->
-                    Prover.check_equal (Prop.normalize prop) e Sil.exp_zero
-                | _ -> false)
-              (Prop.get_sigma prop) in
-          IList.filter (fun (prop, _) -> not (returns_null prop)) spec.Specs.posts
-        else spec.Specs.posts
-    | _ -> spec.Specs.posts in
+  let posts = mk_posts ret_ids prop callee_pname spec.Specs.posts in
   let actual_pre = mk_actual_precondition prop actual_params formal_params in
-  let spec_pre = Specs.Jprop.to_prop spec.Specs.pre in
+  let spec_pre = mk_pre (Specs.Jprop.to_prop spec.Specs.pre) formal_params callee_pname 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 ();

infer/src/harness/androidFramework.ml

@@ -13,6 +13,23 @@ module TypSet = Sil.TypSet
 
 open Utils
 
+type java_method_str = {
+  classname : string;
+  method_name : string;
+  ret_type : string;
+  params : string list;
+  is_static : bool
+}
+
+(* turn string specificiation of Java method into a procname *)
+let java_method_to_procname java_method =
+  Procname.mangled_java
+    (Procname.split_classname java_method.classname)
+    (Some (Procname.split_classname java_method.ret_type))
+    java_method.method_name
+    (IList.map Procname.split_classname java_method.params)
+    (if java_method.is_static then Procname.Static else Procname.Non_Static)
+
 (** Android lifecycle types and their lifecycle methods that are called by the framework *)
 
 (** work-in-progress list of known callback-registering method names *)

infer/src/harness/androidFramework.mli

@@ -11,6 +11,16 @@
 
 open Utils
 
+type java_method_str = {
+  classname : string;
+  method_name : string;
+  ret_type : string;
+  params : string list;
+  is_static : bool
+}
+
+val java_method_to_procname : java_method_str -> Procname.t
+
 (** return the complete list of (package, lifecycle_classname, lifecycle_methods) trios *)
 val get_lifecycles : (string * string * string list) list
 

infer/src/opensource/taint.ml

@@ -0,0 +1,18 @@
+(*
+ * Copyright (c) 2013 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ *)
+
+module L = Logging
+
+open Utils
+
+(** returns true if [callee_pname] returns a tainted value *)
+let returns_secret callee_pname = false
+
+(** returns list of zero-indexed argument numbers of [callee_pname] that may be tainted *)
+let accepts_sensitive_params callee_pname = []

infer/src/opensource/taint.mli

@@ -0,0 +1,14 @@
+(*
+ * Copyright (c) 2013 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ *)
+
+(** returns true if [callee_pname] returns a tainted value *)
+val returns_secret : Procname.t -> bool
+
+(** returns list of zero-indexed argument numbers of [callee_pname] that may be tainted *)
+val accepts_sensitive_params : Procname.t -> int list

infer/tests/ant_report.json

@@ -19,6 +19,21 @@
     "file": "codetoanalyze/java/infer/ContextLeaks.java",
     "procedure": "void ContextLeaks.indirectLeak()"
   },
+  {
+    "bug_type": "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION",
+    "file": "codetoanalyze/java/infer/TaintExample.java",
+    "procedure": "void TaintExample.interprocTaintErrorWithModelMethods1()"
+  },
+  {
+    "bug_type": "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION",
+    "file": "codetoanalyze/java/infer/TaintExample.java",
+    "procedure": "void TaintExample.interprocTaintErrorWithModelMethods2()"
+  },
+  {
+    "bug_type": "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION",
+    "file": "codetoanalyze/java/infer/TaintExample.java",
+    "procedure": "void TaintExample.interprocTaintErrorWithModelMethods3()"
+  },
   {
     "bug_type": "CONTEXT_LEAK",
     "file": "codetoanalyze/java/infer/ContextLeaks.java",
@@ -29,6 +44,11 @@
     "file": "codetoanalyze/java/infer/ContextLeaks.java",
     "procedure": "void ContextLeaks.nonStaticInnerClassLeak()"
   },
+  {
+    "bug_type": "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION",
+    "file": "codetoanalyze/java/infer/TaintExample.java",
+    "procedure": "void TaintExample.simpleTaintErrorWithModelMethods()"
+  },
   {
     "bug_type": "CONTEXT_LEAK",
     "file": "codetoanalyze/java/infer/ContextLeaks.java",

infer/tests/buck_report.json

@@ -19,6 +19,21 @@
     "file": "infer/tests/codetoanalyze/java/infer/ContextLeaks.java",
     "procedure": "void ContextLeaks.indirectLeak()"
   },
+  {
+    "bug_type": "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION",
+    "file": "infer/tests/codetoanalyze/java/infer/TaintExample.java",
+    "procedure": "void TaintExample.interprocTaintErrorWithModelMethods1()"
+  },
+  {
+    "bug_type": "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION",
+    "file": "infer/tests/codetoanalyze/java/infer/TaintExample.java",
+    "procedure": "void TaintExample.interprocTaintErrorWithModelMethods2()"
+  },
+  {
+    "bug_type": "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION",
+    "file": "infer/tests/codetoanalyze/java/infer/TaintExample.java",
+    "procedure": "void TaintExample.interprocTaintErrorWithModelMethods3()"
+  },
   {
     "bug_type": "CONTEXT_LEAK",
     "file": "infer/tests/codetoanalyze/java/infer/ContextLeaks.java",
@@ -29,6 +44,11 @@
     "file": "infer/tests/codetoanalyze/java/infer/ContextLeaks.java",
     "procedure": "void ContextLeaks.nonStaticInnerClassLeak()"
   },
+  {
+    "bug_type": "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION",
+    "file": "infer/tests/codetoanalyze/java/infer/TaintExample.java",
+    "procedure": "void TaintExample.simpleTaintErrorWithModelMethods()"
+  },
   {
     "bug_type": "CONTEXT_LEAK",
     "file": "infer/tests/codetoanalyze/java/infer/ContextLeaks.java",

infer/tests/codetoanalyze/java/infer/TaintExample.java

@@ -21,6 +21,8 @@ import javax.net.ssl.SSLSession;
 import javax.net.ssl.SSLSocket;
 import javax.net.ssl.SSLSocketFactory;
 
+import com.facebook.infer.models.InferTaint;
+
 public class TaintExample {
 
   public InputStream socketNotVerifiedSimple(SSLSocketFactory f)
@@ -106,4 +108,29 @@ public class TaintExample {
     return s.getInputStream();
   }
 
+  public void simpleTaintErrorWithModelMethods() {
+    Object o = InferTaint.inferSecretSource();
+    InferTaint.inferSensitiveSink(o);
+  }
+
+  public Object returnTaintedSourceModelMethods() {
+    return InferTaint.inferSecretSource();
+  }
+
+  public void callSinkMethodModelMethods(Object o) {
+    InferTaint.inferSensitiveSink(o);
+  }
+
+  public void interprocTaintErrorWithModelMethods1() {
+    InferTaint.inferSensitiveSink(returnTaintedSourceModelMethods());
+  }
+
+  public void interprocTaintErrorWithModelMethods2() {
+    callSinkMethodModelMethods(InferTaint.inferSecretSource());
+  }
+
+  public void interprocTaintErrorWithModelMethods3() {
+    callSinkMethodModelMethods(returnTaintedSourceModelMethods());
+  }
+
 }

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

@@ -46,6 +46,10 @@ public class TaintTest {
         "callReadInputStreamCauseTaintError",
         "taintingShouldNotPreventInference1",
         "taintingShouldNotPreventInference2",
+        "simpleTaintErrorWithModelMethods",
+        "interprocTaintErrorWithModelMethods1",
+        "interprocTaintErrorWithModelMethods2",
+        "interprocTaintErrorWithModelMethods3"
     };
 
     assertThat(