Extended framework for taint analysis

Reviewed By: sblackshear

Differential Revision: D2739191

fb-gh-sync-id: 5c66a48

infer/src/backend/interproc.ml

@@ -536,6 +536,7 @@ let forward_tabulate cfg tenv =
     let sid_curr_node = Cfg.Node.get_id curr_node in
     let proc_desc = Cfg.Node.get_proc_desc curr_node in
     let proc_name = Cfg.Procdesc.get_proc_name proc_desc in
+    let formal_params = Cfg.Procdesc.get_formals proc_desc in
     let summary = Specs.get_summary_unsafe "forward_tabulate" proc_name in
     mark_visited summary curr_node; (* mark nodes visited in fp and re phases *)
     let session =
@@ -582,6 +583,10 @@ let forward_tabulate cfg tenv =
           exe_iter
             (fun prop path cnt num_paths ->
                try
+                 let prop = if !Config.taint_analysis then
+                     let tainted_params = Taint.tainted_params proc_name in
+                     Tabulation.add_param_taint proc_name formal_params prop tainted_params
+                   else prop in
                  L.d_strln ("Processing prop " ^ string_of_int cnt ^ "/" ^ string_of_int num_paths);
                  L.d_increase_indent 1;
                  State.reset_diverging_states_goto_node ();

infer/src/backend/tabulation.ml

@@ -746,35 +746,45 @@ let combine
     print_results actual_pre (IList.map fst results);
     Some results
 
-let mk_pre pre formal_params callee_pname =
-  if !Config.taint_analysis then
-    match Taint.accepts_sensitive_params callee_pname with
-    | [] -> pre
-    | param_nums ->
-        let add_param_untaint prop param =
-          (* TODO: we should be able to add the taint attribute directly to the pvar. fix the taint
-             analysis so that it uses Prover.check_equal and gets the right answer here *)
+(* add tainting attribute to a pvar in a prop *)
+let add_tainting_attribute att pvar_param prop =
   IList.fold_left
-            (fun prop_acc hpred -> match hpred with
+    (fun prop_acc hpred ->
+       match hpred with
        | Sil.Hpointsto (Sil.Lvar pvar, (Sil.Eexp (rhs, _)), _)
-                 when Sil.pvar_equal pvar param ->
-                   Prop.add_or_replace_exp_attribute prop_acc rhs Sil.Auntaint
+         when Sil.pvar_equal pvar pvar_param ->
+           L.d_strln ("TAINT ANALYSIS: setting taint/untaint attribute of parameter " ^
+                      (Sil.pvar_to_string pvar));
+           Prop.add_or_replace_exp_attribute prop_acc rhs att
        | _ -> prop_acc)
+    prop (Prop.get_sigma prop)
+
+(* add tainting attributes to a list of paramenters *)
+let add_tainting_att_param_list prop param_nums formal_params att =
+  try
+    IList.map (fun n -> IList.nth formal_params n) param_nums
+    |> IList.fold_left (fun prop param -> add_tainting_attribute att param prop) prop
+  with Failure _ | Invalid_argument _  ->
+    L.d_strln ("TAINT ANALYSIS: WARNING, tainting framework " ^
+               "specifies incorrect parameter number " ^
+               " to be set as tainted/untainted ");
     prop
-            (Prop.get_sigma prop) in
-        let add_param_untaint_if_nums_match prop param_num param =
-          if IList.exists (fun num -> num = param_num) param_nums then
-            add_param_untaint prop param
-          else prop in
-        let pre', _ =
-          IList.fold_left
-            (fun (prop_acc, param_num) param ->
-               (add_param_untaint_if_nums_match prop_acc param_num param, param_num + 1))
-            (Prop.normalize pre, 0)
-            formal_params in
+
+(* Set Ataint attribute to list of parameteres in a prop *)
+let add_param_taint proc_name formal_params prop param_nums =
+  let formal_params' = IList.map
+      (fun (p, _) -> Sil.mk_pvar (Mangled.from_string p) proc_name) formal_params in
+  add_tainting_att_param_list prop param_nums formal_params' (Sil.Ataint proc_name)
+
+(* add Auntaint attribute to a callee_pname precondition *)
+let mk_pre pre formal_params callee_pname =
+  if !Config.taint_analysis then
+    let pre' = add_tainting_att_param_list (Prop.normalize pre)
+        (Taint.accepts_sensitive_params callee_pname) formal_params (Sil.Auntaint) in
     (Prop.expose pre')
   else pre
 
+
 (** Construct the actual precondition: add to the current state a copy
     of the (callee's) formal parameters instantiated with the actual
     parameters. *)

infer/src/backend/tabulation.mli

@@ -43,3 +43,8 @@ val exe_function_call:
   Sil.tenv -> Cfg.cfg -> Ident.t list -> Cfg.Procdesc.t -> Procname.t -> Location.t ->
   (Sil.exp * Sil.typ) list -> Prop.normal Prop.t -> Paths.Path.t ->
   (Prop.normal Prop.t * Paths.Path.t) list
+
+(* Set Ataint attribute to list of parameteres in a prop *)
+val add_param_taint :
+  Procname.t -> (string * Sil.typ) list -> Prop.normal Prop.t ->
+  int list -> Prop.normal Prop.t

infer/src/harness/androidFramework.ml

@@ -13,23 +13,6 @@ module TypSet = Sil.TypSet
 
 open Utils
 
-type java_method_str = {
-  classname : string;
-  method_name : string;
-  ret_type : string;
-  params : string list;
-  is_static : bool
-}
-
-(* turn string specificiation of Java method into a procname *)
-let java_method_to_procname java_method =
-  Procname.mangled_java
-    (Procname.split_classname java_method.classname)
-    (Some (Procname.split_classname java_method.ret_type))
-    java_method.method_name
-    (IList.map Procname.split_classname java_method.params)
-    (if java_method.is_static then Procname.Static else Procname.Non_Static)
-
 (** Android lifecycle types and their lifecycle methods that are called by the framework *)
 
 (** work-in-progress list of known callback-registering method names *)

infer/src/harness/androidFramework.mli

@@ -11,16 +11,6 @@
 
 open Utils
 
-type java_method_str = {
-  classname : string;
-  method_name : string;
-  ret_type : string;
-  params : string list;
-  is_static : bool
-}
-
-val java_method_to_procname : java_method_str -> Procname.t
-
 (** return the complete list of (package, lifecycle_classname, lifecycle_methods) trios *)
 val get_lifecycles : (string * string * string list) list
 

infer/tests/codetoanalyze/objc/errors/taint/viewController.m

@@ -0,0 +1,94 @@
+/*
+* Copyright (c) 2015 - 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.
+*/
+
+#import <Foundation/Foundation.h>
+#import <UIKit/UIKit.h>
+
+BOOL ExampleSanitizer(NSURL * u, int f)
+{
+    if (f) __set_untaint_attribute(u);
+    return f;
+}
+
+@interface ExampleViewController : NSObject
+- (void)loadURL:(NSURL *)URL
+  trackingCodes:(NSArray *)trackingCodes;
+@end
+
+@implementation ExampleViewController
+- (void) dealloc
+{
+    [self dealloc];
+}
+- (void)loadURL:(NSURL *)URL
+  trackingCodes: (NSArray *)trackingCodes
+{
+    // Require untainted URL
+};
+@end
+
+@interface B : NSObject
+- (void) another_url_pass: (NSURL *) u;
+@end
+
+@implementation B
+- (void) dealloc
+{
+    [self dealloc];
+}
+- (void) another_url_pass: (NSURL *) u
+{
+    ExampleViewController *vc = [[ExampleViewController alloc] init];
+    [vc loadURL:u trackingCodes:nil];
+    [vc dealloc];
+}
+@end
+
+@interface A : NSObject
+- (void) pass_url_arond:(NSURL *) u;
+@end
+
+@implementation A
+- (void) dealloc
+{
+    [self dealloc];
+}
+- (void) pass_url_arond: (NSURL *) u
+{
+    B* b = [[B alloc] init];
+    [b another_url_pass:u];
+    [b dealloc];
+}
+@end
+
+@interface ExampleDelegate : NSObject
+- (BOOL)application: (UIApplication *)application
+            openURL: (NSURL *)URL
+  sourceApplication: (NSString *)sourceApplication
+         annotation: (id)annotation;
+@end
+
+@implementation ExampleDelegate
+- (BOOL)application: (UIApplication *)application
+            openURL: (NSURL *)URL
+  sourceApplication: (NSString *)sourceApplication
+         annotation: (id)annotation
+{
+    // Assume tainted URL;
+    A* a = [[A alloc] init];
+    if (!ExampleSanitizer(URL, 0 )) {
+        [a pass_url_arond:URL]; // report taint
+    }
+    if (!ExampleSanitizer(URL, 1 )) {
+        [a pass_url_arond:URL]; // No taint
+    }
+    [a dealloc];
+    return YES;
+}
+@end

infer/tests/endtoend/objc/TaintTest.java

@@ -0,0 +1,67 @@
+/*
+* Copyright (c) 2013 - 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 endtoend.objc;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static utils.matchers.ResultContainsExactly.containsExactly;
+
+import com.google.common.collect.ImmutableList;
+
+import org.junit.BeforeClass;
+import org.junit.ClassRule;
+import org.junit.Test;
+
+import java.io.IOException;
+
+import utils.DebuggableTemporaryFolder;
+import utils.InferException;
+import utils.InferResults;
+import utils.InferRunner;
+
+public class TaintTest {
+
+  public static final String TaintFile =
+      "infer/tests/codetoanalyze/objc/errors/taint/viewController.m";
+
+  public static final String TAINTED_VALUE = "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION";
+
+  private static ImmutableList<String> inferCmd;
+
+  @ClassRule
+  public static DebuggableTemporaryFolder folder = new DebuggableTemporaryFolder();
+
+
+  @BeforeClass
+  public static void runInfer() throws InterruptedException, IOException {
+    inferCmd = InferRunner.createObjCInferCommand(
+        folder,
+        TaintFile);
+  }
+
+  @Test
+  public void whenInferRunsOnTaintFileErrorFound()
+      throws InterruptedException, IOException, InferException {
+    InferResults inferResults = InferRunner.runInferObjC(inferCmd);
+    String[] methods = {
+        "application:openURL:sourceApplication:annotation:"
+    };
+
+    assertThat(
+        "Results should contain tainted value reaching sensitive function.",
+        inferResults,
+        containsExactly(
+            TAINTED_VALUE,
+            TaintFile,
+            methods
+        )
+    );
+  }
+
+}