[quandary] support tainted formals

Summary:
We currently can only model the return values of functions as sources.
In order to model inputs of endpoints as sources, we need the capability to treat the formals of certain functions as sources too.
This diff adds that capability by adding a function for getting the tainted sources to the source module, then using that info in the analysis.

Reviewed By: jeremydubreil

Differential Revision: D4314738

fbshipit-source-id: dd7d423

infer/src/checkers/Source.ml

@@ -18,8 +18,9 @@ module type S = sig
 
   val get_footprint_access_path: t -> AccessPath.t option
 
-  (** return Some (kind) if the call site is a taint source, None otherwise *)
   val get : CallSite.t -> t option
+
+  val get_tainted_formals : Procdesc.t -> (Mangled.t * Typ.t * t option) list
 end
 
 module Dummy = struct
@@ -37,8 +38,12 @@ module Dummy = struct
 
   let make_footprint _ _ = assert false
   let get_footprint_access_path _ = assert false
+
   let get _ = None
 
+  let get_tainted_formals pdesc =
+    IList.map (fun (name, typ) -> name, typ, None) (Procdesc.get_formals pdesc)
+
   module Kind = struct
     type nonrec t = t
     let compare = compare

infer/src/checkers/Source.mli

@@ -18,8 +18,12 @@ module type S = sig
 
   val get_footprint_access_path: t -> AccessPath.t option
 
-  (** return Some (kind) if the call site is a taint source, None otherwise *)
+  (** return Some (source) if the call site is a taint source, None otherwise *)
   val get : CallSite.t -> t option
+
+  (** return each formal of the function paired with either Some(source) if the formal is a taint
+      source, or None if the formal is not a taint source *)
+  val get_tainted_formals : Procdesc.t -> (Mangled.t * Typ.t * t option) list
 end
 
 module Dummy : S with type t = unit

infer/src/quandary/CppTrace.ml

@@ -79,6 +79,9 @@ module CppSource = struct
     | pname ->
         failwithf "Non-C++ procname %a in C++ analysis@." Procname.pp pname
 
+  let get_tainted_formals pdesc =
+    IList.map (fun (name, typ) -> name, typ, None) (Procdesc.get_formals pdesc)
+
   let with_callsite t callee_site =
     { t with site = callee_site; }
 

infer/src/quandary/JavaTrace.ml

@@ -81,6 +81,41 @@ module JavaSource = struct
     | pname when BuiltinDecl.is_declared pname -> None
     | pname -> failwithf "Non-Java procname %a in Java analysis@." Procname.pp pname
 
+  let get_tainted_formals pdesc =
+    let make_untainted (name, typ) =
+      name, typ, None in
+    let taint_formals_with_types type_strs kind pdesc formals =
+      let taint_formal_with_types ((formal_name, formal_typ) as formal) =
+        let matches_classname typ typ_str = match typ with
+          | Typ.Tptr (Tstruct typename, _) -> Typename.name typename = typ_str
+          | _ -> false in
+        if IList.mem matches_classname formal_typ type_strs
+        then
+          let site = CallSite.make (Procdesc.get_proc_name pdesc) (Procdesc.get_loc pdesc) in
+          formal_name, formal_typ, Some (make kind site)
+        else
+          make_untainted formal in
+      IList.map taint_formal_with_types formals in
+
+    let formals = Procdesc.get_formals pdesc in
+    match Procdesc.get_proc_name pdesc with
+    | Procname.Java java_pname ->
+        begin
+          match Procname.java_get_class_name java_pname, Procname.java_get_method java_pname with
+          | "codetoanalyze.java.quandary.TaintedFormals", "taintedContextBad" ->
+              taint_formals_with_types
+                ["java.lang.Integer"; "java.lang.String"]
+                Other
+                pdesc
+                formals
+          | _ ->
+              IList.map make_untainted formals
+        end
+    | procname ->
+        failwithf
+          "Non-Java procedure %a where only Java procedures are expected"
+          Procname.pp procname
+
   let with_callsite t callee_site =
     { t with site = callee_site; }
 

infer/src/quandary/TaintAnalysis.ml

@@ -19,8 +19,8 @@ module Make (TaintSpecification : TaintSpec.S) = struct
   module TaintDomain = TaintSpecification.AccessTree
   module IdMapDomain = IdAccessPathMapDomain
 
-  (** map from formals to their position *)
-  type formal_map = int AccessPath.BaseMap.t
+  (** a map from a formal to its position and (optionally) whether we should treat it as a source *)
+  type formal_map = (int * TraceDomain.Source.t option) AccessPath.BaseMap.t
 
   module Summary = Summary.Make(struct
       type summary = QuandarySummary.t
@@ -90,13 +90,6 @@ module Make (TaintSpecification : TaintSpec.S) = struct
 
     type extras = formal_map
 
-    let is_formal base formal_map =
-      AccessPath.BaseMap.mem base formal_map
-
-    let is_rooted_in_environment ap formal_map =
-      let root, _ = AccessPath.extract ap in
-      is_formal root formal_map || is_global root
-
     let resolve_id id_map id =
       try Some (IdMapDomain.find id id_map)
       with Not_found -> None
@@ -116,8 +109,14 @@ module Make (TaintSpecification : TaintSpec.S) = struct
             Some (TaintDomain.make_normal_leaf trace) in
           let root, _ = AccessPath.extract access_path in
           try
-            let formal_num = AccessPath.BaseMap.find root proc_data.extras in
-            make_footprint_trace (make_footprint_access_path formal_num access_path)
+            let formal_num, taint_opt = AccessPath.BaseMap.find root proc_data.extras in
+            begin
+              match taint_opt with
+              | None ->
+                  make_footprint_trace (make_footprint_access_path formal_num access_path)
+              | Some source ->
+                  Some (TaintDomain.make_normal_leaf (TraceDomain.of_source source))
+            end
           with Not_found ->
             if is_global root
             then make_footprint_trace access_path
@@ -502,7 +501,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
         (fun base node acc ->
            let base' =
              try
-               let formal_index = AccessPath.BaseMap.find base formal_map in
+               let formal_index, _ = AccessPath.BaseMap.find base formal_map in
                make_footprint_var formal_index, snd base
              with Not_found ->
                base in
@@ -533,15 +532,15 @@ module Make (TaintSpecification : TaintSpec.S) = struct
 
     let make_extras pdesc =
       let pname = Procdesc.get_proc_name pdesc in
-      let attrs = Procdesc.get_attributes pdesc in
       let formals_with_nums =
         IList.mapi
-          (fun index (name, typ) ->
+          (fun index (name, typ, taint_opt) ->
              let pvar = Pvar.mk name pname in
-             AccessPath.base_of_pvar pvar typ, index)
-          attrs.ProcAttributes.formals in
+             AccessPath.base_of_pvar pvar typ, index, taint_opt)
+          (TraceDomain.Source.get_tainted_formals pdesc) in
       IList.fold_left
-        (fun formal_map (base, index) -> AccessPath.BaseMap.add base index formal_map)
+        (fun formal_map (base, index, taint_opt) ->
+           AccessPath.BaseMap.add base (index, taint_opt) formal_map)
         AccessPath.BaseMap.empty
         formals_with_nums in
 

infer/src/unit/TaintTests.ml

@@ -45,6 +45,7 @@ module MockTrace = Trace.Make(struct
         then Some site
         else None
 
+      let get_tainted_formals _ = assert false
       let is_footprint _ = false
       let make_footprint _ = assert false
       let get_footprint_access_path _ = assert false

infer/src/unit/TraceTests.ml

@@ -68,6 +68,7 @@ module MockSource = struct
   let make_footprint _ _ = Footprint
 
   let get _ = assert false
+  let get_tainted_formals _ = []
   let get_footprint_access_path _ = assert false
 end
 

infer/tests/codetoanalyze/java/quandary/TaintedFormals.java

@@ -0,0 +1,56 @@
+/*
+ * 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;
+
+class Obj {
+  Object f;
+}
+
+public class TaintedFormals {
+
+  public void callSink(Object formal) {
+    InferTaint.inferSensitiveSink(formal);
+  }
+
+  // taintedFormal1 and taintedFormal2 were are modeled as tainted
+  public void taintedContextBad(String taintedFormal1, Boolean untaintedFormal, Integer taintedFormal2) {
+    InferTaint.inferSensitiveSink(taintedFormal1); // should report here
+    InferTaint.inferSensitiveSink(taintedFormal2); // should report here
+    callSink(taintedFormal1); // should report here
+    callSink(taintedFormal2); // should report here
+
+    InferTaint.inferSensitiveSink(untaintedFormal); // should not report here
+  }
+
+  public Object taintedContextBad(String taintedFormal) {
+    return taintedFormal;
+  }
+
+  public void callTaintedContextBad1(String formal) {
+    Object tainted = taintedContextBad(formal);
+    InferTaint.inferSensitiveSink(tainted);
+  }
+
+  public void callTaintedContextBad2() {
+    taintedContextBad(null, (Boolean) InferTaint.inferSecretSource(), null);
+  }
+
+  public void callTaintedContextOk1() {
+    taintedContextBad("foo", null, null);
+  }
+
+  // shouldn't report here, otherwise we will double report
+  public void callTaintedContextOk2() {
+    taintedContextBad(null, null, new Integer(1));
+  }
+
+}

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

@@ -175,4 +175,10 @@ codetoanalyze/java/quandary/Strings.java, void Strings.viaStringBufferIgnoreRetu
 codetoanalyze/java/quandary/Strings.java, void Strings.viaStringBuilderBad(), 3, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),call to void InferTaint.inferSensitiveSink(Object)]
 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/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,Boolean,Integer),call to void InferTaint.inferSensitiveSink(Object)]
+codetoanalyze/java/quandary/TaintedFormals.java, void TaintedFormals.taintedContextBad(String,Boolean,Integer), 1, QUANDARY_TAINT_ERROR, [return from void TaintedFormals.taintedContextBad(String,Boolean,Integer),call to void InferTaint.inferSensitiveSink(Object)]
+codetoanalyze/java/quandary/TaintedFormals.java, void TaintedFormals.taintedContextBad(String,Boolean,Integer), 2, QUANDARY_TAINT_ERROR, [return from void TaintedFormals.taintedContextBad(String,Boolean,Integer),call to void InferTaint.inferSensitiveSink(Object)]
+codetoanalyze/java/quandary/TaintedFormals.java, void TaintedFormals.taintedContextBad(String,Boolean,Integer), 3, QUANDARY_TAINT_ERROR, [return from void TaintedFormals.taintedContextBad(String,Boolean,Integer),call to void TaintedFormals.callSink(Object),call to void InferTaint.inferSensitiveSink(Object)]
+codetoanalyze/java/quandary/TaintedFormals.java, void TaintedFormals.taintedContextBad(String,Boolean,Integer), 4, QUANDARY_TAINT_ERROR, [return from void TaintedFormals.taintedContextBad(String,Boolean,Integer),call to void TaintedFormals.callSink(Object),call to void InferTaint.inferSensitiveSink(Object)]
 codetoanalyze/java/quandary/UnknownCode.java, void UnknownCode.propagateViaUnknownConstructorBad(), 4, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),call to void InferTaint.inferSensitiveSink(Object)]