[quandary] allow trace-specific rules for handling unknown code

Reviewed By: jeremydubreil

Differential Revision: D3962285

fbshipit-source-id: b14f3d2

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;

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)

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 =

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

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)

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

infer/tests/codetoanalyze/java/quandary/Makefile

@@ -19,6 +19,7 @@ FILES = \
   Interprocedural.java \
   LoggingPrivateData.java \
   Recursion.java \
+  Strings.java \
 
 compile:
 	javac -cp $(CLASSPATH) $(FILES)

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);
+  }
+
+}

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] }