From 29ea879930341fbdc43882a8df0ad6da7e2ebd55 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Tue, 24 Nov 2015 13:07:47 -0800 Subject: [PATCH] eliminating precondition not met in taint analysis Reviewed By: jeremydubreil Differential Revision: D2678195 fb-gh-sync-id: f058626 --- infer/src/backend/tabulation.ml | 95 ++++++++++++------- infer/tests/ant_report.json | 14 ++- infer/tests/buck_report.json | 14 ++- .../java/infer/TaintExample.java | 35 +++++-- .../tests/endtoend/java/infer/TaintTest.java | 8 +- 5 files changed, 115 insertions(+), 51 deletions(-) diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index be0c9a161..51c34f58b 100644 --- a/infer/src/backend/tabulation.ml +++ b/infer/src/backend/tabulation.ml @@ -766,58 +766,83 @@ let inconsistent_actualpre_missing actual_pre split_opt = | None -> false (* Collect the taint/untain info on the pi part *) +(* TODO (t9199155): this be done with a single traversal of the list of atoms/combined with + intersection_taint_untaint to be much more efficient *) let rec get_taint_untaint pi = - let get_att_exp p e (t,u) = + let get_att_exp p e (t,u) atom = match Prop.get_taint_attribute p e with | Some(Sil.Ataint _) -> L.d_str " ---->Found TAINTED exp: "; Sil.d_exp e; L.d_ln (); - (e::t, u) + ((e, atom)::t, u) | Some(Sil.Auntaint) -> L.d_str " ---->Found UNTAINTED exp: "; Sil.d_exp e; L.d_ln (); - (t, e::u) + (t, (e, atom)::u) | _ -> (t,u) in match pi with | [] -> ([],[]) - | Sil.Aneq (e1, e2):: pi' -> + | (Sil.Aneq (e1, e2) as atom) :: pi' -> let (t, u) = get_taint_untaint pi' in - let p = Prop.replace_pi [Sil.Aneq (e1, e2)] Prop.prop_emp in - let (t',u') = get_att_exp p e1 (t,u) in - get_att_exp p e2 (t',u') + let p = Prop.replace_pi [atom] Prop.prop_emp in + let (t',u') = get_att_exp p e1 (t,u) atom in + get_att_exp p e2 (t',u') atom | _ :: pi' -> get_taint_untaint pi' (* perform the taint analysis check by comparing in a function call the actual calling state and the missing pi computed by abduction *) let do_taint_check caller_pname callee_pname calling_prop missing_pi sub prop = - (* Note: returns only the first element in the intersection*) - let rec intersection_taint_untaint taint untaint = + let rec intersection_taint_untaint taint untaint acc = match taint with - | [] -> None - | e:: taint' -> if (IList.exists (fun e' -> Sil.exp_equal e e') untaint) then (Some e) - else intersection_taint_untaint taint' untaint in + | [] -> acc + | (e1, atom_taint) :: taint' -> + let acc' = + try + let (e2, atom_untaint) = + IList.find (fun (e2, _) -> Sil.exp_equal e1 e2) untaint in + (e1, atom_taint, atom_untaint) :: acc + with Not_found -> acc in + intersection_taint_untaint taint' untaint acc' in let combined_calling_prop = Prop.replace_pi ((Prop.get_pi calling_prop) @ missing_pi) calling_prop in let sub_combined_calling_prop = Prop.prop_sub sub combined_calling_prop in let taint_set, untaint_set = get_taint_untaint (Prop.get_pi sub_combined_calling_prop) in L.d_str "Actual pre combined with missing pi: "; Prop.d_prop sub_combined_calling_prop; L.d_ln(); - L.d_str "Taint set: "; Sil.d_exp_list taint_set; L.d_ln (); - L.d_str "Untaint set: "; Sil.d_exp_list untaint_set; L.d_ln (); - match intersection_taint_untaint taint_set untaint_set with - | None -> L.d_str "NO taint error detected"; L.d_ln(); - | Some e -> begin - L.d_str "Taint error detected!"; L.d_ln(); - let e' = match Errdesc.find_pvar_with_exp prop e with - | Some (pv, _) -> Sil.Lvar pv - | None -> e in - let tainting_fun = match Prop.get_taint_attribute prop e with - | Some (Sil.Ataint tf) -> tf - | _ -> Procname.empty (* by definition of e, we should not get to this case *) in - let err_desc = Errdesc.explain_tainted_value_reaching_sensitive_function e' tainting_fun - callee_pname (State.get_loc ()) in - let exn = - Exceptions.Tainted_value_reaching_sensitive_function - (err_desc, try assert false with Assert_failure x -> x) in - Reporting.log_warning caller_pname exn - end + L.d_str "Taint set: "; Sil.d_exp_list (fst (IList.split taint_set)); L.d_ln (); + L.d_str "Untaint set: "; Sil.d_exp_list (fst (IList.split untaint_set)); L.d_ln (); + let report_taint_error (e, _, _) = + L.d_str "Taint error detected!"; L.d_ln(); + let e' = match Errdesc.find_pvar_with_exp prop e with + | Some (pv, _) -> Sil.Lvar pv + | None -> e in + let tainting_fun = match Prop.get_taint_attribute prop e with + | Some (Sil.Ataint tf) -> tf + | _ -> Procname.empty (* by definition of e, we should not get to this case *) in + let err_desc = Errdesc.explain_tainted_value_reaching_sensitive_function e' tainting_fun + callee_pname (State.get_loc ()) in + let exn = + Exceptions.Tainted_value_reaching_sensitive_function + (err_desc, try assert false with Assert_failure x -> x) in + Reporting.log_warning caller_pname exn in + match intersection_taint_untaint taint_set untaint_set [] with + | [] -> + L.d_str "NO taint error detected"; L.d_ln(); + missing_pi + | taint_errors -> + IList.iter report_taint_error taint_errors; + (* get a version of [missing_pi] whose var names match names in taint_errors *) + let missing_pi_sub = + Prop.get_pi (Prop.prop_sub sub (Prop.replace_pi missing_pi Prop.prop_emp)) in + (* filter out UNTAINT(e) atoms from [missing_pi] such that we have already reported a taint + error on e. without doing this, we will get PRECONDITION_NOT_MET (and failed spec + inference), which is bad. instead, what this does is effectively assume that the UNTAINT(e) + precondition was met, and contine with the analysis under this assumption. this makes sense + because we are reporting the taint error, but propagating a *safe* postcondition w.r.t to + tainting. *) + IList.filter + (fun atom -> not + (IList.exists + (fun (_, _, atom_untaint) -> Sil.atom_equal atom atom_untaint) + taint_errors)) + missing_pi_sub let class_cast_exn pname_opt texp1 texp2 exp ml_location = let desc = Errdesc.explain_class_cast_exception pname_opt texp1 texp2 exp (State.get_node ()) (State.get_loc ()) in @@ -887,7 +912,11 @@ let exe_spec let exn = get_check_exn check callee_pname loc (try assert false with Assert_failure x -> x) in Reporting.log_warning caller_pname exn in let do_split () = - let split = process_splitting actual_pre sub1 sub2 frame missing_pi missing_sigma frame_fld missing_fld frame_typ missing_typ in + let missing_pi' = + if !Config.taint_analysis then + do_taint_check caller_pname callee_pname actual_pre missing_pi sub2 prop + else missing_pi in + let split = process_splitting actual_pre sub1 sub2 frame missing_pi' missing_sigma frame_fld missing_fld frame_typ missing_typ in d_splitting split; L.d_ln (); let norm_missing_pi = Prop.pi_sub split.sub split.missing_pi in let norm_missing_sigma = Prop.sigma_sub split.sub split.missing_sigma in @@ -911,8 +940,6 @@ let exe_spec vr_incons_res = inconsistent_results } in begin IList.iter log_check_exn checks; - if !Config.taint_analysis then - do_taint_check caller_pname callee_pname actual_pre missing_pi sub2 prop; let subbed_pre = (Prop.prop_sub sub1 actual_pre) in match check_dereferences callee_pname subbed_pre sub2 spec_pre formal_params with | Some (Deref_undef _, _) when !Config.angelic_execution -> diff --git a/infer/tests/ant_report.json b/infer/tests/ant_report.json index 77b0469a5..4f749f588 100644 --- a/infer/tests/ant_report.json +++ b/infer/tests/ant_report.json @@ -1,4 +1,9 @@ [ + { + "bug_type": "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION", + "file": "codetoanalyze/java/infer/TaintExample.java", + "procedure": "Socket TaintExample.callReadInputStreamCauseTaintError(SSLSocketFactory)" + }, { "bug_type": "CONTEXT_LEAK", "file": "codetoanalyze/java/infer/ContextLeaks.java", @@ -47,7 +52,12 @@ { "bug_type": "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION", "file": "codetoanalyze/java/infer/TaintExample.java", - "procedure": "InputStream TaintExample.taintingShouldNotPreventInference(SSLSocketFactory)" + "procedure": "InputStream TaintExample.taintingShouldNotPreventInference1(SSLSocketFactory)" + }, + { + "bug_type": "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION", + "file": "codetoanalyze/java/infer/TaintExample.java", + "procedure": "InputStream TaintExample.taintingShouldNotPreventInference2(SSLSocketFactory)" }, { "bug_type": "NULL_DEREFERENCE", @@ -659,4 +669,4 @@ "file": "codetoanalyze/java/infer/ResourceLeaks.java", "procedure": "void ResourceLeaks.zipFileLeakExceptionalBranch()" } -] +] \ No newline at end of file diff --git a/infer/tests/buck_report.json b/infer/tests/buck_report.json index 1f63ecf68..f43e8fc77 100644 --- a/infer/tests/buck_report.json +++ b/infer/tests/buck_report.json @@ -1,4 +1,9 @@ [ + { + "bug_type": "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION", + "file": "infer/tests/codetoanalyze/java/infer/TaintExample.java", + "procedure": "Socket TaintExample.callReadInputStreamCauseTaintError(SSLSocketFactory)" + }, { "bug_type": "CONTEXT_LEAK", "file": "infer/tests/codetoanalyze/java/infer/ContextLeaks.java", @@ -47,7 +52,12 @@ { "bug_type": "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION", "file": "infer/tests/codetoanalyze/java/infer/TaintExample.java", - "procedure": "InputStream TaintExample.taintingShouldNotPreventInference(SSLSocketFactory)" + "procedure": "InputStream TaintExample.taintingShouldNotPreventInference1(SSLSocketFactory)" + }, + { + "bug_type": "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION", + "file": "infer/tests/codetoanalyze/java/infer/TaintExample.java", + "procedure": "InputStream TaintExample.taintingShouldNotPreventInference2(SSLSocketFactory)" }, { "bug_type": "NULL_DEREFERENCE", @@ -659,4 +669,4 @@ "file": "infer/tests/codetoanalyze/java/infer/ResourceLeaks.java", "procedure": "void ResourceLeaks.zipFileLeakExceptionalBranch()" } -] +] \ No newline at end of file diff --git a/infer/tests/codetoanalyze/java/infer/TaintExample.java b/infer/tests/codetoanalyze/java/infer/TaintExample.java index 7eb8e6f7e..be2fcde54 100644 --- a/infer/tests/codetoanalyze/java/infer/TaintExample.java +++ b/infer/tests/codetoanalyze/java/infer/TaintExample.java @@ -29,15 +29,6 @@ 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) @@ -61,7 +52,6 @@ public class TaintExample { } } - HostnameVerifier mHostnameVerifier; public void throwExceptionIfNoVerify(SSLSocket sslSocket, String host) @@ -90,5 +80,30 @@ public class TaintExample { return s.getInputStream(); } + public InputStream taintingShouldNotPreventInference1(SSLSocketFactory f) throws IOException { + socketNotVerifiedSimple(f).toString(); + // failing to infer a post for socketNotVerifiedSimple will hide this error + Socket s = f.createSocket(); + return s.getInputStream(); + } + + public InputStream readInputStream(Socket socket) throws IOException { + return socket.getInputStream(); + } + + // if we're not careful, postcondition inference will fail for this function + Socket callReadInputStreamCauseTaintError(SSLSocketFactory f) + throws IOException { + Socket socket = f.createSocket(); + InputStream s = readInputStream(socket); + s.toString(); // to avoid RETURN_VALUE_IGNORED warning + return f.createSocket(); + } + + InputStream taintingShouldNotPreventInference2(SSLSocketFactory f) throws IOException { + // if inference fails for this callee, we won't report an error here + Socket s = callReadInputStreamCauseTaintError(f); + return s.getInputStream(); + } } diff --git a/infer/tests/endtoend/java/infer/TaintTest.java b/infer/tests/endtoend/java/infer/TaintTest.java index 77b409153..19f53ad12 100644 --- a/infer/tests/endtoend/java/infer/TaintTest.java +++ b/infer/tests/endtoend/java/infer/TaintTest.java @@ -27,6 +27,8 @@ public class TaintTest { public static final String TAINTED_VALUE = "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION"; + public static final String NULL_DEREFERENCE = "NULL_DEREFERENCE"; + private static InferResults inferResults; @BeforeClass @@ -41,7 +43,9 @@ public class TaintTest { "socketNotVerifiedSimple", "socketVerifiedForgotToCheckRetval", "socketIgnoreExceptionNoVerify", - "taintingShouldNotPreventInference" + "callReadInputStreamCauseTaintError", + "taintingShouldNotPreventInference1", + "taintingShouldNotPreventInference2", }; assertThat( @@ -53,8 +57,6 @@ public class TaintTest { methods ) ); - - } }