diff --git a/infer/models/java/src/com/facebook/infer/models/InferBuiltins.java b/infer/models/java/src/com/facebook/infer/models/InferBuiltins.java index 57c509df4..cd1b4d925 100644 --- a/infer/models/java/src/com/facebook/infer/models/InferBuiltins.java +++ b/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); } diff --git a/infer/models/java/src/java/lang/String.java b/infer/models/java/src/java/lang/String.java index 9600fa733..02755bb43 100644 --- a/infer/models/java/src/java/lang/String.java +++ b/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(); } } diff --git a/infer/models/java/src/java/net/Socket.java b/infer/models/java/src/java/net/Socket.java index d1af6551e..c0a692063 100644 --- a/infer/models/java/src/java/net/Socket.java +++ b/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(); } diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 90aa464e3..de48a3c51 100644 --- a/infer/src/backend/symExec.ml +++ b/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" *) diff --git a/infer/tests/ant_report.json b/infer/tests/ant_report.json index 843692c60..5d614b4a7 100644 --- a/infer/tests/ant_report.json +++ b/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", diff --git a/infer/tests/buck_report.json b/infer/tests/buck_report.json index 14c5d18d6..606715f19 100644 --- a/infer/tests/buck_report.json +++ b/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", diff --git a/infer/tests/codetoanalyze/java/infer/TaintExample.java b/infer/tests/codetoanalyze/java/infer/TaintExample.java index 4bc333cd7..a966bcff7 100644 --- a/infer/tests/codetoanalyze/java/infer/TaintExample.java +++ b/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) diff --git a/infer/tests/endtoend/java/infer/TaintTest.java b/infer/tests/endtoend/java/infer/TaintTest.java index 2bdeb2198..eff6bd493 100644 --- a/infer/tests/endtoend/java/infer/TaintTest.java +++ b/infer/tests/endtoend/java/infer/TaintTest.java @@ -60,7 +60,8 @@ public class TaintTest { "taintToStringStartsWith", "socketNotVerifiedSimple", "socketVerifiedForgotToCheckRetval", - "socketIgnoreExceptionNoVerify" + "socketIgnoreExceptionNoVerify", + "taintingShouldNotPreventInference" }; assertThat(