diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 67695198a..cc028c536 100644 --- a/infer/src/backend/interproc.ml +++ b/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 (); diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index c97ed027e..13ef81264 100644 --- a/infer/src/backend/tabulation.ml +++ b/infer/src/backend/tabulation.ml @@ -746,35 +746,45 @@ let combine print_results actual_pre (IList.map fst results); Some results +(* 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 + | Sil.Hpointsto (Sil.Lvar pvar, (Sil.Eexp (rhs, _)), _) + 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 + +(* 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 - 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 *) - IList.fold_left - (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 - | _ -> prop_acc) - 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 - (Prop.expose pre') + 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. *) diff --git a/infer/src/backend/tabulation.mli b/infer/src/backend/tabulation.mli index 2c5da35d5..16b421373 100644 --- a/infer/src/backend/tabulation.mli +++ b/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 diff --git a/infer/src/harness/androidFramework.ml b/infer/src/harness/androidFramework.ml index 106b21dcc..aaed199aa 100644 --- a/infer/src/harness/androidFramework.ml +++ b/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 *) diff --git a/infer/src/harness/androidFramework.mli b/infer/src/harness/androidFramework.mli index 79fa91c5e..c57e17c45 100644 --- a/infer/src/harness/androidFramework.mli +++ b/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 diff --git a/infer/tests/codetoanalyze/objc/errors/taint/viewController.m b/infer/tests/codetoanalyze/objc/errors/taint/viewController.m new file mode 100644 index 000000000..d64b7e4dd --- /dev/null +++ b/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 +#import + +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 diff --git a/infer/tests/endtoend/objc/TaintTest.java b/infer/tests/endtoend/objc/TaintTest.java new file mode 100644 index 000000000..4ea336c75 --- /dev/null +++ b/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 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 + ) + ); + } + +}