[quandary] model some formals of Webview methods as tainted

Reviewed By: mburman

Differential Revision: D4378743

fbshipit-source-id: 5c7e21a

infer/src/checkers/Sink.ml

@@ -16,7 +16,7 @@ module type Kind = sig
   include TraceElem.Kind
 
   (** return the parameter index and sink kind for the given call site with the given actuals *)
-  val get : Procname.t -> (Exp.t * Typ.t) list -> (t * int * bool) list
+  val get : Procname.t -> (Exp.t * Typ.t) list -> Tenv.t -> (t * int * bool) list
 end
 
 module type S = sig
@@ -34,7 +34,7 @@ module type S = sig
     }
 
   (** return the parameter index and sink kind for the given call site with the given actuals *)
-  val get : CallSite.t -> (Exp.t * Typ.t) list -> parameter list
+  val get : CallSite.t -> (Exp.t * Typ.t) list -> Tenv.t -> parameter list
 end
 
 module Make (Kind : Kind) = struct
@@ -72,11 +72,11 @@ module Make (Kind : Kind) = struct
   let make_sink_param sink index ~report_reachable =
     { sink; index; report_reachable; }
 
-  let get site actuals =
+  let get site actuals tenv =
     IList.map
       (fun (kind, index, report_reachable) ->
          make_sink_param (make kind site) index ~report_reachable)
-      (Kind.get (CallSite.pname site) actuals)
+      (Kind.get (CallSite.pname site) actuals tenv)
 
   let with_callsite t callee_site =
     { t with site = callee_site; }

infer/src/checkers/Sink.mli

@@ -13,7 +13,7 @@ module type Kind = sig
   include TraceElem.Kind
 
   (** return the parameter index and sink kind for the given call site with the given actuals *)
-  val get : Procname.t -> (Exp.t * Typ.t) list -> (t * int * bool) list
+  val get : Procname.t -> (Exp.t * Typ.t) list -> Tenv.t -> (t * int * bool) list
 end
 
 module type S = sig
@@ -31,7 +31,7 @@ module type S = sig
     }
 
   (** return the parameter index and sink kind for the given call site with the given actuals *)
-  val get : CallSite.t -> (Exp.t * Typ.t) list -> parameter list
+  val get : CallSite.t -> (Exp.t * Typ.t) list -> Tenv.t -> parameter list
 end
 
 module Make (Kind : Kind) : S with module Kind = Kind

infer/src/checkers/SinkTrace.ml

@@ -34,7 +34,7 @@ module MakeSink(TraceElem : TraceElem.S) = struct
   include TraceElem
   type parameter = { sink : t; index : int; report_reachable : bool; }
 
-  let get _ _ = []
+  let get _ _ _ = []
 end
 
 module Make (TraceElem : TraceElem.S) = struct

infer/src/checkers/Source.ml

@@ -23,9 +23,7 @@ module type Kind = sig
 
   val get : Procname.t -> t option
 
-  (** return each formal of the function paired with either Some(kind) if the formal is a taint
+  val get_tainted_formals : Procdesc.t -> Tenv.t -> (Mangled.t * Typ.t * t option) list
-      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 type S = sig
@@ -39,7 +37,7 @@ module type S = sig
 
   val get : CallSite.t -> t option
 
-  val get_tainted_formals : Procdesc.t -> (Mangled.t * Typ.t * t option) list
+  val get_tainted_formals : Procdesc.t -> Tenv.t -> (Mangled.t * Typ.t * t option) list
 end
 
 module Make (Kind : Kind) = struct
@@ -86,11 +84,11 @@ module Make (Kind : Kind) = struct
     | Some kind -> Some (make kind site)
     | None -> None
 
-  let get_tainted_formals pdesc =
+  let get_tainted_formals pdesc tenv =
     let site = CallSite.make (Procdesc.get_proc_name pdesc) (Procdesc.get_loc pdesc) in
     IList.map
       (fun (name, typ, kind_opt) -> name, typ, Option.map kind_opt ~f:(fun kind -> make kind site))
-      (Kind.get_tainted_formals pdesc)
+      (Kind.get_tainted_formals pdesc tenv)
 
   let with_callsite t callee_site =
     { t with site = callee_site; }
@@ -123,7 +121,7 @@ module Dummy = struct
 
   let get _ = None
 
-  let get_tainted_formals pdesc =
+  let get_tainted_formals pdesc _=
     IList.map (fun (name, typ) -> name, typ, None) (Procdesc.get_formals pdesc)
 
   module Kind = struct

infer/src/checkers/Source.mli

@@ -23,7 +23,7 @@ module type Kind = sig
 
   (** return each formal of the function paired with either Some(kind) 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
+  val get_tainted_formals : Procdesc.t -> Tenv.t -> (Mangled.t * Typ.t * t option) list
 end
 
 module type S = sig
@@ -43,7 +43,7 @@ module type S = sig
 
   (** 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
+  val get_tainted_formals : Procdesc.t -> Tenv.t -> (Mangled.t * Typ.t * t option) list
 end
 
 module Make (Kind : Kind) : S with module Kind = Kind

infer/src/checkers/patternMatch.ml

@@ -43,6 +43,17 @@ let rec supertype_exists tenv pred name =
   | None ->
       false
 
+let rec supertype_find_map_opt tenv f name =
+  match Tenv.lookup tenv name with
+  | Some ({supers} as struct_typ) ->
+      begin
+        match f name struct_typ with
+        | None -> IList.find_map_opt (supertype_find_map_opt tenv f) supers
+        | result -> result
+      end
+  | None ->
+      None
+
 let is_immediate_subtype tenv this_type_name super_type_name =
   match Tenv.lookup tenv this_type_name with
   | Some {supers} -> IList.exists (Typename.equal super_type_name) supers

infer/src/checkers/patternMatch.mli

@@ -62,6 +62,11 @@ val is_subtype_of_str : Tenv.t -> Typename.t -> string -> bool
 (** Holds iff the predicate holds on a supertype of the named type, including the type itself *)
 val supertype_exists : Tenv.t -> (Typename.t -> StructTyp.t -> bool) -> Typename.t -> bool
 
+(** Return the first non-None result found when applying the given function to supertypes of the
+    named type, including the type itself *)
+val supertype_find_map_opt :
+  Tenv.t -> (Typename.t -> StructTyp.t -> 'a option) -> Typename.t -> 'a option
+
 (** Get the name of the type of a constant *)
 val java_get_const_type_name : Const.t -> string
 

infer/src/quandary/CppTrace.ml

@@ -42,7 +42,7 @@ module Kind = struct
     | pname ->
         failwithf "Non-C++ procname %a in C++ analysis@." Procname.pp pname
 
-  let get_tainted_formals pdesc =
+  let get_tainted_formals pdesc _ =
     Source.all_formals_untainted pdesc
 
   let pp fmt = function
@@ -60,7 +60,7 @@ module SinkKind = struct
     | Other (** for testing or uncategorized sinks *)
   [@@deriving compare]
 
-  let get pname actuals =
+  let get pname actuals _ =
     let taint_all actuals kind ~report_reachable =
       IList.mapi
         (fun actual_num _ -> kind, actual_num, report_reachable)

infer/src/quandary/JavaTrace.ml

@@ -48,7 +48,7 @@ module SourceKind = 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 get_tainted_formals pdesc _ =
     let make_untainted (name, typ) =
       name, typ, None in
     let taint_formals_with_types type_strs kind formals =
@@ -69,10 +69,7 @@ module SourceKind = struct
         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
+              taint_formals_with_types ["java.lang.Integer"; "java.lang.String"] Other formals
-                ["java.lang.Integer"; "java.lang.String"]
-                Other
-                formals
           | _ ->
               Source.all_formals_untainted pdesc
         end
@@ -93,11 +90,12 @@ module JavaSource = Source.Make(SourceKind)
 module SinkKind = struct
   type t =
     | Intent (** sink that trusts an Intent *)
+    | JavaScript (** sink that passes its arguments to untrusted JS code *)
     | Logging (** sink that logs one or more of its arguments *)
     | Other (** for testing or uncategorized sinks *)
   [@@deriving compare]
 
-  let get pname actuals =
+  let get pname actuals tenv =
     (* taint all the inputs of [pname]. for non-static procedures, taints the "this" parameter only
        if [taint_this] is true. *)
     let taint_all ?(taint_this=false) kind ~report_reachable =
@@ -155,14 +153,42 @@ module SinkKind = struct
               taint_all Logging ~report_reachable:true
           | "com.facebook.infer.builtins.InferTaint", "inferSensitiveSink" ->
               [Other, 0, false]
+          | class_name, method_name ->
+              let taint_matching_supertype typename _ =
+                match Typename.name typename, method_name with
+                | "android.webkit.WebChromeClient",
+                  ("onJsAlert" | "onJsBeforeUnload" | "onJsConfirm" | "onJsPrompt") ->
+                    Some (taint_all JavaScript ~report_reachable:true)
+                | "android.webkit.WebView",
+                  ("addJavascriptInterface" |
+                   "evaluateJavascript" |
+                   "loadData" |
+                   "loadDataWithBaseURL" |
+                   "loadUrl" |
+                   "postWebMessage") ->
+                    Some (taint_all JavaScript ~report_reachable:true)
+                | "android.webkit.WebViewClient",
+                  ("onLoadResource" | "shouldInterceptRequest" | "shouldOverrideUrlLoading") ->
+                    Some (taint_all JavaScript ~report_reachable:true)
                 | _ ->
-              []
+                    None in
+              begin
+                match
+                  PatternMatch.supertype_find_map_opt
+                    tenv
+                    taint_matching_supertype
+                    (Typename.Java.from_string class_name) with
+                | Some sinks -> sinks
+                | None -> []
+              end
+
         end
     | pname when BuiltinDecl.is_declared pname -> []
     | pname -> failwithf "Non-Java procname %a in Java analysis@." Procname.pp pname
 
   let pp fmt = function
     | Intent -> F.fprintf fmt "Intent"
+    | JavaScript -> F.fprintf fmt "JavaScript"
     | Logging -> F.fprintf fmt "Logging"
     | Other -> F.fprintf fmt "Other"
 end
@@ -178,6 +204,7 @@ include
       match Source.kind source, Sink.kind sink with
       | PrivateData, Logging
       | Intent, Intent
+      | (Intent | PrivateData), JavaScript
       | Other, _ | _, Other ->
           true
       | _ ->

infer/src/quandary/TaintAnalysis.ml

@@ -428,7 +428,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
           let analyze_call astate_acc callee_pname =
             let call_site = CallSite.make callee_pname callee_loc in
 
-            let sinks = TraceDomain.Sink.get call_site actuals in
+            let sinks = TraceDomain.Sink.get call_site actuals proc_data.ProcData.tenv in
             let astate_with_sink = match sinks with
               | [] -> astate
               | sinks -> add_sinks sinks actuals astate proc_data call_site in
@@ -513,7 +513,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
 
   module Interprocedural = AbstractInterpreter.Interprocedural(Summary)
 
-  let checker callback =
+  let checker ({ Callbacks.tenv } as callback) =
 
     let compute_post (proc_data : formal_map ProcData.t) =
       if not (Procdesc.did_preanalysis proc_data.pdesc)
@@ -537,7 +537,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
           (fun index (name, typ, taint_opt) ->
              let pvar = Pvar.mk name pname in
              AccessPath.base_of_pvar pvar typ, index, taint_opt)
-          (TraceDomain.Source.get_tainted_formals pdesc) in
+          (TraceDomain.Source.get_tainted_formals pdesc tenv) in
       IList.fold_left
         (fun formal_map (base, index, taint_opt) ->
            AccessPath.BaseMap.add base (index, taint_opt) formal_map)

infer/src/unit/TaintTests.ml

@@ -23,14 +23,14 @@ module MockTrace = Trace.Make(struct
           then Some (CallSite.make pname Location.dummy)
           else None
 
-        let get_tainted_formals _ =
+        let get_tainted_formals _ _ =
           []
       end)
 
     module Sink = Sink.Make(struct
         include MockTraceElem
 
-        let get pname _ =
+        let get pname _ _ =
           if String.is_prefix ~prefix:"SINK" (Procname.to_string pname)
           then [CallSite.make pname Location.dummy, 0, false]
           else []

infer/tests/codetoanalyze/java/quandary/WebViews.java

@@ -0,0 +1,85 @@
+/*
+ * 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 android.content.Context;
+import android.webkit.JavascriptInterface;
+import android.webkit.WebView;
+import android.webkit.WebViewClient;
+import android.webkit.WebChromeClient;
+
+import com.facebook.infer.builtins.InferTaint;
+
+public class WebViews {
+
+  void callWebviewSinks(WebView webview) {
+    String stringSource = (String) InferTaint.inferSecretSource();
+
+    webview.addJavascriptInterface(new Object(), stringSource);
+    webview.evaluateJavascript(stringSource, null);
+    webview.loadData(stringSource, "", "");
+    webview.loadDataWithBaseURL("", stringSource, "", "", "");
+    webview.loadUrl(stringSource); // should have 5 reports
+  }
+
+  void callWebviewClientSinks(WebView webview, WebViewClient client) {
+    String stringSource = (String) InferTaint.inferSecretSource();
+
+    client.onLoadResource(webview, stringSource);
+    client.shouldInterceptRequest(webview, stringSource);
+    client.shouldOverrideUrlLoading(webview, stringSource); // should have 3 reports
+  }
+
+  void callWebviewChromeClientSinks(WebView webview, WebChromeClient client) {
+    String stringSource = (String) InferTaint.inferSecretSource();
+
+    client.onJsAlert(webview, stringSource, "", null);
+    client.onJsBeforeUnload(webview, stringSource, "", null);
+    client.onJsConfirm(webview, stringSource, "", null);
+    client.onJsPrompt(webview, stringSource, "", "", null); // should have 4 reports
+  }
+
+  // make sure all of the rules apply to subclasses as well
+  class MyWebView extends WebView {
+    public MyWebView(Context c) {
+      super(c);
+    }
+  }
+
+  class MyWebViewClient extends WebViewClient {
+  }
+
+  class MyWebChromeClient extends WebChromeClient {
+  }
+
+  void callWebviewSubclassSinks(
+    MyWebView webview, MyWebViewClient client, MyWebChromeClient chromeClient) {
+
+    String stringSource = (String) InferTaint.inferSecretSource();
+    webview.evaluateJavascript(stringSource, null);
+    client.onLoadResource(webview, stringSource);
+    chromeClient.onJsAlert(webview, stringSource, "", null); // should have 3 reports
+  }
+
+  class JsObject {
+    @JavascriptInterface
+    Object returnSource() {
+      return InferTaint.inferSecretSource();
+    }
+  }
+
+  // in order to get this, we have to understand that addJavaScriptInterface can evaluate the
+  // JsObject.returnSource method
+  void FN_addJavascriptInterface(MyWebView webview) {
+    // should warn here
+    webview.addJavascriptInterface(new JsObject(), "injectedObject");
+  }
+
+}

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

@@ -167,3 +167,18 @@ codetoanalyze/java/quandary/TaintedFormals.java, void TaintedFormals.taintedCont
 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)]
+codetoanalyze/java/quandary/WebViews.java, void WebViews.callWebviewChromeClientSinks(WebView,WebChromeClient), 3, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),call to boolean WebChromeClient.onJsAlert(WebView,String,String,JsResult)]
+codetoanalyze/java/quandary/WebViews.java, void WebViews.callWebviewChromeClientSinks(WebView,WebChromeClient), 4, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),call to boolean WebChromeClient.onJsBeforeUnload(WebView,String,String,JsResult)]
+codetoanalyze/java/quandary/WebViews.java, void WebViews.callWebviewChromeClientSinks(WebView,WebChromeClient), 5, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),call to boolean WebChromeClient.onJsConfirm(WebView,String,String,JsResult)]
+codetoanalyze/java/quandary/WebViews.java, void WebViews.callWebviewChromeClientSinks(WebView,WebChromeClient), 6, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),call to boolean WebChromeClient.onJsPrompt(WebView,String,String,String,JsPromptResult)]
+codetoanalyze/java/quandary/WebViews.java, void WebViews.callWebviewClientSinks(WebView,WebViewClient), 3, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),call to void WebViewClient.onLoadResource(WebView,String)]
+codetoanalyze/java/quandary/WebViews.java, void WebViews.callWebviewClientSinks(WebView,WebViewClient), 4, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),call to WebResourceResponse WebViewClient.shouldInterceptRequest(WebView,String)]
+codetoanalyze/java/quandary/WebViews.java, void WebViews.callWebviewClientSinks(WebView,WebViewClient), 5, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),call to boolean WebViewClient.shouldOverrideUrlLoading(WebView,String)]
+codetoanalyze/java/quandary/WebViews.java, void WebViews.callWebviewSinks(WebView), 3, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),call to void WebView.addJavascriptInterface(Object,String)]
+codetoanalyze/java/quandary/WebViews.java, void WebViews.callWebviewSinks(WebView), 4, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),call to void WebView.evaluateJavascript(String,ValueCallback)]
+codetoanalyze/java/quandary/WebViews.java, void WebViews.callWebviewSinks(WebView), 5, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),call to void WebView.loadData(String,String,String)]
+codetoanalyze/java/quandary/WebViews.java, void WebViews.callWebviewSinks(WebView), 6, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),call to void WebView.loadDataWithBaseURL(String,String,String,String,String)]
+codetoanalyze/java/quandary/WebViews.java, void WebViews.callWebviewSinks(WebView), 7, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),call to void WebView.loadUrl(String)]
+codetoanalyze/java/quandary/WebViews.java, void WebViews.callWebviewSubclassSinks(WebViews$MyWebView,WebViews$MyWebViewClient,WebViews$MyWebChromeClient), 4, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),call to void WebView.evaluateJavascript(String,ValueCallback)]
+codetoanalyze/java/quandary/WebViews.java, void WebViews.callWebviewSubclassSinks(WebViews$MyWebView,WebViews$MyWebViewClient,WebViews$MyWebChromeClient), 5, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),call to void WebViewClient.onLoadResource(WebView,String)]
+codetoanalyze/java/quandary/WebViews.java, void WebViews.callWebviewSubclassSinks(WebViews$MyWebView,WebViews$MyWebViewClient,WebViews$MyWebChromeClient), 6, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),call to boolean WebChromeClient.onJsAlert(WebView,String,String,JsResult)]