From 00f948e924c6022227e6a6269e9454ed69a3d701 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Tue, 11 Apr 2017 05:24:10 -0700 Subject: [PATCH] [quandary] don't add callee-local state to the caller Summary: If we couldn't project the callee access path into the caller during summary application, we still added the corresponding trace to the caller state. This was wasteful; it just bloats the caller with state it will never look at. Fixed it by making `get_caller_ap_node` return `None` when the state won't be visible in the caller. Reviewed By: jeremydubreil Differential Revision: D4727937 fbshipit-source-id: 87665e9 --- infer/src/quandary/JavaTaintAnalysis.ml | 3 +- infer/src/quandary/TaintAnalysis.ml | 131 +++++++++++++----- .../codetoanalyze/java/quandary/Strings.java | 2 +- .../codetoanalyze/java/quandary/issues.exp | 9 +- 4 files changed, 104 insertions(+), 41 deletions(-) diff --git a/infer/src/quandary/JavaTaintAnalysis.ml b/infer/src/quandary/JavaTaintAnalysis.ml index 534fcc305..739855162 100644 --- a/infer/src/quandary/JavaTaintAnalysis.ml +++ b/infer/src/quandary/JavaTaintAnalysis.ml @@ -69,7 +69,8 @@ include | pname -> failwithf "Non-Java procname %a in Java analysis@." Typ.Procname.pp pname - let is_taintable_type = function + let is_taintable_type typ= + match typ with | Typ.Tptr (Tstruct (JavaClass typename), _) | Tstruct (JavaClass typename) -> begin match Mangled.to_string_full typename with diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml index 7d6553465..547dfbc9f 100644 --- a/infer/src/quandary/TaintAnalysis.ml +++ b/infer/src/quandary/TaintAnalysis.ml @@ -73,6 +73,14 @@ module Make (TaintSpecification : TaintSpec.S) = struct | Var.ProgramVar pvar -> Pvar.is_global pvar | Var.LogicalVar _ -> false + let is_return (var, _) = match var with + | Var.ProgramVar pvar -> Pvar.is_return pvar + | Var.LogicalVar _ -> false + + let is_footprint (var, _) = match var with + | Var.ProgramVar _ -> false + | Var.LogicalVar id -> Ident.is_footprint id + let make_footprint_var formal_index = Var.of_id (Ident.create_footprint Ident.name_spec formal_index) @@ -264,34 +272,41 @@ module Make (TaintSpecification : TaintSpec.S) = struct | _ -> None in - let get_caller_ap_node ap access_tree = - match get_caller_ap ap with - | Some caller_ap -> - let caller_node_opt = access_path_get_node caller_ap access_tree proc_data in - let caller_node = match caller_node_opt with - | Some caller_node -> caller_node | None -> TaintDomain.empty_node in - caller_ap, caller_node - | None -> - ap, TaintDomain.empty_node in + let get_caller_ap_node_opt ap access_tree = + let get_caller_node caller_ap = + let caller_node_opt = access_path_get_node caller_ap access_tree proc_data in + let caller_node = Option.value ~default:TaintDomain.empty_node caller_node_opt in + caller_ap, caller_node in + Option.map (get_caller_ap ap) ~f:get_caller_node in let replace_footprint_sources callee_trace caller_trace access_tree = let replace_footprint_source source acc = match TraceDomain.Source.get_footprint_access_path source with | Some footprint_access_path -> - let _, (caller_ap_trace, _) = get_caller_ap_node footprint_access_path access_tree in - TraceDomain.join caller_ap_trace acc + begin + match get_caller_ap_node_opt footprint_access_path access_tree with + | Some (_, (caller_ap_trace, _)) -> TraceDomain.join caller_ap_trace acc + | None -> acc + end | None -> acc in TraceDomain.Sources.fold replace_footprint_source (TraceDomain.sources callee_trace) caller_trace in - let add_to_caller_tree access_tree_acc callee_ap callee_trace = - let caller_ap, (caller_trace, caller_tree) = get_caller_ap_node callee_ap access_tree_acc in - let caller_trace' = replace_footprint_sources callee_trace caller_trace access_tree_acc in - let appended_trace = - TraceDomain.append caller_trace' callee_trace callee_site in + let instantiate_and_report callee_trace caller_trace access_tree = + let caller_trace' = replace_footprint_sources callee_trace caller_trace access_tree in + let appended_trace = TraceDomain.append caller_trace' callee_trace callee_site in report_trace appended_trace callee_site proc_data; - TaintDomain.add_node caller_ap (appended_trace, caller_tree) access_tree_acc in + appended_trace in + + let add_to_caller_tree access_tree_acc callee_ap callee_trace = + 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 + | None -> + ignore (instantiate_and_report callee_trace TraceDomain.empty access_tree_acc); + access_tree_acc in let access_tree = TaintDomain.trace_fold @@ -365,7 +380,6 @@ module Make (TaintSpecification : TaintSpec.S) = struct astate | Sil.Call (ret, Const (Cfun called_pname), actuals, callee_loc, call_flags) -> - let handle_unknown_call callee_pname astate = let is_variadic = match callee_pname with | Typ.Procname.Java pname -> @@ -391,7 +405,8 @@ module Make (TaintSpecification : TaintSpec.S) = struct Option.exists (AccessPath.Raw.get_typ (AccessPath.extract access_path) proc_data.tenv) ~f:should_taint_typ - | None -> true) + | None -> + true) (TraceDomain.sources trace_with_propagation) in if TraceDomain.Sources.is_empty filtered_sources then @@ -500,29 +515,75 @@ module Make (TaintSpecification : TaintSpec.S) = struct module Analyzer = AbstractInterpreter.Make (ProcCfg.Exceptional) (TransferFunctions) let make_summary formal_map access_tree = + (* if a trace has footprint sources, attach them to the appropriate footprint var *) let access_tree' = + TaintDomain.fold + (fun access_tree_acc _ ((trace, _) as node) -> + if TraceDomain.Sinks.is_empty (TraceDomain.sinks trace) + then + (* if this trace has no sinks, we don't need to attach it to anything *) + access_tree_acc + else + TraceDomain.Sources.fold + (fun source acc -> + match TraceDomain.Source.get_footprint_access_path source with + | Some footprint_access_path -> + let node' = + match TaintDomain.get_node footprint_access_path acc with + | Some n -> TaintDomain.node_join node n + | None -> node in + TaintDomain.add_node footprint_access_path node' acc + | None -> + acc) + (TraceDomain.sources trace) + access_tree_acc) + access_tree + access_tree in + + (* should only be used on nodes associated with a footprint base *) + let is_empty_node (trace, tree) = + TraceDomain.Sinks.is_empty (TraceDomain.sinks trace) && + match tree with + | TaintDomain.Subtree subtree -> TaintDomain.AccessMap.is_empty subtree + | TaintDomain.Star -> true in + + (* replace formal names with footprint vars for their indices. For example, for `foo(o)`, we'll + replace `o` with FP(1) *) + let with_footprint_vars = AccessPath.BaseMap.fold - (fun base node acc -> - match FormalMap.get_formal_index base formal_map with - | Some formal_index -> - let base' = make_footprint_var formal_index, snd base in - let joined_node = - try TaintDomain.node_join (AccessPath.BaseMap.find base' acc) node - with Not_found -> node in + (fun base ((trace, subtree) as node) acc -> + if is_global base || is_return base + then AccessPath.BaseMap.add base node acc + else if is_footprint base + then + if is_empty_node node + then + acc + else let node' = - if TraceDomain.Sinks.is_empty (TraceDomain.sinks (fst joined_node)) + if TraceDomain.Sinks.is_empty (TraceDomain.sinks trace) + then TraceDomain.empty, subtree + else node in + AccessPath.BaseMap.add base node' acc + else + match FormalMap.get_formal_index base formal_map with + | Some formal_index -> + let base' = make_footprint_var formal_index, snd base in + let joined_node = + try TaintDomain.node_join (AccessPath.BaseMap.find base' acc) node + with Not_found -> node in + if is_empty_node joined_node then - (* Java is call-by-value; we can't update a formal in the callee. so drop the - trace associated with the formal unless it contains sinks *) - TraceDomain.empty, snd joined_node + acc else - joined_node in - AccessPath.BaseMap.add base' node' acc - | None -> AccessPath.BaseMap.add base node acc) - access_tree + AccessPath.BaseMap.add base' joined_node acc + | None -> + (* base is a local var *) + acc) + access_tree' TaintDomain.empty in - TaintSpecification.to_summary_access_tree access_tree' + TaintSpecification.to_summary_access_tree with_footprint_vars module Interprocedural = AbstractInterpreter.Interprocedural(Summary) diff --git a/infer/tests/codetoanalyze/java/quandary/Strings.java b/infer/tests/codetoanalyze/java/quandary/Strings.java index 6b4ddca67..902630ce8 100644 --- a/infer/tests/codetoanalyze/java/quandary/Strings.java +++ b/infer/tests/codetoanalyze/java/quandary/Strings.java @@ -74,7 +74,7 @@ public class Strings { InferTaint.inferSensitiveSink(tainted); } - void FN_viaStringFormatVarArgsIndirectBad() { + void viaStringFormatVarArgsIndirectBad() { viaStringFormatVarArgsIndirect(InferTaint.inferSecretSource()); } diff --git a/infer/tests/codetoanalyze/java/quandary/issues.exp b/infer/tests/codetoanalyze/java/quandary/issues.exp index 497520a95..12fb9161e 100644 --- a/infer/tests/codetoanalyze/java/quandary/issues.exp +++ b/infer/tests/codetoanalyze/java/quandary/issues.exp @@ -112,10 +112,10 @@ codetoanalyze/java/quandary/Interprocedural.java, void Interprocedural.callSinkP codetoanalyze/java/quandary/Interprocedural.java, void Interprocedural.callSinkParam2Bad(), 1, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),call to void Interprocedural.callSinkParam2(Object,Object),call to void InferTaint.inferSensitiveSink(Object)] codetoanalyze/java/quandary/Interprocedural.java, void Interprocedural.callSinkVariadicBad(), 1, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),call to void Interprocedural.callSinkVariadic(java.lang.Object[]),call to void InferTaint.inferSensitiveSink(Object)] codetoanalyze/java/quandary/Interprocedural.java, void Interprocedural.doublePassthroughBad(), 4, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),flow through Object Interprocedural.id(Object),flow through Object Interprocedural.id(Object),call to void InferTaint.inferSensitiveSink(Object)] -codetoanalyze/java/quandary/Interprocedural.java, void Interprocedural.getGlobalThenCallSinkBad(), 2, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),call to void Interprocedural.getGlobalThenCallSink(),flow through Object Interprocedural.getGlobal(),call to void InferTaint.inferSensitiveSink(Object)] -codetoanalyze/java/quandary/Interprocedural.java, void Interprocedural.returnSourceDirectBad(), 1, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),return from Object Interprocedural.returnSourceDirect(),flow through Object Interprocedural.returnSourceDirect(),call to void InferTaint.inferSensitiveSink(Object)] -codetoanalyze/java/quandary/Interprocedural.java, void Interprocedural.returnSourceDirectViaVarBad(), 2, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),return from Object Interprocedural.returnSourceDirect(),flow through Object Interprocedural.returnSourceDirect(),call to void InferTaint.inferSensitiveSink(Object)] -codetoanalyze/java/quandary/Interprocedural.java, void Interprocedural.returnSourceIndirectBad(), 1, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),return from Object Interprocedural.returnSourceDirect(),flow through Object Interprocedural.returnSourceDirect(),return from Object Interprocedural.returnSourceIndirect(),flow through Object Interprocedural.returnSourceIndirect(),call to void InferTaint.inferSensitiveSink(Object)] +codetoanalyze/java/quandary/Interprocedural.java, void Interprocedural.getGlobalThenCallSinkBad(), 2, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),call to void Interprocedural.getGlobalThenCallSink(),call to void InferTaint.inferSensitiveSink(Object)] +codetoanalyze/java/quandary/Interprocedural.java, void Interprocedural.returnSourceDirectBad(), 1, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),return from Object Interprocedural.returnSourceDirect(),call to void InferTaint.inferSensitiveSink(Object)] +codetoanalyze/java/quandary/Interprocedural.java, void Interprocedural.returnSourceDirectViaVarBad(), 2, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),return from Object Interprocedural.returnSourceDirect(),call to void InferTaint.inferSensitiveSink(Object)] +codetoanalyze/java/quandary/Interprocedural.java, void Interprocedural.returnSourceIndirectBad(), 1, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),return from Object Interprocedural.returnSourceDirect(),return from Object Interprocedural.returnSourceIndirect(),call to void InferTaint.inferSensitiveSink(Object)] codetoanalyze/java/quandary/Interprocedural.java, void Interprocedural.returnSourceViaFieldBad(), 1, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),return from Interprocedural$Obj Interprocedural.returnSourceViaField(),call to void InferTaint.inferSensitiveSink(Object)] codetoanalyze/java/quandary/Interprocedural.java, void Interprocedural.returnSourceViaGlobalBad(), 2, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),return from void Interprocedural.returnSourceViaGlobal(),call to void InferTaint.inferSensitiveSink(Object)] codetoanalyze/java/quandary/Interprocedural.java, void Interprocedural.returnSourceViaParameter1Bad(Interprocedural$Obj), 2, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),return from void Interprocedural.returnSourceViaParameter1(Interprocedural$Obj),call to void InferTaint.inferSensitiveSink(Object)] @@ -172,6 +172,7 @@ codetoanalyze/java/quandary/Strings.java, void Strings.viaStringBuilderBad(), 3, codetoanalyze/java/quandary/Strings.java, void Strings.viaStringBuilderIgnoreReturnBad(), 5, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),call to void InferTaint.inferSensitiveSink(Object)] codetoanalyze/java/quandary/Strings.java, void Strings.viaStringBuilderSugarBad(), 2, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),call to void InferTaint.inferSensitiveSink(Object)] codetoanalyze/java/quandary/Strings.java, void Strings.viaStringFormatVarArgsDirectBad(), 3, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),call to void InferTaint.inferSensitiveSink(Object)] +codetoanalyze/java/quandary/Strings.java, void Strings.viaStringFormatVarArgsIndirectBad(), 1, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),call to void Strings.viaStringFormatVarArgsIndirect(Object),call to void InferTaint.inferSensitiveSink(Object)] codetoanalyze/java/quandary/TaintedFormals.java, void TaintedFormals.callTaintedContextBad1(String), 2, QUANDARY_TAINT_ERROR, [return from Object TaintedFormals.taintedContextBad(String),return from Object TaintedFormals.taintedContextBad(String),call to void InferTaint.inferSensitiveSink(Object)] codetoanalyze/java/quandary/TaintedFormals.java, void TaintedFormals.callTaintedContextBad2(), 1, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),call to void TaintedFormals.taintedContextBad(String,Intent,Integer),call to ComponentName ContextWrapper.startService(Intent)] codetoanalyze/java/quandary/TaintedFormals.java, void TaintedFormals.taintedContextBad(String,Intent,Integer), 3, QUANDARY_TAINT_ERROR, [return from void TaintedFormals.taintedContextBad(String,Intent,Integer),call to void InferTaint.inferSensitiveSink(Object)]