From dcdebbd811a35af19938a29574e6e31047490e3c Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Wed, 25 Nov 2015 14:54:18 -0800 Subject: [PATCH] creating a framework for adding src/sink models based on method names/signatures alone Reviewed By: jeremydubreil Differential Revision: D2692136 fb-gh-sync-id: 12de038 --- .../com/facebook/infer/models/InferTaint.java | 24 ++++ infer/src/backend/procname.mli | 2 + infer/src/backend/tabulation.ml | 104 +++++++++++++----- infer/src/harness/androidFramework.ml | 17 +++ infer/src/harness/androidFramework.mli | 10 ++ infer/src/opensource/taint.ml | 18 +++ infer/src/opensource/taint.mli | 14 +++ infer/tests/ant_report.json | 20 ++++ infer/tests/buck_report.json | 20 ++++ .../java/infer/TaintExample.java | 27 +++++ .../tests/endtoend/java/infer/TaintTest.java | 4 + 11 files changed, 233 insertions(+), 27 deletions(-) create mode 100644 infer/models/java/src/com/facebook/infer/models/InferTaint.java create mode 100644 infer/src/opensource/taint.ml create mode 100644 infer/src/opensource/taint.mli diff --git a/infer/models/java/src/com/facebook/infer/models/InferTaint.java b/infer/models/java/src/com/facebook/infer/models/InferTaint.java new file mode 100644 index 000000000..df72d22aa --- /dev/null +++ b/infer/models/java/src/com/facebook/infer/models/InferTaint.java @@ -0,0 +1,24 @@ +/* +* 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 com.facebook.infer.models; + +public class InferTaint { + + public static Object inferSecretSource() { + Object o = InferUndefined.object_undefined(); + InferBuiltins.assume_allocated(o); + return o; + } + + public static void inferSensitiveSink(Object iMightBeTainted) { + + } + +} diff --git a/infer/src/backend/procname.mli b/infer/src/backend/procname.mli index 14ad4396d..370863a52 100644 --- a/infer/src/backend/procname.mli +++ b/infer/src/backend/procname.mli @@ -122,6 +122,8 @@ val is_class_initializer : t -> bool (** [is_infer_undefined pn] returns true if [pn] is a special Infer undefined proc *) val is_infer_undefined : t -> bool +val split_classname : string -> string option * string + (** Check if the procedure belongs to an anonymous inner class. *) val java_is_anonymous_inner_class : t -> bool diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index a54cb2083..bc1cc53f7 100644 --- a/infer/src/backend/tabulation.ml +++ b/infer/src/backend/tabulation.ml @@ -746,6 +746,35 @@ 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 *) + 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') + else pre + (** Construct the actual precondition: add to the current state a copy of the (callee's) formal parameters instantiated with the actual parameters. *) @@ -766,6 +795,52 @@ let mk_actual_precondition prop actual_params formal_params = let actual_pre = Prop.prop_sigma_star prop instantiated_formals in Prop.normalize actual_pre +let mk_posts ret_ids prop callee_pname posts = + match ret_ids with + | [ret_id] -> + let mk_getter_idempotent posts = + (* if we have seen a previous call to the same function, only use specs whose return value + is consistent with constraints on the return value of the previous call w.r.t to + nullness. meant to eliminate false NPE warnings from the common + "if (get() != null) get().something()" pattern *) + let last_call_ret_non_null = + IList.exists + (fun (exp, attr) -> + match attr with + | Sil.Aretval pname when Procname.equal callee_pname pname -> + Prover.check_disequal prop exp Sil.exp_zero + | _ -> false) + (Prop.get_all_attributes prop) in + if last_call_ret_non_null then + let returns_null prop = + IList.exists + (function + | Sil.Hpointsto (Sil.Lvar pvar, Sil.Eexp (e, _), _) when Sil.pvar_is_return pvar -> + Prover.check_equal (Prop.normalize prop) e Sil.exp_zero + | _ -> false) + (Prop.get_sigma prop) in + IList.filter (fun (prop, _) -> not (returns_null prop)) posts + else posts in + let mk_retval_tainted posts = + if Taint.returns_secret callee_pname then + let taint_retval (prop, path) = + let prop_normal = Prop.normalize prop in + let prop' = + Prop.add_or_replace_exp_attribute prop_normal + (Sil.Var ret_id) + (Sil.Ataint callee_pname) + |> Prop.expose in + (prop', path) in + IList.map taint_retval posts + else posts in + let posts' = + if !Config.idempotent_getters && !Config.curr_language = Config.Java + then mk_getter_idempotent posts + else posts in + if !Config.taint_analysis then mk_retval_tainted posts' else posts' + | _ -> posts + + (** Check if actual_pre * missing_footprint |- false *) let inconsistent_actualpre_missing actual_pre split_opt = match split_opt with @@ -881,34 +956,9 @@ let exe_spec tenv cfg ret_ids (n, nspecs) caller_pdesc callee_pname loc prop path_pre (spec : Prop.exposed Specs.spec) actual_params formal_params : abduction_res = let caller_pname = Cfg.Procdesc.get_proc_name caller_pdesc in - let posts = - match ret_ids with - | [ret_id] when !Config.idempotent_getters && !Config.curr_language = Config.Java -> - (* if we have seen a previous call to the same function, only use specs whose return value - is consistent with constraints on the return value of the previous call w.r.t to nullness. - meant to eliminate false NPE warnings from the common "if (get() != null) get().something()" - pattern *) - let last_call_ret_non_null = - IList.exists - (fun (exp, attr) -> - match attr with - | Sil.Aretval pname when Procname.equal callee_pname pname -> - Prover.check_disequal prop exp Sil.exp_zero - | _ -> false) - (Prop.get_all_attributes prop) in - if last_call_ret_non_null then - let returns_null prop = - IList.exists - (function - | Sil.Hpointsto (Sil.Lvar pvar, Sil.Eexp (e, _), _) when Sil.pvar_is_return pvar -> - Prover.check_equal (Prop.normalize prop) e Sil.exp_zero - | _ -> false) - (Prop.get_sigma prop) in - IList.filter (fun (prop, _) -> not (returns_null prop)) spec.Specs.posts - else spec.Specs.posts - | _ -> spec.Specs.posts in + let posts = mk_posts ret_ids prop callee_pname spec.Specs.posts in let actual_pre = mk_actual_precondition prop actual_params formal_params in - let spec_pre = Specs.Jprop.to_prop spec.Specs.pre in + let spec_pre = mk_pre (Specs.Jprop.to_prop spec.Specs.pre) formal_params callee_pname in L.d_strln ("EXECUTING SPEC " ^ string_of_int n ^ "/" ^ string_of_int nspecs); L.d_strln "ACTUAL PRECONDITION ="; L.d_increase_indent 1; Prop.d_prop actual_pre; L.d_decrease_indent 1; L.d_ln (); diff --git a/infer/src/harness/androidFramework.ml b/infer/src/harness/androidFramework.ml index f207b2ac4..9ca6fb22d 100644 --- a/infer/src/harness/androidFramework.ml +++ b/infer/src/harness/androidFramework.ml @@ -13,6 +13,23 @@ 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 351365068..c3b608719 100644 --- a/infer/src/harness/androidFramework.mli +++ b/infer/src/harness/androidFramework.mli @@ -11,6 +11,16 @@ 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/src/opensource/taint.ml b/infer/src/opensource/taint.ml new file mode 100644 index 000000000..61d416883 --- /dev/null +++ b/infer/src/opensource/taint.ml @@ -0,0 +1,18 @@ +(* + * 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. + *) + +module L = Logging + +open Utils + +(** returns true if [callee_pname] returns a tainted value *) +let returns_secret callee_pname = false + +(** returns list of zero-indexed argument numbers of [callee_pname] that may be tainted *) +let accepts_sensitive_params callee_pname = [] diff --git a/infer/src/opensource/taint.mli b/infer/src/opensource/taint.mli new file mode 100644 index 000000000..991397491 --- /dev/null +++ b/infer/src/opensource/taint.mli @@ -0,0 +1,14 @@ +(* + * 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. + *) + +(** returns true if [callee_pname] returns a tainted value *) +val returns_secret : Procname.t -> bool + +(** returns list of zero-indexed argument numbers of [callee_pname] that may be tainted *) +val accepts_sensitive_params : Procname.t -> int list diff --git a/infer/tests/ant_report.json b/infer/tests/ant_report.json index 4f749f588..ba0df7c3e 100644 --- a/infer/tests/ant_report.json +++ b/infer/tests/ant_report.json @@ -19,6 +19,21 @@ "file": "codetoanalyze/java/infer/ContextLeaks.java", "procedure": "void ContextLeaks.indirectLeak()" }, + { + "bug_type": "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION", + "file": "codetoanalyze/java/infer/TaintExample.java", + "procedure": "void TaintExample.interprocTaintErrorWithModelMethods1()" + }, + { + "bug_type": "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION", + "file": "codetoanalyze/java/infer/TaintExample.java", + "procedure": "void TaintExample.interprocTaintErrorWithModelMethods2()" + }, + { + "bug_type": "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION", + "file": "codetoanalyze/java/infer/TaintExample.java", + "procedure": "void TaintExample.interprocTaintErrorWithModelMethods3()" + }, { "bug_type": "CONTEXT_LEAK", "file": "codetoanalyze/java/infer/ContextLeaks.java", @@ -29,6 +44,11 @@ "file": "codetoanalyze/java/infer/ContextLeaks.java", "procedure": "void ContextLeaks.nonStaticInnerClassLeak()" }, + { + "bug_type": "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION", + "file": "codetoanalyze/java/infer/TaintExample.java", + "procedure": "void TaintExample.simpleTaintErrorWithModelMethods()" + }, { "bug_type": "CONTEXT_LEAK", "file": "codetoanalyze/java/infer/ContextLeaks.java", diff --git a/infer/tests/buck_report.json b/infer/tests/buck_report.json index f43e8fc77..75a9b8f7e 100644 --- a/infer/tests/buck_report.json +++ b/infer/tests/buck_report.json @@ -19,6 +19,21 @@ "file": "infer/tests/codetoanalyze/java/infer/ContextLeaks.java", "procedure": "void ContextLeaks.indirectLeak()" }, + { + "bug_type": "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION", + "file": "infer/tests/codetoanalyze/java/infer/TaintExample.java", + "procedure": "void TaintExample.interprocTaintErrorWithModelMethods1()" + }, + { + "bug_type": "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION", + "file": "infer/tests/codetoanalyze/java/infer/TaintExample.java", + "procedure": "void TaintExample.interprocTaintErrorWithModelMethods2()" + }, + { + "bug_type": "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION", + "file": "infer/tests/codetoanalyze/java/infer/TaintExample.java", + "procedure": "void TaintExample.interprocTaintErrorWithModelMethods3()" + }, { "bug_type": "CONTEXT_LEAK", "file": "infer/tests/codetoanalyze/java/infer/ContextLeaks.java", @@ -29,6 +44,11 @@ "file": "infer/tests/codetoanalyze/java/infer/ContextLeaks.java", "procedure": "void ContextLeaks.nonStaticInnerClassLeak()" }, + { + "bug_type": "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION", + "file": "infer/tests/codetoanalyze/java/infer/TaintExample.java", + "procedure": "void TaintExample.simpleTaintErrorWithModelMethods()" + }, { "bug_type": "CONTEXT_LEAK", "file": "infer/tests/codetoanalyze/java/infer/ContextLeaks.java", diff --git a/infer/tests/codetoanalyze/java/infer/TaintExample.java b/infer/tests/codetoanalyze/java/infer/TaintExample.java index be2fcde54..6037bbf1e 100644 --- a/infer/tests/codetoanalyze/java/infer/TaintExample.java +++ b/infer/tests/codetoanalyze/java/infer/TaintExample.java @@ -21,6 +21,8 @@ import javax.net.ssl.SSLSession; import javax.net.ssl.SSLSocket; import javax.net.ssl.SSLSocketFactory; +import com.facebook.infer.models.InferTaint; + public class TaintExample { public InputStream socketNotVerifiedSimple(SSLSocketFactory f) @@ -106,4 +108,29 @@ public class TaintExample { return s.getInputStream(); } + public void simpleTaintErrorWithModelMethods() { + Object o = InferTaint.inferSecretSource(); + InferTaint.inferSensitiveSink(o); + } + + public Object returnTaintedSourceModelMethods() { + return InferTaint.inferSecretSource(); + } + + public void callSinkMethodModelMethods(Object o) { + InferTaint.inferSensitiveSink(o); + } + + public void interprocTaintErrorWithModelMethods1() { + InferTaint.inferSensitiveSink(returnTaintedSourceModelMethods()); + } + + public void interprocTaintErrorWithModelMethods2() { + callSinkMethodModelMethods(InferTaint.inferSecretSource()); + } + + public void interprocTaintErrorWithModelMethods3() { + callSinkMethodModelMethods(returnTaintedSourceModelMethods()); + } + } diff --git a/infer/tests/endtoend/java/infer/TaintTest.java b/infer/tests/endtoend/java/infer/TaintTest.java index 19f53ad12..44fd5bc58 100644 --- a/infer/tests/endtoend/java/infer/TaintTest.java +++ b/infer/tests/endtoend/java/infer/TaintTest.java @@ -46,6 +46,10 @@ public class TaintTest { "callReadInputStreamCauseTaintError", "taintingShouldNotPreventInference1", "taintingShouldNotPreventInference2", + "simpleTaintErrorWithModelMethods", + "interprocTaintErrorWithModelMethods1", + "interprocTaintErrorWithModelMethods2", + "interprocTaintErrorWithModelMethods3" }; assertThat(