[quandary] using summaries part 2: the relational cases

Differential Revision: D3861751

fbshipit-source-id: d7858e6

infer/src/quandary/TaintAnalysis.ml

@@ -166,36 +166,75 @@ module Make (TraceDomain : QuandarySummary.Trace) = struct
 
     let apply_summary
         ret_ids
-        (summary : QuandarySummary.t)
+        actuals
+        summary
         (astate_in : Domain.astate)
         proc_data
         callee_site =
+      let callee_loc = CallSite.loc callee_site in
+
       let apply_return ret_ap = function
         | [ret_id] -> AccessPath.with_base_var (Var.of_id ret_id) ret_ap
         | [] -> failwith "Have summary for retval, but no ret id to bind it to!"
         | _ -> failwith "Unimp: summaries for function with multiple return values" in
 
+      let get_actual_ap_trace formal_num formal_ap access_tree =
+        let get_actual_ap formal_num =
+          let f_resolve_id = resolve_id astate_in.id_map in
+          let actual_exp, actual_typ =
+            try IList.nth actuals formal_num
+            with Failure _ -> failwithf "Bad formal number %d" formal_num in
+          AccessPath.of_exp actual_exp actual_typ ~f_resolve_id in
+        let project ~formal_ap ~actual_ap =
+          let projected_ap = AccessPath.append actual_ap (snd (AccessPath.extract formal_ap)) in
+          if AccessPath.is_exact formal_ap
+          then AccessPath.Exact projected_ap
+          else AccessPath.Abstracted projected_ap in
+        match get_actual_ap formal_num with
+        | Some actual_ap ->
+            let projected_ap = project ~formal_ap ~actual_ap in
+            let projected_trace =
+              match access_path_get_node projected_ap access_tree proc_data callee_loc with
+              | Some (trace, _) -> trace
+              | None -> TraceDomain.initial in
+            Some (projected_ap, projected_trace)
+        | None ->
+            None in
+
       let apply_one access_tree (in_out_summary : QuandarySummary.in_out_summary) =
         let in_trace = match in_out_summary.input with
           | In_empty ->
               TraceDomain.initial
-          | In_formal _ | In_global _ ->
-              (* TODO: implement these cases *)
-              assert false in
-        let caller_ap =
+          | In_formal (formal_num, formal_ap) ->
+              begin
+                match get_actual_ap_trace formal_num formal_ap access_tree with
+                | Some (_, actual_trace) -> actual_trace
+                | None -> TraceDomain.initial
+              end
+          | In_global _ ->
+              (* TODO: implement this once we add globals to the footprint (t13273652) *)
+              TraceDomain.initial in
+
+        let caller_ap_trace_opt =
           match in_out_summary.output with
           | Out_return ret_ap ->
-              apply_return ret_ap ret_ids
-          | Out_formal _ | Out_global _ ->
-              (* TODO: implement these cases *)
-              assert false in
-        let output_trace = TraceDomain.of_summary_trace in_out_summary.output_trace in
-        let appended_trace = TraceDomain.append in_trace output_trace callee_site in
-        let joined_trace =
-          match access_path_get_node caller_ap access_tree proc_data (CallSite.loc callee_site) with
-          | Some (orig_trace, _) -> TraceDomain.join orig_trace appended_trace
-          | None -> appended_trace in
-        TaintDomain.add_trace caller_ap joined_trace access_tree in
+              Some (apply_return ret_ap ret_ids, TraceDomain.initial)
+          | Out_formal (formal_num, formal_ap) ->
+              get_actual_ap_trace formal_num formal_ap access_tree
+          | Out_global _ ->
+              (* TODO: implement this once we add globals to the footprint (t13273652) *)
+              None in
+        match caller_ap_trace_opt with
+        | Some (caller_ap, caller_trace) ->
+            let output_trace = TraceDomain.of_summary_trace in_out_summary.output_trace in
+            let appended_trace = TraceDomain.append in_trace output_trace callee_site in
+            let joined_trace = TraceDomain.join caller_trace appended_trace in
+            IList.iter
+              (Reporting.log_error (CallSite.pname callee_site) ~loc:callee_loc)
+              (TraceDomain.get_reportable_exns joined_trace);
+            TaintDomain.add_trace caller_ap joined_trace access_tree
+        | None ->
+            access_tree in
 
       let access_tree = IList.fold_left apply_one astate_in.access_tree summary in
       { astate_in with access_tree; }
@@ -283,7 +322,7 @@ module Make (TraceDomain : QuandarySummary.Trace) = struct
           let astate_with_summary =
             match Summary.read_summary proc_data.tenv proc_data.pdesc callee_pname with
             | Some summary ->
-                apply_summary ret_ids summary astate_with_source proc_data call_site
+                apply_summary ret_ids actuals summary astate_with_source proc_data call_site
             | None ->
                 astate_with_source in
 

infer/src/quandary/Trace.ml

@@ -153,9 +153,13 @@ module Make (Spec : Spec) = struct
         |> Sources.union caller_trace.sources in
       let sinks = Sinks.union caller_trace.sinks callee_trace.sinks in
       let passthroughs =
+        (* true if the procedure of [sink] is itself a sink rather than a caller of a sink *)
+        let is_original_sink sink =
+          Procname.equal (CallSite.pname callee_site) (CallSite.pname (Sink.call_site sink)) in
         let joined_passthroughs =
           Passthroughs.union caller_trace.passthroughs callee_trace.passthroughs in
-        if Sinks.is_empty callee_trace.sinks
+        if Sinks.is_empty callee_trace.sinks ||
+           not (Sinks.for_all is_original_sink callee_trace.sinks)
         then Passthroughs.add (Passthrough.make callee_site) joined_passthroughs
         else joined_passthroughs in
       { sources; sinks; passthroughs; }

infer/src/unit/TraceTests.ml

@@ -20,7 +20,7 @@ module MockTraceElem = struct
 
   type t = kind
 
-  let call_site _ = assert false
+  let call_site _ = CallSite.dummy
 
   let kind t = t
 

infer/tests/codetoanalyze/java/quandary/Interprocedural.java

@@ -19,6 +19,10 @@ class Interprocedural {
     Object f;
   }
 
+  public static Object id(Object param) {
+    return param;
+  }
+
   /** source tests */
 
   public static Object returnSourceDirect() {
@@ -52,6 +56,66 @@ class Interprocedural {
     InferTaint.inferSensitiveSink(returnSourceViaField().f);
   }
 
+  /** sink tests */
+
+  public static void callSinkParam1(Object param1, Object param2) {
+    InferTaint.inferSensitiveSink(param1);
+  }
+
+  public static void callSinkParam1Bad() {
+    callSinkParam1(InferTaint.inferSecretSource(), null);
+  }
+
+  public static void callSinkParam1Ok() {
+    callSinkParam1(null, InferTaint.inferSecretSource());
+  }
+
+  public static void callSinkParam2(Object param1, Object param2) {
+    InferTaint.inferSensitiveSink(param2);
+  }
+
+  public static void callSinkParam2Bad() {
+    callSinkParam2(null, InferTaint.inferSecretSource());
+  }
+
+  public static void callSinkParam2Ok() {
+    callSinkParam2(InferTaint.inferSecretSource(), null);
+  }
+
+  public void callSinkOnFieldDirect() {
+    InferTaint.inferSensitiveSink(this.f);
+  }
+
+  public void callSinkOnFieldDirectBad() {
+    this.f = InferTaint.inferSecretSource();
+    callSinkOnFieldDirect();
+  }
+
+  public static void callSinkOnFieldIndirect(Obj param) {
+    InferTaint.inferSensitiveSink(param.f);
+  }
+
+  public static void callSinkOnFieldIndirectBad() {
+    Obj obj = new Obj();
+    obj.f = InferTaint.inferSecretSource();
+    callSinkOnFieldIndirect(obj);
+  }
+
+  /** passthrough tests */
+
+  public static void singlePassthroughBad() {
+    Object source = InferTaint.inferSecretSource();
+    Object launderedSource = id(source);
+    InferTaint.inferSensitiveSink(launderedSource);
+  }
+
+  public static void doublePassthroughBad() {
+    Object source = InferTaint.inferSecretSource();
+    Object launderedSource1 = id(source);
+    Object launderedSource2 = id(launderedSource1);
+    InferTaint.inferSensitiveSink(launderedSource2);
+  }
+
   /** false positives: an ideal analysis would not report these, but we will */
 
   public static Object returnSourceConditional(boolean b) {
@@ -63,4 +127,27 @@ class Interprocedural {
     InferTaint.inferSensitiveSink(returnSourceConditional(false));
   }
 
+   public static void reassignInCallee(Obj o) {
+     o.f = null;
+  }
+
+  public static void FP_reassignInCallee() {
+    Obj o = new Obj();
+    o.f = InferTaint.inferSecretSource();
+    reassignInCallee(o);
+    InferTaint.inferSensitiveSink(o.f);
+  }
+
+  /** false negatives: an ideal analysis would report on these, but we do not */
+
+  // this gets modeled as Object[] params in Java. need to treat the array is tainted if its
+  // contents are tainted in order to get this (t13493230).
+  public static void callSinkVariadic(Object... params) {
+    InferTaint.inferSensitiveSink(params);
+  }
+
+  public static void FN_callSinkVariadicBad() {
+    callSinkVariadic(null, null, InferTaint.inferSecretSource());
+  }
+
 }

infer/tests/codetoanalyze/java/quandary/issues.exp

@@ -29,11 +29,18 @@ Fields.java:44: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.infer
 Fields.java:51: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 49]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 51]) via {  }
 Fields.java:56: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 55]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 56]) via {  }
 Fields.java:63: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 62]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 63]) via {  }
-Interprocedural.java:33: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 25]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 33]) via { Object Interprocedural.returnSourceDirect() at [line 33] }
-Interprocedural.java:38: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 25]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 38]) via { Object Interprocedural.returnSourceDirect() at [line 37] }
-Interprocedural.java:42: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 29]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 42]) via { Object Interprocedural.returnSourceIndirect() at [line 42] }
-Interprocedural.java:52: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 47]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 52]) via { Interprocedural$Obj Interprocedural.returnSourceViaField() at [line 52] }
-Interprocedural.java:63: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 58]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 63]) via { Object Interprocedural.returnSourceConditional(boolean) at [line 63] }
+Interprocedural.java:37: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 29]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 37]) via { Object Interprocedural.returnSourceDirect() at [line 37] }
+Interprocedural.java:42: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 29]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 42]) via { Object Interprocedural.returnSourceDirect() at [line 41] }
+Interprocedural.java:46: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 33]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 46]) via { Object Interprocedural.returnSourceIndirect() at [line 46] }
+Interprocedural.java:56: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 51]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 56]) via { Interprocedural$Obj Interprocedural.returnSourceViaField() at [line 56] }
+Interprocedural.java:66: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 66]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 62]) via { void Interprocedural.callSinkParam1(Object,Object) at [line 66] }
+Interprocedural.java:78: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 78]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 74]) via { void Interprocedural.callSinkParam2(Object,Object) at [line 78] }
+Interprocedural.java:91: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 90]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 86]) via { void Interprocedural.callSinkOnFieldDirect() at [line 91] }
+Interprocedural.java:101: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 100]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 95]) via { void Interprocedural.callSinkOnFieldIndirect(Interprocedural$Obj) at [line 101] }
+Interprocedural.java:109: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 107]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 109]) via { Object Interprocedural.id(Object) at [line 108] }
+Interprocedural.java:116: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 113]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 116]) via { Object Interprocedural.id(Object) at [line 114], Object Interprocedural.id(Object) at [line 115] }
+Interprocedural.java:127: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 122]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 127]) via { Object Interprocedural.returnSourceConditional(boolean) at [line 127] }
+Interprocedural.java:138: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 136]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 138]) via {  }
 LoggingPrivateData.java:18: ERROR: QUANDARY_TAINT_ERROR Error: SharedPreferences(String SharedPreferences.getString(String,String) at [line 18]) -> Logging(int Log.d(String,String) at [line 18]) via {  }
 LoggingPrivateData.java:22: ERROR: QUANDARY_TAINT_ERROR Error: SharedPreferences(String SharedPreferences.getString(String,String) at [line 22]) -> Logging(int Log.d(String,String) at [line 22]) via {  }
 LoggingPrivateData.java:37: ERROR: QUANDARY_TAINT_ERROR Error: SharedPreferences(String SharedPreferences.getString(String,String) at [line 36]) -> Logging(int Log.w(String,Throwable) at [line 37]) via {  }