From 5e2e7b88aad249989ee06ed514732d442cc491b9 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Tue, 4 Oct 2016 15:14:53 -0700 Subject: [PATCH] [quandary] allow trace-specific rules for handling unknown code Reviewed By: jeremydubreil Differential Revision: D3962285 fbshipit-source-id: b14f3d2 --- infer/src/checkers/registerCheckers.ml | 2 +- infer/src/quandary/JavaTaintAnalysis.ml | 58 +++++++++++++++++++ infer/src/quandary/QuandarySummary.ml | 2 + infer/src/quandary/QuandarySummary.mli | 2 + infer/src/quandary/TaintAnalysis.ml | 20 ++----- infer/src/unit/TaintTests.ml | 1 + .../codetoanalyze/java/quandary/Makefile | 1 + .../codetoanalyze/java/quandary/Strings.java | 35 +++++++++++ .../codetoanalyze/java/quandary/issues.exp | 2 + 9 files changed, 107 insertions(+), 16 deletions(-) create mode 100644 infer/src/quandary/JavaTaintAnalysis.ml create mode 100644 infer/tests/codetoanalyze/java/quandary/Strings.java diff --git a/infer/src/checkers/registerCheckers.ml b/infer/src/checkers/registerCheckers.ml index 8984bd201..50614bbb3 100644 --- a/infer/src/checkers/registerCheckers.ml +++ b/infer/src/checkers/registerCheckers.ml @@ -33,7 +33,7 @@ let active_procedure_checkers () = SqlChecker.callback_sql, false; Eradicate.callback_eradicate, Config.eradicate; BoundedCallTree.checker, Config.crashcontext; - TaintAnalysis.Java.checker, Config.quandary; + JavaTaintAnalysis.checker, Config.quandary; Checkers.callback_check_field_access, false; ImmutableChecker.callback_check_immutable_cast, checkers_enabled; RepeatedCallsChecker.callback_check_repeated_calls, checkers_enabled; diff --git a/infer/src/quandary/JavaTaintAnalysis.ml b/infer/src/quandary/JavaTaintAnalysis.ml new file mode 100644 index 000000000..f3930601d --- /dev/null +++ b/infer/src/quandary/JavaTaintAnalysis.ml @@ -0,0 +1,58 @@ +(* + * Copyright (c) 2016 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + *) + +open! Utils + +module F = Format +module L = Logging + +include + TaintAnalysis.Make(struct + include JavaTrace + + let to_summary_trace trace = QuandarySummary.Java trace + + let of_summary_trace = function + | QuandarySummary.Java trace -> trace + | QuandarySummary.Unknown -> assert false + + (* propagate the trace from the nth parameter of [site.pname] to the return value of + [site.pname]. if [propagate_reachable] is true, all traces reachable from the parameter will + be propagated as well (e.g., for foo(x), we'll also propagate the traces associated with x.f, + x.f.g, and so on) *) + let propagate_nth_to_return n site ret_typ ~propagate_all = + let pname = CallSite.pname site in + let dummy_param_ap = + let raw_ap = + (* base of this access path is always ignored, so type/name don't matter *) + AccessPath.of_pvar (Pvar.mk (Mangled.from_string "fake_param") pname) Typ.Tvoid in + if propagate_all then AccessPath.Abstracted raw_ap else AccessPath.Exact raw_ap in + let input = QuandarySummary.make_formal_input n dummy_param_ap in + let output = + QuandarySummary.make_return_output + (AccessPath.Exact (AccessPath.of_pvar (Pvar.get_ret_pvar pname) ret_typ)) in + let footprint_source = Source.make_footprint dummy_param_ap site in + let footprint_trace = of_source footprint_source in + QuandarySummary.make_in_out_summary input output (to_summary_trace footprint_trace) + + let handle_unknown site ret_typ_opt = + match CallSite.pname site with + | Procname.Java pname -> + begin + match Procname.java_get_class_name pname, + Procname.java_get_method pname, + ret_typ_opt with + | "java.lang.String", "valueOf", Some ret_typ -> + [propagate_nth_to_return 0 site ret_typ ~propagate_all:true] + | _ -> + [] + end + | pname -> + failwithf "Non-Java procname %a in Java analysis@." Procname.pp pname + end) diff --git a/infer/src/quandary/QuandarySummary.ml b/infer/src/quandary/QuandarySummary.ml index e481bebbd..c394051a7 100644 --- a/infer/src/quandary/QuandarySummary.ml +++ b/infer/src/quandary/QuandarySummary.ml @@ -55,6 +55,8 @@ module type Trace = sig val to_summary_trace : t -> summary_trace val of_summary_trace : summary_trace -> t + + val handle_unknown : CallSite.t -> Typ.t option -> in_out_summary list end let make_formal_input index access_path = diff --git a/infer/src/quandary/QuandarySummary.mli b/infer/src/quandary/QuandarySummary.mli index 38c9af9eb..1d4b8656c 100644 --- a/infer/src/quandary/QuandarySummary.mli +++ b/infer/src/quandary/QuandarySummary.mli @@ -56,6 +56,8 @@ module type Trace = sig val to_summary_trace : t -> summary_trace val of_summary_trace : summary_trace -> t + + val handle_unknown : CallSite.t -> Typ.t option -> in_out_summary list end val make_formal_input : int -> AccessPath.t -> input diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml index 506e455ee..d296334f6 100644 --- a/infer/src/quandary/TaintAnalysis.ml +++ b/infer/src/quandary/TaintAnalysis.ml @@ -326,11 +326,11 @@ module Make (TraceDomain : QuandarySummary.Trace) = struct failwith "Unimp: handling multiple return ids" in let astate_with_summary = - match Summary.read_summary proc_data.tenv proc_data.pdesc callee_pname with - | Some summary -> - apply_summary ret_id actuals summary astate_with_source proc_data call_site - | None -> - astate_with_source in + let summary = + match Summary.read_summary proc_data.tenv proc_data.pdesc callee_pname with + | Some summary -> summary + | None -> TraceDomain.handle_unknown call_site (Option.map snd ret_id) in + apply_summary ret_id actuals summary astate_with_source proc_data call_site in astate_with_summary | Sil.Call _ -> @@ -457,13 +457,3 @@ module Make (TraceDomain : QuandarySummary.Trace) = struct end end - -module Java = Make(struct - include JavaTrace - - let to_summary_trace trace = QuandarySummary.Java trace - - let of_summary_trace = function - | QuandarySummary.Java trace -> trace - | QuandarySummary.Unknown -> assert false - end) diff --git a/infer/src/unit/TaintTests.ml b/infer/src/unit/TaintTests.ml index 70485114e..1e926068a 100644 --- a/infer/src/unit/TaintTests.ml +++ b/infer/src/unit/TaintTests.ml @@ -65,6 +65,7 @@ module MockTaintAnalysis = TaintAnalysis.Make(struct let of_summary_trace _ = assert false let to_summary_trace _ = assert false + let handle_unknown _ _ = [] end) module TestInterpreter = AnalyzerTester.Make diff --git a/infer/tests/codetoanalyze/java/quandary/Makefile b/infer/tests/codetoanalyze/java/quandary/Makefile index 15247883b..3b8e654b5 100644 --- a/infer/tests/codetoanalyze/java/quandary/Makefile +++ b/infer/tests/codetoanalyze/java/quandary/Makefile @@ -19,6 +19,7 @@ FILES = \ Interprocedural.java \ LoggingPrivateData.java \ Recursion.java \ + Strings.java \ compile: javac -cp $(CLASSPATH) $(FILES) diff --git a/infer/tests/codetoanalyze/java/quandary/Strings.java b/infer/tests/codetoanalyze/java/quandary/Strings.java new file mode 100644 index 000000000..1e7b192b5 --- /dev/null +++ b/infer/tests/codetoanalyze/java/quandary/Strings.java @@ -0,0 +1,35 @@ +/* + * Copyright (c) 2016 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ + +package codetoanalyze.java.quandary; + +import com.facebook.infer.builtins.InferTaint; + +/** testing how the analysis handles strings and string manipulation functions */ + +public class Strings { + + static class Wrapper { + Object f; + } + + static void valueOfStringBad() { + Object source = InferTaint.inferSecretSource(); + String stringSource = String.valueOf(source); + InferTaint.inferSensitiveSink(stringSource); + } + + static void valueOfStringWrapperBad() { + Wrapper w = new Wrapper(); + w.f = InferTaint.inferSecretSource(); + String stringSource = String.valueOf(w.f); + InferTaint.inferSensitiveSink(stringSource); + } + +} diff --git a/infer/tests/codetoanalyze/java/quandary/issues.exp b/infer/tests/codetoanalyze/java/quandary/issues.exp index 27ed1f304..50f8c1a42 100644 --- a/infer/tests/codetoanalyze/java/quandary/issues.exp +++ b/infer/tests/codetoanalyze/java/quandary/issues.exp @@ -90,3 +90,5 @@ LoggingPrivateData.java:37: ERROR: QUANDARY_TAINT_ERROR Error: SharedPreferences Recursion.java:26: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 26]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 21]) via { void Recursion.callSinkThenDiverge(Object) at [line 26] } Recursion.java:36: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 36]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 31]) via { void Recursion.safeRecursionCallSink(int,Object) at [line 36] } Recursion.java:42: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 42]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 41]) via { void Recursion.recursionBad(int,Object) at [line 42] } +Strings.java:25: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 23]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 25]) via { String String.valueOf(Object) at [line 24] } +Strings.java:32: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 30]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 32]) via { String String.valueOf(Object) at [line 31] }