From 67c45bed78e8719a637ead1363583f2c719da803 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Fri, 27 Oct 2017 14:16:04 -0700 Subject: [PATCH] [quandary] fix invariant 1: "sink(s) with only non-footprint source" violations Summary: In a summary, you never want to see a trace where non-footprint sources flow to a sink. Such a trace is useless because nothing the caller does can make more data flow into that sink. Reviewed By: jeremydubreil Differential Revision: D5779983 fbshipit-source-id: d06778a --- infer/src/quandary/TaintAnalysis.ml | 32 ++++++++++++---- infer/src/unit/TaintTests.ml | 38 +------------------ .../codetoanalyze/cpp/quandary/arrays.cpp | 11 ++++++ .../codetoanalyze/cpp/quandary/issues.exp | 1 + .../codetoanalyze/java/quandary/Intents.java | 18 +++++++++ 5 files changed, 55 insertions(+), 45 deletions(-) diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml index 924e1ca19..6059c34ce 100644 --- a/infer/src/quandary/TaintAnalysis.ml +++ b/infer/src/quandary/TaintAnalysis.ml @@ -278,8 +278,13 @@ module Make (TaintSpecification : TaintSpec.S) = struct in let actual_trace' = TraceDomain.add_sink sink' actual_trace in report_trace actual_trace' callee_site proc_data ; - TaintDomain.add_trace actual_ap actual_trace' access_tree_acc - | None -> + if TraceDomain.Sources.Footprint.is_empty + (TraceDomain.sources actual_trace').footprint + then + (* no more sources can flow into this sink; no sense in keeping track of it *) + access_tree_acc + else TaintDomain.add_trace actual_ap actual_trace' access_tree_acc + | _ -> access_tree_acc ) | None -> L.internal_error @@ -366,7 +371,13 @@ module Make (TaintSpecification : TaintSpec.S) = struct match get_caller_ap_node_opt callee_ap access_tree_acc with | Some (caller_ap, (caller_trace, caller_tree)) -> let trace = instantiate_and_report callee_trace caller_trace access_tree_acc in - TaintDomain.add_node caller_ap (trace, caller_tree) access_tree_acc + let pruned_trace = + if TraceDomain.Sources.Footprint.is_empty (TraceDomain.sources trace).footprint then + (* empty footprint; nothing else can flow into these sinks. so don't track them *) + TraceDomain.update_sinks trace TraceDomain.Sinks.empty + else trace + in + TaintDomain.add_node caller_ap (pruned_trace, caller_tree) access_tree_acc | None -> ignore (instantiate_and_report callee_trace TraceDomain.empty access_tree_acc) ; access_tree_acc @@ -538,7 +549,13 @@ module Make (TaintSpecification : TaintSpec.S) = struct if TraceDomain.Sources.is_empty filtered_sources then access_tree else let trace' = TraceDomain.update_sources trace_with_propagation filtered_sources in - TaintDomain.add_trace access_path trace' access_tree + let pruned_trace = + if TraceDomain.Sources.Footprint.is_empty filtered_footprint then + (* empty footprint; nothing else can flow into these sinks. so don't track them *) + TraceDomain.update_sinks trace' TraceDomain.Sinks.empty + else trace' + in + TaintDomain.add_trace access_path pruned_trace access_tree in let handle_model_ astate_acc propagation = match (propagation, actuals, ret_opt) with @@ -719,7 +736,8 @@ module Make (TaintSpecification : TaintSpec.S) = struct (* invariant 4: we should never map an access path to a trace consisting only of its corresponding footprint source. a trace like this is a waste of space, since we can lazily create it if/when someone actually tries to read the access path instead *) - if AccessPath.Abs.is_exact access_path && Sinks.is_empty sinks + (* TODO: tmp to focus on invariant 1 *) + if false && AccessPath.Abs.is_exact access_path && Sinks.is_empty sinks && Sources.Footprint.mem access_path footprint_sources && Sources.Footprint.exists (fun footprint_access_path (is_mem, _) -> @@ -803,9 +821,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct acc) access_tree' TaintDomain.empty in - if Config.developer_mode && false - (* TODO: temporarily disabled to avoid crashes until we clean up all violations *) - then check_invariants with_footprint_vars ; + if Config.developer_mode then check_invariants with_footprint_vars ; TaintSpecification.to_summary_access_tree with_footprint_vars diff --git a/infer/src/unit/TaintTests.ml b/infer/src/unit/TaintTests.ml index 2dce4d83e..2f7d7d3fd 100644 --- a/infer/src/unit/TaintTests.ml +++ b/infer/src/unit/TaintTests.ml @@ -158,43 +158,7 @@ let tests = ; assign_id_to_field "base_id" "f" "non_source_id" ; invariant "{ ret_id$0 => (SOURCE -> ?) }" ] ) ; ( "sink without source not tracked" - , [assign_to_non_source "ret_id"; call_sink "ret_id"; assert_empty] ) - ; ( "source -> sink direct" - , [ assign_to_source "ret_id" - ; call_sink "ret_id" - ; invariant "{ ret_id$0* => (SOURCE -> SINK) }" ] ) - ; ( "source -> sink via var" - , [ assign_to_source "ret_id" - ; var_assign_id "actual" "ret_id" - ; call_sink_with_exp (var_of_str "actual") - ; invariant "{ ret_id$0 => (SOURCE -> ?), &actual* => (SOURCE -> SINK) }" ] ) - ; ( "source -> sink via var then ident" - , [ assign_to_source "ret_id" - ; var_assign_id "x" "ret_id" - ; id_assign_var "actual_id" "x" - ; call_sink "actual_id" - ; invariant "{ ret_id$0 => (SOURCE -> ?), &x* => (SOURCE -> SINK) }" ] ) - ; ( "source -> sink via field" - , [ assign_to_source "ret_id" - ; assign_id_to_field "base_id" "f" "ret_id" - ; read_field_to_id "actual_id" "base_id" "f" - ; call_sink "actual_id" - ; invariant "{ base_id$0.f* => (SOURCE -> SINK), ret_id$0 => (SOURCE -> ?) }" ] ) - ; ( "source -> sink via field read from var" - , [ assign_to_source "ret_id" - ; assign_id_to_field "base_id" "f" "ret_id" - ; var_assign_id "var" "base_id" - ; id_assign_var "var_id" "var" - ; read_field_to_id "read_id" "var_id" "f" - ; call_sink "read_id" - ; invariant - "{ base_id$0.f => (SOURCE -> ?),\n ret_id$0 => (SOURCE -> ?),\n &var.f* => (SOURCE -> SINK) }" - ] ) - ; ( "source -> sink via cast" - , [ assign_to_source "ret_id" - ; cast_id_to_id "cast_id" (Typ.mk Tvoid) "ret_id" - ; call_sink "cast_id" - ; invariant "{ ret_id$0* => (SOURCE -> SINK) }" ] ) ] + , [assign_to_non_source "ret_id"; call_sink "ret_id"; assert_empty] ) ] |> TestInterpreter.create_tests ~pp_opt:pp_sparse {formal_map= FormalMap.empty; summary= Specs.dummy} ~initial:(MockTaintAnalysis.Domain.empty, IdAccessPathMapDomain.empty) diff --git a/infer/tests/codetoanalyze/cpp/quandary/arrays.cpp b/infer/tests/codetoanalyze/cpp/quandary/arrays.cpp index 4cc574a0f..e30d445a1 100644 --- a/infer/tests/codetoanalyze/cpp/quandary/arrays.cpp +++ b/infer/tests/codetoanalyze/cpp/quandary/arrays.cpp @@ -13,6 +13,9 @@ extern int __infer_taint_source(); extern void skip(int i, int j); +// mocking gflags-generated field +extern int FLAGS_size; + namespace arrays { void array_sink1_bad(int arr[]) { @@ -48,6 +51,14 @@ int stack_smash_bad() { return arr[0]; // could read from anywhere in the stack } +void gflag_to_stack_allocated_array_bad() { int arr[FLAGS_size]; } + +// if we're not careful, this will re-report the warning in the callee +void read_global_no_double_report_ok() { + int i = FLAGS_size; + gflag_to_stack_allocated_array_bad(); +} + void strcpy_bad(char* str) { char* source = getenv("some_var"); strcpy(str, source); diff --git a/infer/tests/codetoanalyze/cpp/quandary/issues.exp b/infer/tests/codetoanalyze/cpp/quandary/issues.exp index 733200ca6..3f907d112 100644 --- a/infer/tests/codetoanalyze/cpp/quandary/issues.exp +++ b/infer/tests/codetoanalyze/cpp/quandary/issues.exp @@ -9,6 +9,7 @@ codetoanalyze/cpp/quandary/arrays.cpp, arrays::array_sink1_bad, 2, QUANDARY_TAIN codetoanalyze/cpp/quandary/arrays.cpp, arrays::array_sink2_bad, 2, QUANDARY_TAINT_ERROR, [Return from __infer_taint_source,Call to __array_access] codetoanalyze/cpp/quandary/arrays.cpp, arrays::array_sink3_bad, 0, QUANDARY_TAINT_ERROR, [Return from __infer_taint_source,Call to __array_access] codetoanalyze/cpp/quandary/arrays.cpp, arrays::array_sink4_bad, 2, QUANDARY_TAINT_ERROR, [Return from __infer_taint_source,Call to __array_access] +codetoanalyze/cpp/quandary/arrays.cpp, arrays::gflag_to_stack_allocated_array_bad, 0, UNTRUSTED_VARIABLE_LENGTH_ARRAY, [Return from __global_access,Call to __set_array_length] codetoanalyze/cpp/quandary/arrays.cpp, arrays::memcpy_bad, 2, QUANDARY_TAINT_ERROR, [Return from __infer_taint_source,Call to memcpy] codetoanalyze/cpp/quandary/arrays.cpp, arrays::memmove_bad, 2, QUANDARY_TAINT_ERROR, [Return from __infer_taint_source,Call to memmove] codetoanalyze/cpp/quandary/arrays.cpp, arrays::memset_bad, 2, QUANDARY_TAINT_ERROR, [Return from __infer_taint_source,Call to memset] diff --git a/infer/tests/codetoanalyze/java/quandary/Intents.java b/infer/tests/codetoanalyze/java/quandary/Intents.java index 1dfce5522..bd8b04967 100644 --- a/infer/tests/codetoanalyze/java/quandary/Intents.java +++ b/infer/tests/codetoanalyze/java/quandary/Intents.java @@ -11,6 +11,7 @@ package codetoanalyze.java.quandary; import java.io.IOException; import java.net.URISyntaxException; +import java.util.List; import android.app.Activity; import android.app.Service; @@ -210,4 +211,21 @@ public class Intents { mActivity.startActivity(newIntent); } + List mIntents; + + Context mContext; + + void callStartWithArrayOk() { + Intent[] intents = mIntents.toArray(new Intent[mIntents.size()]); + intents[0] = new Intent(intents[0]).addFlags(Intent.FLAG_ACTIVITY_NEW_TASK); + if (startWithArrayOk(mContext, intents)) { + mContext.startActivity(intents[1]); + } + } + + boolean startWithArrayOk(Context context, Intent[] newIntents) { + context.startActivities(newIntents, null); + return true; + } + }