fixing taint analysis so it doesn't prevent postcondition inference

Reviewed By: jeremydubreil

Differential Revision: D2675121

fb-gh-sync-id: ee559ca

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

@@ -35,7 +35,10 @@ 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_untaint_attribute(Object o);
-    public native static boolean __state_untainted(Object o);
+
+    // report an error if o is tainted, then assume UNTAINT(o) going forward
+    public native static void __check_untainted(Object o);
 
 }

infer/models/java/src/java/lang/String.java

@@ -56,22 +56,22 @@ public final class String {
 
 
     public boolean equals(Object anObject) {
-        InferBuiltins.assume(!InferBuiltins.__state_untainted(anObject));
+        InferBuiltins.__check_untainted(anObject);
         return this == anObject;
     }
 
     public int compareTo(String aString) {
-        InferBuiltins.assume(!InferBuiltins.__state_untainted(aString));
+        InferBuiltins.__check_untainted(aString);
         return InferUndefined.nonneg_int();
     }
 
     public boolean endsWith(String aString) {
-        InferBuiltins.assume(!InferBuiltins.__state_untainted(aString));
+        InferBuiltins.__check_untainted(aString);
         return InferUndefined.boolean_undefined();
     }
 
     public boolean startsWith(String aString) {
-        InferBuiltins.assume(!InferBuiltins.__state_untainted(aString));
+        InferBuiltins.__check_untainted(aString);
         return InferUndefined.boolean_undefined();
     }
 }

infer/models/java/src/java/net/Socket.java

@@ -67,12 +67,12 @@ public class Socket {
     }
 
     public InputStream getInputStream() throws IOException {
-      InferBuiltins.assume(!InferBuiltins.__state_untainted(this));
+      InferBuiltins.__check_untainted(this);
       return ((PlainSocketImpl) impl).getInputStream();
     }
 
     public OutputStream getOutputStream() throws IOException {
-      InferBuiltins.assume(!InferBuiltins.__state_untainted(this));
+      InferBuiltins.__check_untainted(this);
       return ((PlainSocketImpl) impl).getOutputStream();
     }
 

infer/src/backend/symExec.ml

@@ -1826,6 +1826,27 @@ module ModelBuiltins = struct
         [(prop', path)]
     | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
 
+  (** report an error if [lexp] is tainted; otherwise, add untained([lexp]) as a precondition *)
+  let execute___check_untainted cfg pdesc instr tenv prop path ret_ids args callee_pname loc
+    : Builtin.ret_typ =
+    match args, ret_ids with
+    | [(lexp, typ)], _ ->
+        let pname = Cfg.Procdesc.get_proc_name pdesc in
+        let n_lexp, prop = exp_norm_check_arith pname prop lexp in
+        (match Prop.get_taint_attribute prop n_lexp with
+         | Some (Sil.Ataint source_pname) ->
+             (* since set_taint_attribute and assert_untained are only used in the models, we should
+                never encounter this case (unless someone is silly enough to write
+                set_taint_attribute(o); check_untainted(o) in a model.) *)
+             failwith "Don't write set_taint_attribute(o); ...check_untainted(o) in the same method"
+         | _ ->
+             if !Config.footprint then
+               let untaint_attr = Sil.Const (Sil.Cattribute (Sil.Auntaint)) in
+               (** add untained(n_lexp) to the footprint *)
+               [(Prop.conjoin_neq ~footprint:true n_lexp untaint_attr prop, path)]
+             else [(prop, path)])
+    | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
+
   (** take a pointer to a struct, and return the value of a hidden field in the struct *)
   let execute___get_hidden_field cfg pdesc instr tenv _prop path ret_ids args callee_name loc
     : Builtin.ret_typ =
@@ -1891,18 +1912,6 @@ module ModelBuiltins = struct
         [(prop'', path)]
     | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
 
-  let execute___state_untainted cfg pdesc instr tenv _prop path ret_ids args callee_name loc
-    : Builtin.ret_typ =
-    match args with
-    | [(lexp, typ)] when IList.length ret_ids <= 1 ->
-        let pname = Cfg.Procdesc.get_proc_name pdesc in
-        (match ret_ids with
-         | [ret_id] ->
-             let n_lexp, prop = exp_norm_check_arith pname _prop lexp in
-             [(return_result (Sil.BinOp(Sil.Ne, n_lexp, (Sil.Const(Sil.Cattribute((Sil.Auntaint)))))) prop ret_ids, path)]
-         | _ -> [(_prop, path)])
-    | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
-
   (* Update the objective-c hidden counter by applying the operation op and the operand delta.*)
   (* Eg. op=+/- delta is an integer *)
   let execute___objc_counter_update
@@ -2250,7 +2259,7 @@ module ModelBuiltins = struct
     match args with
     | [(lexp, typ)] ->
         let prop_assume = Prop.conjoin_eq lexp (Sil.exp_bool true) prop in
-        if Prover.check_inconsistency prop_assume then execute_diverge prop_assume path
+        if Prover.check_inconsistency prop_assume then  execute_diverge prop_assume path
         else [(prop_assume, path)]
     | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
 
@@ -2320,7 +2329,7 @@ module ModelBuiltins = struct
   let _ = Builtin.register "__set_hidden_field" execute___set_hidden_field  (* set a hidden field in the struct to the given value *)
   let _ = Builtin.register "__set_taint_attribute" execute___set_taint_attribute (* set the attribute of the parameter as tainted *)
   let _ = Builtin.register "__set_untaint_attribute" execute___set_untaint_attribute (* set the attribute of the parameter as tainted *)
-  let _ = Builtin.register "__state_untainted" execute___state_untainted (* check if the parameter is tainted *)
+  let _ = Builtin.register "__check_untainted" execute___check_untainted (* report a taint error if the parameter is tainted, and assume it is untainted afterward *)
   let __objc_retain = Builtin.register "__objc_retain" execute___objc_retain (* objective-c "retain" *)
   let __objc_release = Builtin.register "__objc_release" execute___objc_release (* objective-c "release" *)
   let __objc_retain_cf = Builtin.register "__objc_retain_cf" execute___objc_retain_cf (* objective-c "retain" *)

infer/tests/ant_report.json

@@ -144,6 +144,11 @@
     "file": "codetoanalyze/java/infer/TaintExample.java",
     "bug_type": "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION"
   },
+  {
+    "procedure": "InputStream TaintExample.taintingShouldNotPreventInference(SSLSocketFactory)",
+    "file": "codetoanalyze/java/infer/TaintExample.java",
+    "bug_type": "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION"
+  },
   {
     "procedure": "int NullPointerExceptions.NPEvalueOfFromHashmapBad(HashMap,int)",
     "file": "codetoanalyze/java/infer/NullPointerExceptions.java",

infer/tests/buck_report.json

@@ -144,6 +144,11 @@
     "file": "infer/tests/codetoanalyze/java/infer/TaintExample.java",
     "bug_type": "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION"
   },
+  {
+    "procedure": "InputStream TaintExample.taintingShouldNotPreventInference(SSLSocketFactory)",
+    "file": "infer/tests/codetoanalyze/java/infer/TaintExample.java",
+    "bug_type": "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION"
+  },
   {
     "procedure": "int NullPointerExceptions.NPEvalueOfFromHashmapBad(HashMap,int)",
     "file": "infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java",

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

@@ -267,6 +267,15 @@ public class TaintExample {
     return socket.getInputStream();
   }
 
+  public InputStream taintingShouldNotPreventInference(SSLSocketFactory f)
+    throws IOException {
+
+    socketNotVerifiedSimple(f).toString();
+    // failing to infer a post for socketNotVerifiedSimple will hide this error
+    Socket socket = f.createSocket();
+    return socket.getInputStream();
+  }
+
   public InputStream socketVerifiedForgotToCheckRetval(SSLSocketFactory f,
                                                        HostnameVerifier v,
                                                        SSLSession session)

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

@@ -60,7 +60,8 @@ public class TaintTest {
         "taintToStringStartsWith",
         "socketNotVerifiedSimple",
         "socketVerifiedForgotToCheckRetval",
-        "socketIgnoreExceptionNoVerify"
+        "socketIgnoreExceptionNoVerify",
+        "taintingShouldNotPreventInference"
     };
 
     assertThat(