diff --git a/infer/models/java/builtins/com/facebook/infer/builtins/InferBuiltins.java b/infer/models/java/builtins/com/facebook/infer/builtins/InferBuiltins.java index 170e4243d..813f52eb5 100644 --- a/infer/models/java/builtins/com/facebook/infer/builtins/InferBuiltins.java +++ b/infer/models/java/builtins/com/facebook/infer/builtins/InferBuiltins.java @@ -40,11 +40,4 @@ public class InferBuiltins { public native static String __split_get_nth(String s, String sep, int n); - public native static void __set_taint_attribute(Object o, String taintKind); - - public native static void __set_untaint_attribute(Object o); - - // report an error if o is tainted, then assume UNTAINT(o) going forward - public native static void __check_untainted(Object o); - } diff --git a/infer/models/java/src/android/content/ContentValues.java b/infer/models/java/src/android/content/ContentValues.java deleted file mode 100644 index c72164d06..000000000 --- a/infer/models/java/src/android/content/ContentValues.java +++ /dev/null @@ -1,38 +0,0 @@ -/* - * 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 android.content; - -import com.facebook.infer.builtins.InferBuiltins; - -public class ContentValues { - - /** - * We want to treat this as a sink for both privacy and security purposes. - * - * Privacy: The purpose of ContentValues is to feed information into a ContentProvider, a core - * Android component that can expose data for other Android applications to query. Thus, you do - * not want secret information to flow into ContentValues because you don't want to give other - * apps an interface that lets them query your secret information. There's a possibility for false - * positives here because ContentProviders can control access to information via permissions, but - * in general it's just a bad idea to let secret info into a ContentProvider. - * - * Security: You don't want untrusted external content to flow into ContentValues because it may - * be used to store data in a ContentProvider, potentially giving an external app control over - * what goes into the database backing the ContentProvider/giving them direct access to make - * queries on your content provider (rather than exposing a small set of trusted queries, which is - * what should be done). This could have any number of security implications depending on how the - * ContentProvider is used. - **/ - public void put(String key, String value) { - InferBuiltins.__check_untainted(key); - InferBuiltins.__check_untainted(value); - } - -} diff --git a/infer/models/java/src/java/net/Socket.java b/infer/models/java/src/java/net/Socket.java index 4b64afd33..676a2a4ab 100644 --- a/infer/models/java/src/java/net/Socket.java +++ b/infer/models/java/src/java/net/Socket.java @@ -25,16 +25,13 @@ public class Socket { inputStream = new InputStream(); InferBuiltins.__set_file_attribute(inputStream); outputStream = new OutputStream(); - InferBuiltins.__set_file_attribute(outputStream); } public InputStream getInputStream() throws IOException { - InferBuiltins.__check_untainted(this); return inputStream; } public OutputStream getOutputStream() throws IOException { - InferBuiltins.__check_untainted(this); return outputStream; } diff --git a/infer/models/java/src/javax/net/SocketFactory.java b/infer/models/java/src/javax/net/SocketFactory.java deleted file mode 100644 index f1cc6c9c7..000000000 --- a/infer/models/java/src/javax/net/SocketFactory.java +++ /dev/null @@ -1,64 +0,0 @@ -/* - * 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. - */ - -package javax.net; - -import java.io.IOException; -import java.net.InetAddress; -import java.net.Socket; - -import com.facebook.infer.builtins.InferBuiltins; - -public class SocketFactory { - - // using recency abstraction to remember the last Socket created - private static Socket sLast; - - public static Socket getLastSocket() { - return sLast; - } - - // proxy for Socket of undefined type - private native Socket genSocket(); - - private Socket returnAllocatedSocket() { - Socket socket = genSocket(); - InferBuiltins.assume_allocated(socket); - sLast = socket; - return socket; - } - - public Socket createSocket() { - Socket socket = returnAllocatedSocket(); - InferBuiltins.__set_taint_attribute(socket, "UnverifiedSSLSocket"); - return socket; - } - - // the methods below are abstract methods in the actual Java class, but we need to implement it - // explicitly due to Infer's dynamic dispatch woes - public Socket createSocket(InetAddress addr, int i) throws IOException { - return this.createSocket(); - } - - public Socket createSocket(InetAddress addr1, int i, InetAddress addr2, int j) - throws IOException { - - return this.createSocket(); - } - - public Socket createSocket(String s, int i) throws IOException { - return this.createSocket(); - - } - - public Socket createSocket(String s, int i, InetAddress addr, int j) throws IOException { - return this.createSocket(); - } - -} diff --git a/infer/models/java/src/javax/net/ssl/HostnameVerifier.java b/infer/models/java/src/javax/net/ssl/HostnameVerifier.java deleted file mode 100644 index d85ce4816..000000000 --- a/infer/models/java/src/javax/net/ssl/HostnameVerifier.java +++ /dev/null @@ -1,38 +0,0 @@ -/* - * 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. - */ - -package javax.net.ssl; - -import java.net.Socket; -import javax.net.SocketFactory; -import javax.net.ssl.SSLSession; - -import com.facebook.infer.builtins.InferBuiltins; -import com.facebook.infer.builtins.InferUndefined; - -public class HostnameVerifier { - - public boolean verify( - String hostname, - SSLSession session) { - - Socket socket = SocketFactory.getLastSocket(); - - if (InferUndefined.boolean_undefined()) { - // verification succeeded; we can untaint the socket - InferBuiltins.__set_untaint_attribute(socket); - return true; - } else { - // verification failed; we can't untaint the socket - return false; - } - } - - -} diff --git a/infer/src/IR/BUILTINS.mli b/infer/src/IR/BUILTINS.mli index fa7e1b4b3..acb806382 100644 --- a/infer/src/IR/BUILTINS.mli +++ b/infer/src/IR/BUILTINS.mli @@ -26,8 +26,6 @@ module type S = sig val __cast : t (** [__cast(val,typ)] implements java's [typ(val)] *) - val __check_untainted : t - val __cxx_typeid : t val __delete : t @@ -99,14 +97,10 @@ module type S = sig val __set_observer_attribute : t - val __set_taint_attribute : t - val __set_unlocked_attribute : t val __set_unsubscribed_observer_attribute : t - val __set_untaint_attribute : t - val __set_wont_leak_attribute : t val __split_get_nth : t diff --git a/infer/src/IR/BuiltinDecl.ml b/infer/src/IR/BuiltinDecl.ml index 98b85c673..89046401e 100644 --- a/infer/src/IR/BuiltinDecl.ml +++ b/infer/src/IR/BuiltinDecl.ml @@ -42,8 +42,6 @@ let __builtin_va_start = create_procname "__builtin_va_start" let __cast = create_procname "__cast" -let __check_untainted = create_procname "__check_untainted" - let __cxx_typeid = create_procname "__cxx_typeid" let __delete = create_procname "__delete" @@ -115,14 +113,10 @@ let __set_mem_attribute = create_procname "__set_mem_attribute" let __set_observer_attribute = create_procname "__set_observer_attribute" -let __set_taint_attribute = create_procname "__set_taint_attribute" - let __set_unlocked_attribute = create_procname "__set_unlocked_attribute" let __set_unsubscribed_observer_attribute = create_procname "__set_unsubscribed_observer_attribute" -let __set_untaint_attribute = create_procname "__set_untaint_attribute" - let __set_wont_leak_attribute = create_procname "__set_wont_leak_attribute" let __split_get_nth = create_procname "__split_get_nth" diff --git a/infer/src/IR/Exceptions.ml b/infer/src/IR/Exceptions.ml index 3a23b521d..868e8b832 100644 --- a/infer/src/IR/Exceptions.ml +++ b/infer/src/IR/Exceptions.ml @@ -137,8 +137,6 @@ exception Stack_variable_address_escape of Localise.error_desc * L.ml_loc exception Symexec_memory_error of L.ml_loc -exception Tainted_value_reaching_sensitive_function of Localise.error_desc * L.ml_loc - exception Unary_minus_applied_to_unsigned_expression of Localise.error_desc * L.ml_loc exception Uninitialized_value of Localise.error_desc * L.ml_loc @@ -387,14 +385,6 @@ let recognize_exception exn = , Low , None , Nocat ) - | Tainted_value_reaching_sensitive_function (desc, ml_loc) - -> ( Localise.tainted_value_reaching_sensitive_function - , desc - , Some ml_loc - , Exn_user - , Medium - , Some Kerror - , Nocat ) | Unix.Unix_error (_, s1, s2) -> let desc = Localise.verbatim_desc (s1 ^ s2) in (Localise.from_string "Unix_error", desc, None, Exn_system, Low, None, Nocat) diff --git a/infer/src/IR/Exceptions.mli b/infer/src/IR/Exceptions.mli index 9ac55d2d7..1cc57d366 100644 --- a/infer/src/IR/Exceptions.mli +++ b/infer/src/IR/Exceptions.mli @@ -136,9 +136,6 @@ exception Skip_pointer_dereference of Localise.error_desc * Logging.ml_loc exception Stack_variable_address_escape of Localise.error_desc * Logging.ml_loc exception Symexec_memory_error of Logging.ml_loc - -exception Tainted_value_reaching_sensitive_function of Localise.error_desc * Logging.ml_loc - exception Unary_minus_applied_to_unsigned_expression of Localise.error_desc * Logging.ml_loc exception Uninitialized_value of Localise.error_desc * Logging.ml_loc diff --git a/infer/src/IR/Localise.ml b/infer/src/IR/Localise.ml index a93fb114b..a3bc43570 100644 --- a/infer/src/IR/Localise.ml +++ b/infer/src/IR/Localise.ml @@ -189,9 +189,6 @@ let stack_variable_address_escape = from_string "STACK_VARIABLE_ADDRESS_ESCAPE" let static_initialization_order_fiasco = from_string "STATIC_INITIALIZATION_ORDER_FIASCO" -let tainted_value_reaching_sensitive_function = - from_string "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION" - let thread_safety_violation = from_string "THREAD_SAFETY_VIOLATION" let unary_minus_applied_to_unsigned_expression = @@ -1122,41 +1119,6 @@ let desc_stack_variable_address_escape expr_str addr_dexp_str loc = in {no_desc with descriptions= [description]; tags= !tags} -let desc_tainted_value_reaching_sensitive_function taint_kind expr_str tainting_fun sensitive_fun - loc = - let tags = Tags.create () in - Tags.update tags Tags.value expr_str ; - let description = - match taint_kind with - | PredSymb.Tk_unverified_SSL_socket - -> F.asprintf - "The hostname of SSL socket %a (returned from %s) has not been verified! Reading from the socket via the call to %s %s is dangerous. You should verify the hostname of the socket using a HostnameVerifier before reading; otherwise, you may be vulnerable to a man-in-the-middle attack." - MF.pp_monospaced expr_str (format_method tainting_fun) (format_method sensitive_fun) - (at_line tags loc) - | PredSymb.Tk_shared_preferences_data - -> F.asprintf - "%a holds sensitive data read from a SharedPreferences object (via call to %s). This data may leak via the call to %s %s." - MF.pp_monospaced expr_str (format_method tainting_fun) (format_method sensitive_fun) - (at_line tags loc) - | PredSymb.Tk_privacy_annotation - -> F.asprintf - "%a holds privacy-sensitive data (source: call to %s). This data may leak via the call to %s %s." - MF.pp_monospaced expr_str (format_method tainting_fun) (format_method sensitive_fun) - (at_line tags loc) - | PredSymb.Tk_integrity_annotation - -> F.asprintf - "%a holds untrusted user-controlled data (source: call to %s). This data may flow into a security-sensitive sink via the call to %s %s." - MF.pp_monospaced expr_str (format_method tainting_fun) (format_method sensitive_fun) - (at_line tags loc) - | PredSymb.Tk_unknown - -> F.asprintf - "Value %a could be insecure (tainted) due to call to function %s %s %s %s. Function %s %s" - MF.pp_monospaced expr_str (format_method tainting_fun) - "and is reaching sensitive function" (format_method sensitive_fun) (at_line tags loc) - (format_method sensitive_fun) "requires its input to be verified or sanitized." - in - {no_desc with descriptions= [description]; tags= !tags} - let desc_uninitialized_dangling_pointer_deref deref expr_str loc = let tags = Tags.create () in Tags.update tags Tags.value expr_str ; diff --git a/infer/src/IR/Localise.mli b/infer/src/IR/Localise.mli index 069a1b32c..36060f3e9 100644 --- a/infer/src/IR/Localise.mli +++ b/infer/src/IR/Localise.mli @@ -162,9 +162,6 @@ val skip_pointer_dereference : t val stack_variable_address_escape : t val static_initialization_order_fiasco : t - -val tainted_value_reaching_sensitive_function : t - val thread_safety_violation : t val unary_minus_applied_to_unsigned_expression : t @@ -388,7 +385,4 @@ val desc_unary_minus_applied_to_unsigned_expression : val desc_unsafe_guarded_by_access : Typ.Fieldname.t -> string -> Location.t -> error_desc -val desc_tainted_value_reaching_sensitive_function : - PredSymb.taint_kind -> string -> Typ.Procname.t -> Typ.Procname.t -> Location.t -> error_desc - val desc_uninitialized_dangling_pointer_deref : deref_str -> string -> Location.t -> error_desc diff --git a/infer/src/IR/PredSymb.ml b/infer/src/IR/PredSymb.ml index efcd84b70..ee43a53fe 100644 --- a/infer/src/IR/PredSymb.ml +++ b/infer/src/IR/PredSymb.ml @@ -60,16 +60,6 @@ type path_pos = Typ.Procname.t * int [@@deriving compare] let equal_path_pos = [%compare.equal : path_pos] -type taint_kind = - | Tk_unverified_SSL_socket - | Tk_shared_preferences_data - | Tk_privacy_annotation - | Tk_integrity_annotation - | Tk_unknown - [@@deriving compare] - -type taint_info = {taint_source: Typ.Procname.t; taint_kind: taint_kind} [@@deriving compare] - (** acquire/release action on a resource *) type res_action = { ra_kind: res_act_kind (** kind of action *) @@ -108,9 +98,6 @@ type t = | Aautorelease | Adangling of dangling_kind (** dangling pointer *) | Aundef of Typ.Procname.t * _annot_item * _location * _path_pos - (** undefined value obtained by calling the given procedure, plus its return value annots *) - | Ataint of taint_info - | Auntaint of taint_info | Alocked | Aunlocked | Adiv0 of path_pos (** value appeared in second argument of division at given path position *) @@ -152,7 +139,6 @@ let mem_dealloc_pname = function type category = | ACresource | ACautorelease - | ACtaint | AClock | ACdiv0 | ACobjc_null @@ -168,8 +154,6 @@ let to_category att = match att with | Aresource _ | Adangling _ -> ACresource - | Ataint _ | Auntaint _ - -> ACtaint | Alocked | Aunlocked -> AClock | Aautorelease @@ -242,10 +226,6 @@ let to_string pe = function | Aundef (pn, _, loc, _) -> "UND" ^ Binop.str pe Lt ^ Typ.Procname.to_string pn ^ Binop.str pe Gt ^ ":" ^ string_of_int loc.Location.line - | Ataint {taint_source} - -> "TAINTED[" ^ Typ.Procname.to_string taint_source ^ "]" - | Auntaint _ - -> "UNTAINTED" | Alocked -> "LOCKED" | Aunlocked diff --git a/infer/src/IR/PredSymb.mli b/infer/src/IR/PredSymb.mli index 8f0128b42..a60e83102 100644 --- a/infer/src/IR/PredSymb.mli +++ b/infer/src/IR/PredSymb.mli @@ -53,15 +53,6 @@ type path_pos = Typ.Procname.t * int [@@deriving compare] val equal_path_pos : path_pos -> path_pos -> bool -type taint_kind = - | Tk_unverified_SSL_socket - | Tk_shared_preferences_data - | Tk_privacy_annotation - | Tk_integrity_annotation - | Tk_unknown - -type taint_info = {taint_source: Typ.Procname.t; taint_kind: taint_kind} - (** acquire/release action on a resource *) type res_action = { ra_kind: res_act_kind (** kind of action *) @@ -83,9 +74,6 @@ type t = | Aautorelease | Adangling of dangling_kind (** dangling pointer *) | Aundef of Typ.Procname.t * Annot.Item.t * Location.t * path_pos - (** undefined value obtained by calling the given procedure, plus its return value annots *) - | Ataint of taint_info - | Auntaint of taint_info | Alocked | Aunlocked | Adiv0 of path_pos (** value appeared in second argument of division at given path position *) @@ -111,7 +99,6 @@ val mem_dealloc_pname : mem_kind -> Typ.Procname.t type category = | ACresource | ACautorelease - | ACtaint | AClock | ACdiv0 | ACobjc_null diff --git a/infer/src/absint/PatternMatch.ml b/infer/src/absint/PatternMatch.ml index cd8587041..01e88976c 100644 --- a/infer/src/absint/PatternMatch.ml +++ b/infer/src/absint/PatternMatch.ml @@ -14,15 +14,6 @@ open! IStd module L = Logging module F = Format -type taint_spec = - { classname: string - ; method_name: string - ; ret_type: string - ; params: string list - ; is_static: bool - ; taint_kind: PredSymb.taint_kind - ; language: Config.language } - let type_is_object typ = match typ.Typ.desc with | Tptr ({desc= Tstruct name}, _) diff --git a/infer/src/absint/PatternMatch.mli b/infer/src/absint/PatternMatch.mli index 39747500f..8488e83cc 100644 --- a/infer/src/absint/PatternMatch.mli +++ b/infer/src/absint/PatternMatch.mli @@ -11,15 +11,6 @@ open! IStd (** Module for Pattern matching. *) -type taint_spec = - { classname: string - ; method_name: string - ; ret_type: string - ; params: string list - ; is_static: bool - ; taint_kind: PredSymb.taint_kind - ; language: Config.language } - val get_java_field_access_signature : Sil.instr -> (string * string * string) option (** Returns the signature of a field access (class name, field name, field type name) *) diff --git a/infer/src/backend/Attribute.ml b/infer/src/backend/Attribute.ml index 12fc44479..3a81df1f8 100644 --- a/infer/src/backend/Attribute.ml +++ b/infer/src/backend/Attribute.ml @@ -95,8 +95,6 @@ let get_undef tenv prop exp = get tenv prop exp ACundef let get_resource tenv prop exp = get tenv prop exp ACresource -let get_taint tenv prop exp = get tenv prop exp ACtaint - let get_autorelease tenv prop exp = get tenv prop exp ACautorelease let get_objc_null tenv prop exp = get tenv prop exp ACobjc_null diff --git a/infer/src/backend/Attribute.mli b/infer/src/backend/Attribute.mli index 5bb9f8abf..7ba3933f1 100644 --- a/infer/src/backend/Attribute.mli +++ b/infer/src/backend/Attribute.mli @@ -59,9 +59,6 @@ val get_resource : Tenv.t -> 'a Prop.t -> Exp.t -> Sil.atom option val get_retval : Tenv.t -> 'a Prop.t -> Exp.t -> Sil.atom option (** Get the retval null attribute associated to the expression, if any *) -val get_taint : Tenv.t -> 'a Prop.t -> Exp.t -> Sil.atom option -(** Get the taint attribute associated to the expression, if any *) - val get_undef : Tenv.t -> 'a Prop.t -> Exp.t -> Sil.atom option (** Get the undef attribute associated to the expression, if any *) diff --git a/infer/src/backend/BuiltinDefn.ml b/infer/src/backend/BuiltinDefn.ml index 73075589f..8381a3c9b 100644 --- a/infer/src/backend/BuiltinDefn.ml +++ b/infer/src/backend/BuiltinDefn.ml @@ -392,17 +392,6 @@ let execute___set_mem_attribute {Builtin.tenv; pdesc; prop_; path; ret_id; args; | _ -> raise (Exceptions.Wrong_argument_number __POS__) -(** report an error if [lexp] is tainted; otherwise, add untained([lexp]) as a precondition *) -let execute___check_untainted - {Builtin.tenv; pdesc; prop_; path; ret_id; args; proc_name= callee_pname} : Builtin.ret_typ = - match (args, ret_id) with - | [(lexp, _)], _ - -> let caller_pname = Procdesc.get_proc_name pdesc in - let n_lexp, prop = check_arith_norm_exp tenv caller_pname lexp prop_ in - [(check_untainted tenv n_lexp PredSymb.Tk_unknown caller_pname callee_pname prop, path)] - | _ - -> raise (Exceptions.Wrong_argument_number __POS__) - (** take a pointer to a struct, and return the value of a hidden field in the struct *) let execute___get_hidden_field {Builtin.tenv; pdesc; prop_; path; ret_id; args} : Builtin.ret_typ = match args with @@ -640,38 +629,6 @@ let execute___set_unlocked_attribute ({Builtin.pdesc; loc} as builtin_args) : Bu let execute___set_wont_leak_attribute builtin_args : Builtin.ret_typ = execute___set_attr PredSymb.Awont_leak builtin_args -(** Set the attibute of the value as tainted *) -let execute___set_taint_attribute {Builtin.tenv; pdesc; args; prop_; path} : Builtin.ret_typ = - match args with - | [(exp, _); (Exp.Const Const.Cstr taint_kind_str, _)] - -> let taint_source = Procdesc.get_proc_name pdesc in - let taint_kind = - match taint_kind_str with - | "UnverifiedSSLSocket" - -> PredSymb.Tk_unverified_SSL_socket - | "SharedPreferenceData" - -> PredSymb.Tk_shared_preferences_data - | other_str - -> failwith ("Unrecognized taint kind " ^ other_str) - in - set_attr tenv pdesc prop_ path exp - (PredSymb.Ataint {PredSymb.taint_source= taint_source; taint_kind}) - | _ - -> (* note: we can also get this if [taint_kind] is not a string literal *) - raise (Exceptions.Wrong_argument_number __POS__) - -(** Set the attibute of the value as tainted *) -let execute___set_untaint_attribute {Builtin.tenv; pdesc; args; prop_; path} : Builtin.ret_typ = - match args with - | [(exp, _)] - -> let taint_source = Procdesc.get_proc_name pdesc in - let taint_kind = PredSymb.Tk_unknown in - (* TODO: change builtin to specify taint kind *) - set_attr tenv pdesc prop_ path exp - (PredSymb.Auntaint {PredSymb.taint_source= taint_source; taint_kind}) - | _ - -> raise (Exceptions.Wrong_argument_number __POS__) - let execute___objc_cast {Builtin.tenv; pdesc; prop_; path; ret_id; args} : Builtin.ret_typ = match args with | [(val1_, _); (texp2_, _)] @@ -1086,9 +1043,6 @@ let __builtin_va_start = Builtin.register BuiltinDecl.__builtin_va_start execute (* [__cast(val,typ)] implements java's [typ(val)] *) let __cast = Builtin.register BuiltinDecl.__cast execute___cast -(* report a taint error if the parameter is tainted, and assume it is untainted afterward *) -let __check_untainted = Builtin.register BuiltinDecl.__check_untainted execute___check_untainted - let __cxx_typeid = Builtin.register BuiltinDecl.__cxx_typeid execute___cxx_typeid let __delete = Builtin.register BuiltinDecl.__delete (execute_free PredSymb.Mnew) @@ -1180,9 +1134,6 @@ let __set_mem_attribute = let __set_observer_attribute = Builtin.register BuiltinDecl.__set_observer_attribute (execute___set_attr PredSymb.Aobserver) -let __set_taint_attribute = - Builtin.register BuiltinDecl.__set_taint_attribute execute___set_taint_attribute - let __set_unlocked_attribute = Builtin.register BuiltinDecl.__set_unlocked_attribute execute___set_unlocked_attribute @@ -1190,9 +1141,6 @@ let __set_unsubscribed_observer_attribute = Builtin.register BuiltinDecl.__set_unsubscribed_observer_attribute (execute___set_attr PredSymb.Aunsubscribed_observer) -let __set_untaint_attribute = - Builtin.register BuiltinDecl.__set_untaint_attribute execute___set_untaint_attribute - let __set_wont_leak_attribute = Builtin.register BuiltinDecl.__set_wont_leak_attribute execute___set_wont_leak_attribute diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml index 00d96c4ff..db71effb5 100644 --- a/infer/src/backend/errdesc.ml +++ b/infer/src/backend/errdesc.ml @@ -1137,24 +1137,6 @@ let explain_return_expression_required loc typ = (** Explain retain cycle value error *) let explain_retain_cycle cycle loc dotty_str = Localise.desc_retain_cycle cycle loc dotty_str -(** Explain a tainted value error *) -let explain_tainted_value_reaching_sensitive_function prop e {PredSymb.taint_source; taint_kind} - sensitive_fun loc = - let var_desc = - match e with - | Exp.Lvar pv - -> Pvar.to_string pv - | _ -> - match find_with_exp prop e with - | Some (pvar, pvar_off) - -> let dexp = dexp_apply_pvar_off (DExp.Dpvar pvar) pvar_off in - DExp.to_string dexp - | None - -> Exp.to_string e - in - Localise.desc_tainted_value_reaching_sensitive_function taint_kind var_desc taint_source - sensitive_fun loc - (** explain a return statement missing *) let explain_return_statement_missing loc = Localise.desc_return_statement_missing loc diff --git a/infer/src/backend/errdesc.mli b/infer/src/backend/errdesc.mli index 88c0dcd88..c27e9d375 100644 --- a/infer/src/backend/errdesc.mli +++ b/infer/src/backend/errdesc.mli @@ -113,11 +113,6 @@ val explain_unary_minus_applied_to_unsigned_expression : Tenv.t -> Exp.t -> Typ.t -> Procdesc.Node.t -> Location.t -> Localise.error_desc (** explain unary minus applied to unsigned expression *) -val explain_tainted_value_reaching_sensitive_function : - Prop.normal Prop.t -> Exp.t -> PredSymb.taint_info -> Typ.Procname.t -> Location.t - -> Localise.error_desc -(** Explain a tainted value error *) - val explain_leak : Tenv.t -> Sil.hpred -> 'a Prop.t -> PredSymb.t option -> string option -> Exceptions.visibility * Localise.error_desc diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 3cba8edd7..e0fce0a0a 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -478,20 +478,6 @@ let mark_visited summary node = stats.Specs.nodes_visited_fp <- IntSet.add (node_id :> int) stats.Specs.nodes_visited_fp else stats.Specs.nodes_visited_re <- IntSet.add (node_id :> int) stats.Specs.nodes_visited_re -let add_taint_attrs tenv proc_name proc_desc prop = - match Taint.tainted_params proc_name with - | [] - -> prop - | tainted_param_nums - -> let formal_params = Procdesc.get_formals proc_desc in - let formal_params' = List.map ~f:(fun (p, _) -> Pvar.mk p proc_name) formal_params in - Taint.get_params_to_taint tainted_param_nums formal_params' - |> List.fold - ~f:(fun prop_acc (param, taint_kind) -> - let attr = PredSymb.Ataint {taint_source= proc_name; taint_kind} in - Taint.add_tainting_attribute tenv attr param prop_acc) - ~init:prop - let forward_tabulate tenv pdesc wl = let pname = Procdesc.get_proc_name pdesc in let handle_exn_node curr_node exn = @@ -543,8 +529,7 @@ let forward_tabulate tenv pdesc wl = L.d_ln () ; L.d_ln () in - let do_prop curr_node handle_exn prop_ path cnt num_paths = - let prop = if Config.taint_analysis then add_taint_attrs tenv pname pdesc prop_ else prop_ in + let do_prop curr_node handle_exn prop path cnt num_paths = L.d_strln ("Processing prop " ^ string_of_int cnt ^ "/" ^ string_of_int num_paths) ; L.d_increase_indent 1 ; try diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index ced714079..3c8259d98 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -929,9 +929,6 @@ let add_constraints_on_retval tenv pdesc prop ret_exp ~has_nullable_annot typ ca else match typ.Typ.desc with Typ.Tptr _ -> Prop.conjoin_neq tenv exp Exp.zero prop | _ -> prop in - let add_tainted_post ret_exp callee_pname prop = - Attribute.add_or_replace tenv prop (Apred (Ataint callee_pname, [ret_exp])) - in if Config.angelic_execution && not (is_rec_call callee_pname) then (* introduce a fresh program variable to allow abduction on the return value *) let abduced_ret_pv = Pvar.mk_abduced_ret callee_pname callee_loc in @@ -946,34 +943,9 @@ let add_constraints_on_retval tenv pdesc prop ret_exp ~has_nullable_annot typ ca (* bind return id to the abduced value pointed to by the pvar we introduced *) bind_exp_to_abduced_val ret_exp abduced_ret_pv prop in - let prop'' = add_ret_non_null ret_exp typ prop' in - if Config.taint_analysis then - match Taint.returns_tainted callee_pname None with - | Some taint_kind - -> add_tainted_post ret_exp {taint_source= callee_pname; taint_kind} prop'' - | None - -> prop'' - else prop'' + add_ret_non_null ret_exp typ prop' else add_ret_non_null ret_exp typ prop -let add_taint prop lhs_id rhs_exp pname tenv = - let add_attribute_if_field_tainted prop fieldname struct_typ = - if Taint.has_taint_annotation fieldname struct_typ then - let taint_info = {PredSymb.taint_source= pname; taint_kind= Tk_unknown} in - Attribute.add_or_replace tenv prop (Apred (Ataint taint_info, [Exp.Var lhs_id])) - else prop - in - match rhs_exp with - | Exp.Lfield (_, fieldname, ({desc= Tstruct typname} | {desc= Tptr ({desc= Tstruct typname}, _)})) - -> ( - match Tenv.lookup tenv typname with - | Some struct_typ - -> add_attribute_if_field_tainted prop fieldname struct_typ - | None - -> prop ) - | _ - -> prop - let execute_load ?(report_deref_errors= true) pname pdesc tenv id rhs_exp typ loc prop_ = let execute_load_ pdesc tenv id loc acc_in iter = let iter_ren = Prop.prop_iter_make_id_primed tenv id iter in @@ -994,10 +966,7 @@ let execute_load ?(report_deref_errors= true) pname pdesc tenv id rhs_exp typ lo Attribute.add_or_replace tenv prop' (Apred (Adangling DAuninit, [Exp.Var id])) else prop' in - let prop''' = - if Config.taint_analysis then add_taint prop'' id rhs_exp pname tenv else prop'' - in - prop''' :: acc + prop'' :: acc in match pred_insts_op with | None @@ -1537,23 +1506,6 @@ and add_constraints_on_actuals_by_ref tenv prop actuals_by_ref callee_pname call in List.fold ~f:do_actual_by_ref ~init:prop non_const_actuals_by_ref -and check_untainted tenv exp taint_kind caller_pname callee_pname prop = - match Attribute.get_taint tenv prop exp with - | Some Apred (Ataint taint_info, _) - -> let err_desc = - Errdesc.explain_tainted_value_reaching_sensitive_function prop exp taint_info callee_pname - (State.get_loc ()) - in - let exn = Exceptions.Tainted_value_reaching_sensitive_function (err_desc, __POS__) in - Reporting.log_warning_deprecated caller_pname exn ; - Attribute.add_or_replace tenv prop (Apred (Auntaint taint_info, [exp])) - | _ - -> if !Config.footprint then - let taint_info = {PredSymb.taint_source= callee_pname; taint_kind} in - (* add untained(n_lexp) to the footprint *) - Attribute.add tenv ~footprint:true prop (Auntaint taint_info) [exp] - else prop - (** execute a call for an unknown or scan function *) and unknown_or_scan_call ~is_scan ret_type_option ret_annots {Builtin.tenv; pdesc; prop_= pre; path; ret_id; args; proc_name= callee_pname; loc; instr} = @@ -1578,25 +1530,6 @@ and unknown_or_scan_call ~is_scan ret_type_option ret_annots in List.fold ~f:do_exp ~init:prop filtered_args in - let add_tainted_pre prop actuals caller_pname callee_pname = - if Config.taint_analysis then - match Taint.accepts_sensitive_params callee_pname None with - | [] - -> prop - | param_nums - -> let check_taint_if_nums_match (prop_acc, param_num) (actual_exp, _actual_typ) = - let prop_acc' = - match List.find ~f:(fun (num, _) -> Int.equal num param_num) param_nums with - | Some (_, taint_kind) - -> check_untainted tenv actual_exp taint_kind caller_pname callee_pname prop_acc - | None - -> prop_acc - in - (prop_acc', param_num + 1) - in - List.fold ~f:check_taint_if_nums_match ~init:(prop, 0) actuals |> fst - else prop - in let should_abduce_param_value pname = let open Typ.Procname in match pname with @@ -1637,9 +1570,7 @@ and unknown_or_scan_call ~is_scan ret_type_option ret_annots | _ -> pre_1 in - let pre_3 = add_constraints_on_actuals_by_ref tenv pre_2 actuals_by_ref callee_pname loc in - let caller_pname = Procdesc.get_proc_name pdesc in - add_tainted_pre pre_3 args caller_pname callee_pname + add_constraints_on_actuals_by_ref tenv pre_2 actuals_by_ref callee_pname loc in if is_scan (* if scan function, don't mark anything with undef attributes *) then [(Tabulation.remove_constant_string_class tenv pre_final, path)] diff --git a/infer/src/backend/symExec.mli b/infer/src/backend/symExec.mli index 2974d16ad..08dea49a9 100644 --- a/infer/src/backend/symExec.mli +++ b/infer/src/backend/symExec.mli @@ -31,10 +31,6 @@ val unknown_or_scan_call : is_scan:bool -> Typ.t option -> Annot.Item.t -> Built val check_variadic_sentinel : ?fails_on_nil:bool -> int -> int * int -> Builtin.t -val check_untainted : - Tenv.t -> Exp.t -> PredSymb.taint_kind -> Typ.Procname.t -> Typ.Procname.t -> Prop.normal Prop.t - -> Prop.normal Prop.t - val check_arith_norm_exp : Tenv.t -> Typ.Procname.t -> Exp.t -> Prop.normal Prop.t -> Exp.t * Prop.normal Prop.t (** Check for arithmetic problems and normalize an expression. *) diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index e6e6478c3..5613c9b94 100644 --- a/infer/src/backend/tabulation.ml +++ b/infer/src/backend/tabulation.ml @@ -925,58 +925,6 @@ let combine tenv ret_id (posts: ('a Prop.t * Paths.Path.t) list) actual_pre path print_results tenv actual_pre (List.map ~f:fst results) ; Some results -(* Add Auntaint attribute to a callee_pname precondition *) -let mk_pre tenv pre formal_params callee_pname callee_attrs = - if Config.taint_analysis then - match Taint.accepts_sensitive_params callee_pname (Some callee_attrs) with - | [] - -> pre - | tainted_param_nums - -> Taint.get_params_to_taint tainted_param_nums formal_params - |> List.fold - ~f:(fun prop_acc (param, taint_kind) -> - let attr = PredSymb.Auntaint {taint_source= callee_pname; taint_kind} in - Taint.add_tainting_attribute tenv attr param prop_acc) - ~init:(Prop.normalize tenv pre) - |> Prop.expose - else pre - -let report_taint_error e taint_info callee_pname caller_pname calling_prop = - let err_desc = - Errdesc.explain_tainted_value_reaching_sensitive_function calling_prop e taint_info - callee_pname (State.get_loc ()) - in - let exn = Exceptions.Tainted_value_reaching_sensitive_function (err_desc, __POS__) in - Reporting.log_warning_deprecated caller_pname exn - -let check_taint_on_variadic_function tenv callee_pname caller_pname actual_params calling_prop = - let rec n_tail lst n = - (* return the tail of a list from element n *) - if Int.equal n 1 then lst else match lst with [] -> [] | _ :: lst' -> n_tail lst' (n - 1) - in - let tainted_params = Taint.accepts_sensitive_params callee_pname None in - match tainted_params with - | [(tp, _)] when tp < 0 - -> (* All actual params from abs(tp) should not be tainted. If we find one we give the warning *) - let tp_abs = abs tp in - L.d_strln - ( "Checking tainted actual parameters from parameter number " ^ string_of_int tp_abs - ^ " onwards." ) ; - let actual_params' = n_tail actual_params tp_abs in - L.d_str "Paramters to be checked: [ " ; - List.iter - ~f:(fun (e, _) -> - L.d_str (" " ^ Exp.to_string e ^ " ") ; - match Attribute.get_taint tenv calling_prop e with - | Some Apred (Ataint taint_info, _) - -> report_taint_error e taint_info callee_pname caller_pname calling_prop - | _ - -> ()) - actual_params' ; - L.d_strln " ]" - | _ - -> () - (** Construct the actual precondition: add to the current state a copy of the (callee's) formal parameters instantiated with the actual parameters. *) @@ -1008,60 +956,39 @@ let mk_actual_precondition tenv prop actual_params formal_params = let actual_pre = Prop.prop_sigma_star prop instantiated_formals in Prop.normalize tenv actual_pre -let mk_posts tenv ret_id prop callee_pname callee_attrs posts = - match ret_id with - | Some (ret_id, _) - -> let mk_getter_idempotent posts = - (* if we have seen a previous call to the same function, only use specs whose return value +let mk_posts tenv ret_id_opt prop callee_pname posts = + if is_none ret_id_opt then posts + else + 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 = + let last_call_ret_non_null = + List.exists + ~f:(function + | Sil.Apred (Aretval (pname, _), [exp]) when Typ.Procname.equal callee_pname pname + -> Prover.check_disequal tenv prop exp Exp.zero + | _ + -> false) + (Attribute.get_all prop) + in + if last_call_ret_non_null then + let returns_null prop = List.exists ~f:(function - | Sil.Apred (Aretval (pname, _), [exp]) when Typ.Procname.equal callee_pname pname - -> Prover.check_disequal tenv prop exp Exp.zero + | Sil.Hpointsto (Exp.Lvar pvar, Sil.Eexp (e, _), _) when Pvar.is_return pvar + -> Prover.check_equal tenv (Prop.normalize tenv prop) e Exp.zero | _ -> false) - (Attribute.get_all prop) + prop.Prop.sigma in - if last_call_ret_non_null then - let returns_null prop = - List.exists - ~f:(function - | Sil.Hpointsto (Exp.Lvar pvar, Sil.Eexp (e, _), _) when Pvar.is_return pvar - -> Prover.check_equal tenv (Prop.normalize tenv prop) e Exp.zero - | _ - -> false) - prop.Prop.sigma - in - List.filter ~f:(fun (prop, _) -> not (returns_null prop)) posts - else posts - in - let mk_retval_tainted posts = - match Taint.returns_tainted callee_pname (Some callee_attrs) with - | Some taint_kind - -> let taint_retval (prop, path) = - let prop_normal = Prop.normalize tenv prop in - let prop' = - Attribute.add_or_replace tenv prop_normal - (Apred (Ataint {taint_source= callee_pname; taint_kind}, [Exp.Var ret_id])) - |> Prop.expose - in - (prop', path) - in - List.map ~f:taint_retval posts - | None - -> posts - in - let posts' = - if Config.idempotent_getters && Config.curr_language_is Config.Java then - mk_getter_idempotent posts - else posts - in - if Config.taint_analysis then mk_retval_tainted posts' else posts' - | _ - -> posts + List.filter ~f:(fun (prop, _) -> not (returns_null prop)) posts + else posts + in + if Config.idempotent_getters && Config.curr_language_is Config.Java then + mk_getter_idempotent posts + else posts (** Check if actual_pre * missing_footprint |- false *) let inconsistent_actualpre_missing tenv actual_pre split_opt = @@ -1073,69 +1000,6 @@ let inconsistent_actualpre_missing tenv actual_pre split_opt = | None -> false -(* perform the taint analysis check by comparing the taint atoms in [calling_pi] with the untaint - atoms required by the [missing_pi] computed during abduction *) -let do_taint_check tenv caller_pname callee_pname calling_prop missing_pi sub actual_params = - let calling_pi = calling_prop.Prop.pi in - (* get a version of [missing_pi] whose var names match the names in calling pi *) - let missing_pi_sub = Prop.pi_sub (`Exp sub) missing_pi in - let combined_pi = calling_pi @ missing_pi_sub in - (* build a map from exp -> [taint attrs, untaint attrs], keeping only exprs with both kinds of - attrs (we will flag errors on those exprs) *) - let collect_taint_untaint_exprs acc_map (atom: Sil.atom) = - match atom with - | Apred (Ataint _, [e]) - -> let taint_atoms, untaint_atoms = - try Exp.Map.find e acc_map - with Not_found -> ([], []) - in - Exp.Map.add e (atom :: taint_atoms, untaint_atoms) acc_map - | Apred (Auntaint _, [e]) - -> let taint_atoms, untaint_atoms = - try Exp.Map.find e acc_map - with Not_found -> ([], []) - in - Exp.Map.add e (taint_atoms, atom :: untaint_atoms) acc_map - | _ - -> acc_map - in - let taint_untaint_exp_map = - List.fold ~f:collect_taint_untaint_exprs ~init:Exp.Map.empty combined_pi - |> Exp.Map.filter (fun _ (taint, untaint) -> taint <> [] && untaint <> []) - in - (* TODO: in the future, we will have a richer taint domain that will require making sure that the - "kind" (e.g. security, privacy) of the taint and untaint match, but for now we don't look at - the untaint atoms *) - let report_taint_errors e (taint_atoms, _untaint_atoms) = - let report_one_error (taint_atom: Sil.atom) = - let taint_info = - match taint_atom with - | Apred (Ataint taint_info, _) - -> taint_info - | _ - -> failwith "Expected to get taint attr on atom" - in - report_taint_error e taint_info callee_pname caller_pname calling_prop - in - List.iter ~f:report_one_error taint_atoms - in - Exp.Map.iter report_taint_errors taint_untaint_exp_map ; - (* filter out UNTAINT(e) atoms from [missing_pi] such that we have already reported a taint - error on e. without doing this, we will get PRECONDITION_NOT_MET (and failed spec - inference), which is bad. instead, what this does is effectively assume that the UNTAINT(e) - precondition was met, and continue with the analysis under this assumption. this makes sense - because we are reporting the taint error, but propagating a *safe* postcondition w.r.t to - tainting. *) - let not_untaint_atom atom = - not - (Exp.Map.exists - (fun _ (_, untaint_atoms) -> - List.exists ~f:(fun a -> Sil.equal_atom atom a) untaint_atoms) - taint_untaint_exp_map) - in - check_taint_on_variadic_function tenv callee_pname caller_pname actual_params calling_prop ; - List.filter ~f:not_untaint_atom missing_pi_sub - let class_cast_exn tenv pname_opt texp1 texp2 exp ml_loc = let desc = Errdesc.explain_class_cast_exception tenv pname_opt texp1 texp2 exp (State.get_node ()) @@ -1165,14 +1029,12 @@ let check_uninitialize_dangling_deref tenv callee_pname actual_pre sub formal_pa props (** Perform symbolic execution for a single spec *) -let exe_spec tenv ret_id (n, nspecs) caller_pdesc callee_pname callee_attrs loc prop path_pre +let exe_spec tenv ret_id_opt (n, nspecs) caller_pdesc callee_pname loc prop path_pre (spec: Prop.exposed Specs.spec) actual_params formal_params : abduction_res = let caller_pname = Procdesc.get_proc_name caller_pdesc in - let posts = mk_posts tenv ret_id prop callee_pname callee_attrs spec.Specs.posts in + let posts = mk_posts tenv ret_id_opt prop callee_pname spec.Specs.posts in let actual_pre = mk_actual_precondition tenv prop actual_params formal_params in - let spec_pre = - mk_pre tenv (Specs.Jprop.to_prop spec.Specs.pre) formal_params callee_pname callee_attrs - in + let spec_pre = Specs.Jprop.to_prop spec.Specs.pre in L.d_strln ("EXECUTING SPEC " ^ string_of_int n ^ "/" ^ string_of_int nspecs) ; L.d_strln "ACTUAL PRECONDITION =" ; L.d_increase_indent 1 ; @@ -1205,17 +1067,12 @@ let exe_spec tenv ret_id (n, nspecs) caller_pdesc callee_pname callee_attrs loc Reporting.log_warning_deprecated caller_pname exn in let do_split () = - let missing_pi' = - if Config.taint_analysis then - do_taint_check tenv caller_pname callee_pname actual_pre missing_pi sub2 actual_params - else missing_pi - in - process_splitting actual_pre sub1 sub2 frame missing_pi' missing_sigma frame_fld - missing_fld frame_typ missing_typ + process_splitting actual_pre sub1 sub2 frame missing_pi missing_sigma frame_fld missing_fld + frame_typ missing_typ in let report_valid_res split = match - combine tenv ret_id posts actual_pre path_pre split caller_pdesc callee_pname loc + combine tenv ret_id_opt posts actual_pre path_pre split caller_pdesc callee_pname loc with | None -> Invalid_res Cannot_combine @@ -1474,8 +1331,8 @@ let exe_call_postprocess tenv ret_id trace_call callee_pname callee_attrs loc re -> res (** Execute the function call and return the list of results with return value *) -let exe_function_call callee_summary tenv ret_id caller_pdesc callee_pname loc actual_params prop - path = +let exe_function_call callee_summary tenv ret_id_opt caller_pdesc callee_pname loc actual_params + prop path = let callee_attrs = Specs.get_attributes callee_summary in let caller_pname = Procdesc.get_proc_name caller_pdesc in let caller_summary = Specs.get_summary_unsafe "exe_function_call" caller_pname in @@ -1491,8 +1348,8 @@ let exe_function_call callee_summary tenv ret_id caller_pdesc callee_pname loc a Prop.d_prop prop ; L.d_ln () ; let exe_one_spec (n, spec) = - exe_spec tenv ret_id (n, nspecs) caller_pdesc callee_pname callee_attrs loc prop path spec - actual_params formal_params + exe_spec tenv ret_id_opt (n, nspecs) caller_pdesc callee_pname loc prop path spec actual_params + formal_params in let results = List.map ~f:exe_one_spec spec_list in - exe_call_postprocess tenv ret_id trace_call callee_pname callee_attrs loc results + exe_call_postprocess tenv ret_id_opt trace_call callee_pname callee_attrs loc results diff --git a/infer/src/backend/taint.ml b/infer/src/backend/taint.ml deleted file mode 100644 index 17052af52..000000000 --- a/infer/src/backend/taint.ml +++ /dev/null @@ -1,365 +0,0 @@ -(* - * 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. - *) - -open! IStd -module L = Logging -open PatternMatch - -(* list of sources that return a tainted value *) -let sources0 = - [ (* for testing only *) - { classname= "com.facebook.infer.builtins.InferTaint" - ; method_name= "inferSecretSource" - ; ret_type= "java.lang.Object" - ; params= [] - ; is_static= true - ; taint_kind= Tk_unknown - ; language= Config.Java } - ; { classname= "com.facebook.infer.builtins.InferTaint" - ; method_name= "inferSecretSourceUndefined" - ; ret_type= "java.lang.Object" - ; params= [] - ; is_static= true - ; taint_kind= Tk_unknown - ; language= Config.Java } - ; (* actual specs *) - { classname= "android.content.SharedPreferences" - ; method_name= "getString" - ; ret_type= "java.lang.String" - ; params= ["java.lang.String"; "java.lang.String"] - ; is_static= false - ; taint_kind= Tk_shared_preferences_data - ; language= Config.Java } - ; (* === iOS === *) - { classname= "NSHTTPCookie" - ; method_name= "value" - ; ret_type= "NSString *" - ; params= [] - ; is_static= false - ; taint_kind= Tk_privacy_annotation - ; language= Config.Clang } ] - @ FbTaint.sources - -(* list of (sensitive sinks, zero-indexed numbers of parameters that should not be tainted). note: - index 0 means "the first non-this/self argument"; we currently don't have a way to say "this/self - should not be tainted" with this form of specification *) -let sinks = - (* it's instance method *) - [ (* for testing only *) - ( { classname= "com.facebook.infer.builtins.InferTaint" - ; method_name= "inferSensitiveSink" - ; ret_type= "void" - ; params= ["java.lang.Object"] - ; is_static= true - ; taint_kind= Tk_unknown - ; language= Config.Java } - , [0] ) - ; ( { classname= "com.facebook.infer.builtins.InferTaint" - ; method_name= "inferSensitiveSinkUndefined" - ; ret_type= "void" - ; params= ["java.lang.Object"] - ; is_static= true - ; taint_kind= Tk_unknown - ; language= Config.Java } - , [0] ) - ; (* actual specs *) - ( { classname= "android.util.Log" - ; method_name= "d" - ; ret_type= "int" - ; params= ["java.lang.String"; "java.lang.String"] - ; is_static= true - ; taint_kind= Tk_privacy_annotation - ; language= Config.Java } - , [0; 1] ) - ; ( { classname= "android.content.ContentResolver" - ; method_name= "openInputStream" - ; ret_type= "java.io.InputStream" - ; params= ["android.net.Uri"] - ; is_static= false - ; taint_kind= Tk_privacy_annotation - ; language= Config.Java } - , [1] ) - ; ( { classname= "android.content.ContentResolver" - ; method_name= "openOutputStream" - ; ret_type= "java.io.OutputStream" - ; params= ["android.net.Uri"] - ; is_static= false - ; taint_kind= Tk_privacy_annotation - ; language= Config.Java } - , [0] ) - ; ( { classname= "android.content.ContentResolver" - ; method_name= "openOutputStream" - ; ret_type= "java.io.OutputStream" - ; params= ["android.net.Uri"; "java.lang.String"] - ; is_static= false - ; taint_kind= Tk_privacy_annotation - ; language= Config.Java } - , [0] ) - ; ( { classname= "android.content.ContentResolver" - ; method_name= "openAssetFileDescriptor" - ; ret_type= "android.content.res.AssetFileDescriptor" - ; params= ["android.net.Uri"; "java.lang.String"] - ; is_static= false - ; taint_kind= Tk_privacy_annotation - ; language= Config.Java } - , [0] ) - ; ( { classname= "android.content.ContentResolver" - ; method_name= "openAssetFileDescriptor" - ; ret_type= "android.content.res.AssetFileDescriptor" - ; params= ["android.net.Uri"; "java.lang.String"; "android.os.CancellationSignal"] - ; is_static= false - ; taint_kind= Tk_privacy_annotation - ; language= Config.Java } - , [0] ) - ; ( { classname= "android.content.ContentResolver" - ; method_name= "openFileDescriptor" - ; ret_type= "android.os.ParcelFileDescriptor" - ; params= ["android.net.Uri"; "java.lang.String"; "android.os.CancellationSignal"] - ; is_static= false - ; taint_kind= Tk_privacy_annotation - ; language= Config.Java } - , [0] ) - ; ( { classname= "android.content.ContentResolver" - ; method_name= "openFileDescriptor" - ; ret_type= "android.os.ParcelFileDescriptor" - ; params= ["android.net.Uri"; "java.lang.String"] - ; is_static= false - ; taint_kind= Tk_privacy_annotation - ; language= Config.Java } - , [0] ) - ; ( { classname= "android.content.ContentResolver" - ; method_name= "openTypedAssetFileDescriptor" - ; ret_type= "android.content.res.AssetFileDescriptor" - ; params= - [ "android.net.Uri" - ; "java.lang.String" - ; "android.os.Bundle" - ; "android.os.CancellationSignal" ] - ; is_static= false - ; taint_kind= Tk_privacy_annotation - ; language= Config.Java } - , [0] ) - ; ( { classname= "android.content.ContentResolver" - ; method_name= "openTypedAssetFileDescriptor" - ; ret_type= "android.content.res.AssetFileDescriptor" - ; params= ["android.net.Uri"; "java.lang.String"; "android.os.Bundle"] - ; is_static= false - ; taint_kind= Tk_privacy_annotation - ; language= Config.Java } - , [0] ) - ; (* === iOS === *) - ( { classname= "NSString" - ; method_name= "stringWithFormat:" - ; ret_type= "instancetype" - ; params= [] - ; is_static= true - ; taint_kind= Tk_unknown - ; language= Config.Clang } - , [-2] ) - ; ( { classname= "NSString" - ; method_name= "stringWithUTF8String:" - ; ret_type= "instancetype" - ; params= [] - ; is_static= true - ; taint_kind= Tk_unknown - ; language= Config.Clang } - , [-2] ) - ; ( { classname= "NSString" - ; method_name= "localizedStringWithFormat:" - ; ret_type= "instancetype" - ; params= [] - ; is_static= true - ; taint_kind= Tk_unknown - ; language= Config.Clang } - , [-2] ) - ; ( { classname= "NSString" - ; method_name= "initWithFormat:" - ; ret_type= "instancetype" - ; params= [] - ; is_static= false - ; taint_kind= Tk_unknown - ; language= Config.Clang } - , [-2] ) - ; ( { classname= "NSString" - ; method_name= "stringWithString:" - ; ret_type= "instancetype" - ; params= [] - ; is_static= true - ; taint_kind= Tk_unknown - ; language= Config.Clang } - , [0] ) - ; (* ==== iOS for testing only ==== *) - ( { classname= "ExampleViewController" - ; method_name= "loadURL:trackingCodes:" - ; ret_type= "void" - ; params= [] - ; is_static= false - ; taint_kind= Tk_unknown - ; language= Config.Clang } - , [1] ) ] - @ FbTaint.sinks - -let functions_with_tainted_params = - [ (* ==== iOS for testing only ==== *) - ( { classname= "ExampleDelegate" - ; method_name= "application:openURL:sourceApplication:annotation:" - ; ret_type= "BOOL" - ; params= [] - ; is_static= false - ; (* it's instance method *) - taint_kind= Tk_unknown - ; language= Config.Clang } - , [2] ) - ; (* actual specs *) - ( { (* This method is a source in iOS as it get as parameter - a non trusted URL (openURL). The method the passes - it around and this URL may arrive unsanitized to - loadURL:trackingCodes: of FBWebViewController - which uses the URL. *) - classname= "AppDelegate" - ; method_name= "application:openURL:sourceApplication:annotation:" - ; ret_type= "BOOL" - ; params= [] - ; is_static= false - ; (* it's instance method *) - taint_kind= Tk_integrity_annotation - ; language= Config.Clang } - , [2] ) ] - @ FbTaint.functions_with_tainted_params - -(* turn string specificiation of Java method into a procname *) -let java_method_to_procname java_method = - Typ.Procname.Java - (Typ.Procname.java (Typ.Name.Java.from_string java_method.classname) - (Some (Typ.Procname.split_classname java_method.ret_type)) java_method.method_name - (List.map ~f:Typ.Procname.split_classname java_method.params) - (if java_method.is_static then Typ.Procname.Static else Typ.Procname.Non_Static)) - -(* turn string specificiation of an objc method into a procname *) -let objc_method_to_procname objc_method = - let method_kind = Typ.Procname.objc_method_kind_of_bool (not objc_method.is_static) in - let typename = Typ.Name.Objc.from_string objc_method.classname in - Typ.Procname.ObjC_Cpp - (Typ.Procname.objc_cpp typename objc_method.method_name method_kind Typ.NoTemplate - ~is_generic_model:false) - -let taint_spec_to_taint_info taint_spec = - let taint_source = - match taint_spec.language with - | Config.Clang - -> objc_method_to_procname taint_spec - | Config.Java - -> java_method_to_procname taint_spec - in - {PredSymb.taint_source= taint_source; taint_kind= taint_spec.taint_kind} - -let sources = List.map ~f:taint_spec_to_taint_info sources0 - -let mk_pname_param_num methods = - List.map ~f:(fun (mname, param_num) -> (taint_spec_to_taint_info mname, param_num)) methods - -let taint_sinks = mk_pname_param_num sinks - -let func_with_tainted_params = mk_pname_param_num functions_with_tainted_params - -let attrs_opt_get_annots = function - | Some attrs - -> attrs.ProcAttributes.method_annotation - | None - -> Annot.Method.empty - -(* TODO: return a taint kind *) - -(** returns true if [callee_pname] returns a tainted value *) -let returns_tainted callee_pname callee_attrs_opt = - let procname_matches taint_info = - Typ.Procname.equal taint_info.PredSymb.taint_source callee_pname - in - match List.find ~f:procname_matches sources with - | Some taint_info - -> Some taint_info.PredSymb.taint_kind - | None - -> let ret_annot, _ = attrs_opt_get_annots callee_attrs_opt in - if Annotations.ia_is_integrity_source ret_annot then Some PredSymb.Tk_integrity_annotation - else if Annotations.ia_is_privacy_source ret_annot then Some PredSymb.Tk_privacy_annotation - else None - -let find_callee taint_infos callee_pname = - List.find - ~f:(fun (taint_info, _) -> Typ.Procname.equal taint_info.PredSymb.taint_source callee_pname) - taint_infos - -(** returns list of zero-indexed argument numbers of [callee_pname] that may be tainted *) -let accepts_sensitive_params callee_pname callee_attrs_opt = - match find_callee taint_sinks callee_pname with - | None - -> let _, param_annots = attrs_opt_get_annots callee_attrs_opt in - let offset = if Typ.Procname.java_is_static callee_pname then 0 else 1 in - let indices_and_annots = - List.mapi ~f:(fun param_num attr -> (param_num + offset, attr)) param_annots - in - let tag_tainted_indices acc (index, attr) = - if Annotations.ia_is_integrity_sink attr then (index, PredSymb.Tk_privacy_annotation) - :: acc - else if Annotations.ia_is_privacy_sink attr then (index, PredSymb.Tk_privacy_annotation) - :: acc - else acc - in - List.fold ~f:tag_tainted_indices ~init:[] indices_and_annots - | Some (taint_info, tainted_param_indices) - -> List.map - ~f:(fun param_num -> (param_num, taint_info.PredSymb.taint_kind)) - tainted_param_indices - -(** returns list of zero-indexed parameter numbers of [callee_pname] that should be - considered tainted during symbolic execution *) -let tainted_params callee_pname = - match find_callee func_with_tainted_params callee_pname with - | Some (taint_info, tainted_param_indices) - -> List.map - ~f:(fun param_num -> (param_num, taint_info.PredSymb.taint_kind)) - tainted_param_indices - | None - -> [] - -let has_taint_annotation fieldname (struct_typ: Typ.Struct.t) = - let fld_has_taint_annot (fname, _, annot) = - Typ.Fieldname.equal fieldname fname - && (Annotations.ia_is_privacy_source annot || Annotations.ia_is_integrity_source annot) - in - List.exists ~f:fld_has_taint_annot struct_typ.fields - || List.exists ~f:fld_has_taint_annot struct_typ.statics - -(* add tainting attributes to a list of paramenters *) -let get_params_to_taint tainted_param_nums formal_params = - let get_taint_kind index = - List.find ~f:(fun (taint_index, _) -> Int.equal index taint_index) tainted_param_nums - in - let collect_params_to_taint params_to_taint_acc (index, param) = - match get_taint_kind index with - | Some (_, taint_kind) - -> (param, taint_kind) :: params_to_taint_acc - | None - -> params_to_taint_acc - in - let numbered_params = List.mapi ~f:(fun i param -> (i, param)) formal_params in - List.fold ~f:collect_params_to_taint ~init:[] numbered_params - -(* add tainting attribute to a pvar in a prop *) -let add_tainting_attribute tenv att pvar_param prop = - List.fold - ~f:(fun prop_acc hpred -> - match hpred with - | Sil.Hpointsto (Exp.Lvar pvar, Sil.Eexp (rhs, _), _) when Pvar.equal pvar pvar_param - -> L.d_strln - ("TAINT ANALYSIS: setting taint/untaint attribute of parameter " ^ Pvar.to_string pvar) ; - Attribute.add_or_replace tenv prop_acc (Apred (att, [rhs])) - | _ - -> prop_acc) - ~init:prop prop.Prop.sigma diff --git a/infer/src/backend/taint.mli b/infer/src/backend/taint.mli deleted file mode 100644 index 934e2efab..000000000 --- a/infer/src/backend/taint.mli +++ /dev/null @@ -1,30 +0,0 @@ -(* - * 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. - *) - -open! IStd - -val returns_tainted : Typ.Procname.t -> ProcAttributes.t option -> PredSymb.taint_kind option -(** returns true if [callee_pname] returns a tainted value *) - -val accepts_sensitive_params : - Typ.Procname.t -> ProcAttributes.t option -> (int * PredSymb.taint_kind) list -(** returns list of zero-indexed argument numbers of [callee_pname] that may be tainted *) - -val tainted_params : Typ.Procname.t -> (int * PredSymb.taint_kind) list -(** returns list of zero-indexed parameter numbers of [callee_pname] that should be - considered tainted during symbolic execution *) - -val has_taint_annotation : Typ.Fieldname.t -> Typ.Struct.t -> bool -(** returns the taint_kind of [fieldname] if it has a taint source annotation *) - -val add_tainting_attribute : - Tenv.t -> PredSymb.t -> Pvar.t -> Prop.normal Prop.t -> Prop.normal Prop.t - -val get_params_to_taint : - (int * PredSymb.taint_kind) list -> Pvar.t list -> (Pvar.t * PredSymb.taint_kind) list diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 12137cf96..b1e3cb106 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -234,9 +234,6 @@ let specs_files_suffix = ".specs" let start_filename = ".start" -(** If true performs taint analysis *) -let taint_analysis = true - (** Enable detailed tracing information during array abstraction *) let trace_absarray = false diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 7d6886585..2ee519922 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -216,9 +216,6 @@ val specs_dir_name : string val specs_files_suffix : string val start_filename : string - -val taint_analysis : bool - val trace_absarray : bool val undo_join : bool diff --git a/infer/src/opensource/fbTaint.ml b/infer/src/opensource/fbTaint.ml deleted file mode 100644 index 9ad6ea170..000000000 --- a/infer/src/opensource/fbTaint.ml +++ /dev/null @@ -1,16 +0,0 @@ -(* - * 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. - *) - -open! IStd - -let sources = [] - -let sinks = [] - -let functions_with_tainted_params = [] diff --git a/infer/src/opensource/fbTaint.mli b/infer/src/opensource/fbTaint.mli deleted file mode 100644 index f069bb5f7..000000000 --- a/infer/src/opensource/fbTaint.mli +++ /dev/null @@ -1,16 +0,0 @@ -(* - * 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. - *) - -open! IStd - -val sources : PatternMatch.taint_spec list - -val sinks : (PatternMatch.taint_spec * int list) list - -val functions_with_tainted_params : (PatternMatch.taint_spec * int list) list diff --git a/infer/tests/build_systems/ant/issues.exp b/infer/tests/build_systems/ant/issues.exp index 3f80c70a8..32fe6ad2a 100644 --- a/infer/tests/build_systems/ant/issues.exp +++ b/infer/tests/build_systems/ant/issues.exp @@ -172,30 +172,6 @@ codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.zipFileLeakExcep codetoanalyze/java/infer/SuppressLintExample.java, void SuppressAllWarnigsInTheClass.shouldNotReportNPE(), 2, NULL_DEREFERENCE, [start of procedure shouldNotReportNPE()] codetoanalyze/java/infer/SuppressLintExample.java, void SuppressAllWarnigsInTheClass.shouldNotReportResourceLeak(), 2, RESOURCE_LEAK, [start of procedure shouldNotReportResourceLeak()] codetoanalyze/java/infer/SuppressLintExample.java, void SuppressLintExample.shouldReportNPE(), 2, NULL_DEREFERENCE, [start of procedure shouldReportNPE()] -codetoanalyze/java/infer/TaintExample.java, InputStream TaintExample.socketIgnoreExceptionNoVerify(SSLSocketFactory), 9, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure socketIgnoreExceptionNoVerify(...),start of procedure throwExceptionIfNoVerify(...),Taking true branch,exception javax.net.ssl.SSLException,return from a call to void TaintExample.throwExceptionIfNoVerify(SSLSocket,String),Switch condition is true. Entering switch case] -codetoanalyze/java/infer/TaintExample.java, InputStream TaintExample.socketNotVerifiedSimple(SSLSocketFactory), 3, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure socketNotVerifiedSimple(...)] -codetoanalyze/java/infer/TaintExample.java, InputStream TaintExample.socketVerifiedForgotToCheckRetval(SSLSocketFactory,HostnameVerifier,SSLSession), 7, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure socketVerifiedForgotToCheckRetval(...)] -codetoanalyze/java/infer/TaintExample.java, InputStream TaintExample.taintingShouldNotPreventInference1(SSLSocketFactory), 4, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure taintingShouldNotPreventInference1(...),start of procedure socketNotVerifiedSimple(...),return from a call to InputStream TaintExample.socketNotVerifiedSimple(SSLSocketFactory),Skipped call: function or method not found] -codetoanalyze/java/infer/TaintExample.java, Socket TaintExample.callReadInputStreamCauseTaintError(SSLSocketFactory), 3, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure callReadInputStreamCauseTaintError(...)] -codetoanalyze/java/infer/TaintExample.java, void TaintExample.contentValuesPutWithTaintedString(ContentValues,SharedPreferences,String,String), 2, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure contentValuesPutWithTaintedString(...)] -codetoanalyze/java/infer/TaintExample.java, void TaintExample.interprocTaintErrorWithModelMethods1(), 1, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure interprocTaintErrorWithModelMethods1(),start of procedure returnTaintedSourceModelMethods(),return from a call to Object TaintExample.returnTaintedSourceModelMethods()] -codetoanalyze/java/infer/TaintExample.java, void TaintExample.interprocTaintErrorWithModelMethods2(), 1, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure interprocTaintErrorWithModelMethods2()] -codetoanalyze/java/infer/TaintExample.java, void TaintExample.interprocTaintErrorWithModelMethods3(), 1, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure interprocTaintErrorWithModelMethods3(),start of procedure returnTaintedSourceModelMethods(),return from a call to Object TaintExample.returnTaintedSourceModelMethods()] -codetoanalyze/java/infer/TaintExample.java, void TaintExample.interprocTaintErrorWithModelMethodsUndefined1(), 1, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure interprocTaintErrorWithModelMethodsUndefined1(),start of procedure returnTaintedSourceModelMethodsUndefined(),return from a call to Object TaintExample.returnTaintedSourceModelMethodsUndefined()] -codetoanalyze/java/infer/TaintExample.java, void TaintExample.interprocTaintErrorWithModelMethodsUndefined2(), 1, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure interprocTaintErrorWithModelMethodsUndefined2()] -codetoanalyze/java/infer/TaintExample.java, void TaintExample.interprocTaintErrorWithModelMethodsUndefined3(), 1, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure interprocTaintErrorWithModelMethodsUndefined3(),start of procedure returnTaintedSourceModelMethodsUndefined(),return from a call to Object TaintExample.returnTaintedSourceModelMethodsUndefined()] -codetoanalyze/java/infer/TaintExample.java, void TaintExample.simpleTaintErrorWithModelMethods(), 2, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure simpleTaintErrorWithModelMethods()] -codetoanalyze/java/infer/TaintExample.java, void TaintExample.simpleTaintErrorWithModelMethodsUndefined(), 2, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure simpleTaintErrorWithModelMethodsUndefined(),Skipped call: function or method not found] -codetoanalyze/java/infer/TaintExample.java, void TaintExample.testIntegritySinkAnnotReport(String), 1, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure testIntegritySinkAnnotReport(...),start of procedure integritySource(),return from a call to String TaintExample.integritySource()] -codetoanalyze/java/infer/TaintExample.java, void TaintExample.testIntegritySourceAnnot(), 1, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure testIntegritySourceAnnot(),start of procedure integritySource(),return from a call to String TaintExample.integritySource()] -codetoanalyze/java/infer/TaintExample.java, void TaintExample.testIntegritySourceInstanceFieldAnnot(), 2, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure testIntegritySourceInstanceFieldAnnot()] -codetoanalyze/java/infer/TaintExample.java, void TaintExample.testIntegritySourceStaticFieldAnnot(), 2, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure testIntegritySourceStaticFieldAnnot()] -codetoanalyze/java/infer/TaintExample.java, void TaintExample.testPrivacySinkAnnot1(), 2, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure testPrivacySinkAnnot1(),start of procedure privacySource(),return from a call to String TaintExample.privacySource()] -codetoanalyze/java/infer/TaintExample.java, void TaintExample.testPrivacySinkAnnot3(), 2, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure testPrivacySinkAnnot3(),start of procedure privacySource(),return from a call to String TaintExample.privacySource()] -codetoanalyze/java/infer/TaintExample.java, void TaintExample.testPrivacySourceAnnot(), 1, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure testPrivacySourceAnnot(),start of procedure privacySource(),return from a call to String TaintExample.privacySource()] -codetoanalyze/java/infer/TaintExample.java, void TaintExample.testPrivacySourceFieldAnnotPropagation(), 2, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure testPrivacySourceFieldAnnotPropagation()] -codetoanalyze/java/infer/TaintExample.java, void TaintExample.testPrivacySourceInstanceFieldAnnot(), 2, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure testPrivacySourceInstanceFieldAnnot()] -codetoanalyze/java/infer/TaintExample.java, void TaintExample.testPrivacySourceStaticFieldAnnot(), 2, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure testPrivacySourceStaticFieldAnnot()] codetoanalyze/java/infer/WriterLeaks.java, void WriterLeaks.bufferedWriterNotClosedAfterWrite(), 7, RESOURCE_LEAK, [start of procedure bufferedWriterNotClosedAfterWrite(),Skipped call: function or method not found,Skipped call: function or method not found,exception java.io.IOException] codetoanalyze/java/infer/WriterLeaks.java, void WriterLeaks.fileWriterNotClosedAfterWrite(), 6, RESOURCE_LEAK, [start of procedure fileWriterNotClosedAfterWrite(),Skipped call: function or method not found,exception java.io.IOException] codetoanalyze/java/infer/WriterLeaks.java, void WriterLeaks.outputStreamWriterNotClosedAfterWrite(), 6, RESOURCE_LEAK, [start of procedure outputStreamWriterNotClosedAfterWrite(),Skipped call: function or method not found,exception java.io.IOException] diff --git a/infer/tests/codetoanalyze/java/infer/TaintExample.java b/infer/tests/codetoanalyze/java/infer/TaintExample.java deleted file mode 100644 index 931d0c0d5..000000000 --- a/infer/tests/codetoanalyze/java/infer/TaintExample.java +++ /dev/null @@ -1,267 +0,0 @@ -/* - * 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 codetoanalyze.java.infer; - -import java.io.InputStream; -import java.io.IOException; -import java.net.MalformedURLException; -import java.net.Socket; -import java.net.URL; - -import javax.net.ssl.HostnameVerifier; -import javax.net.ssl.SSLException; -import javax.net.ssl.SSLSession; -import javax.net.ssl.SSLSocket; -import javax.net.ssl.SSLSocketFactory; - -import android.content.ContentValues; -import android.content.SharedPreferences; - -import com.facebook.infer.builtins.InferTaint; -import com.facebook.infer.annotation.IntegritySource; -import com.facebook.infer.annotation.IntegritySink; -import com.facebook.infer.annotation.PrivacySource; -import com.facebook.infer.annotation.PrivacySink; - -public class TaintExample { - - public InputStream socketNotVerifiedSimple(SSLSocketFactory f) - throws IOException { - Socket socket = f.createSocket(); - return socket.getInputStream(); - } - - public InputStream socketVerifiedForgotToCheckRetval(SSLSocketFactory f, - HostnameVerifier v, - SSLSession session) - throws IOException { - - Socket socket = f.createSocket(); - v.verify("hostname", session); - return socket.getInputStream(); - } - - public InputStream socketVerifiedOk1(SSLSocketFactory f, - HostnameVerifier v, - SSLSession session) - throws IOException { - - Socket socket = f.createSocket(); - if (v.verify("hostname", session)) { - return socket.getInputStream(); - } else { - return null; - } - } - - HostnameVerifier mHostnameVerifier; - - public void throwExceptionIfNoVerify(SSLSocket sslSocket, String host) - throws IOException { - - if (!mHostnameVerifier.verify(host, sslSocket.getSession())) { - throw new SSLException("Couldn't verify!"); - } - } - - public InputStream socketVerifiedOk2(SSLSocketFactory f) throws IOException { - SSLSocket s = (SSLSocket) f.createSocket(); - throwExceptionIfNoVerify(s, "hostname"); - return s.getInputStream(); - } - - public InputStream socketIgnoreExceptionNoVerify(SSLSocketFactory f) - throws IOException { - - SSLSocket s = (SSLSocket) f.createSocket(); - try { - throwExceptionIfNoVerify(s, "hostname"); - } catch (SSLException e) { - // ignore the fact that verifying the socket failed - } - return s.getInputStream(); - } - - public InputStream taintingShouldNotPreventInference1(SSLSocketFactory f) throws IOException { - socketNotVerifiedSimple(f).toString(); - // failing to infer a post for socketNotVerifiedSimple will hide this error - Socket s = f.createSocket(); - return s.getInputStream(); - } - - public InputStream readInputStream(Socket socket) throws IOException { - return socket.getInputStream(); - } - - // if we're not careful, postcondition inference will fail for this function - Socket callReadInputStreamCauseTaintError(SSLSocketFactory f) - throws IOException { - Socket socket = f.createSocket(); - InputStream s = readInputStream(socket); - s.toString(); // to avoid RETURN_VALUE_IGNORED warning - return f.createSocket(); - } - - InputStream taintingShouldNotPreventInference2(SSLSocketFactory f) throws IOException { - // if inference fails for this callee, we won't report an error here - Socket s = callReadInputStreamCauseTaintError(f); - 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()); - } - - public void simpleTaintErrorWithModelMethodsUndefined() { - Object o = InferTaint.inferSecretSourceUndefined(); - InferTaint.inferSensitiveSinkUndefined(o); - } - - public Object returnTaintedSourceModelMethodsUndefined() { - return InferTaint.inferSecretSourceUndefined(); - } - - public void callSinkMethodModelMethodsUndefined(Object o) { - InferTaint.inferSensitiveSinkUndefined(o); - } - - public void interprocTaintErrorWithModelMethodsUndefined1() { - InferTaint.inferSensitiveSinkUndefined(returnTaintedSourceModelMethodsUndefined()); - } - - public void interprocTaintErrorWithModelMethodsUndefined2() { - callSinkMethodModelMethodsUndefined(InferTaint.inferSecretSourceUndefined()); - } - - public void interprocTaintErrorWithModelMethodsUndefined3() { - callSinkMethodModelMethodsUndefined(returnTaintedSourceModelMethodsUndefined()); - } - - public void contentValuesPutWithTaintedString(ContentValues values, SharedPreferences prefs, - String key, String value) { - values.put(key, prefs.getString(key, value)); - } - - public void contentValuesPutOk(ContentValues values, String key, String value) { - values.put(key, value); - } - - @PrivacySource - public String privacySource() { - return "source"; - } - - public void testPrivacySourceAnnot() { - InferTaint.inferSensitiveSinkUndefined(privacySource()); // should report - } - - public void instancePrivacySink(@PrivacySink String s1, String s2) { - } - - public static void staticPrivacySink(@PrivacySink String s1, String s2) { - } - - public void testPrivacySinkAnnot1() { - String source = privacySource(); - instancePrivacySink(source, ""); // should report - } - - public void testPrivacySinkAnnot2() { - String source = privacySource(); - instancePrivacySink("", source); // should not report - } - - public void testPrivacySinkAnnot3() { - String source = privacySource(); - staticPrivacySink(source, ""); // should report - } - - public void testPrivacySinkAnnot4() { - String source = privacySource(); - staticPrivacySink("", source); // should not report - } - - @PrivacySource String mPrivacySource; - - @PrivacySource String sPrivacySource; - - public void testPrivacySourceInstanceFieldAnnot() { - String source = mPrivacySource; - InferTaint.inferSensitiveSinkUndefined(source); // should report - } - - public void testPrivacySourceStaticFieldAnnot() { - String source = sPrivacySource; - InferTaint.inferSensitiveSinkUndefined(source); // should report - } - - String aFieldWithoutAnnotations; - - public void testPrivacySourceFieldAnnotPropagation() { - aFieldWithoutAnnotations = mPrivacySource; - InferTaint.inferSensitiveSinkUndefined(aFieldWithoutAnnotations); // should report - } - - @IntegritySource - public String integritySource() { - return "source"; - } - - @IntegritySource String mIntegritySource; - - @IntegritySource String sIntegritySource; - - public void testIntegritySourceAnnot() { - InferTaint.inferSensitiveSinkUndefined(integritySource()); // should report - } - - public void testIntegritySourceInstanceFieldAnnot() { - String source = mIntegritySource; - InferTaint.inferSensitiveSinkUndefined(source); // should report - } - - public void testIntegritySourceStaticFieldAnnot() { - String source = sIntegritySource; - InferTaint.inferSensitiveSinkUndefined(source); // should report - } - - public void integritySink(@IntegritySink String s1, String s2) { - } - - void testIntegritySinkAnnotReport(String s) { - integritySink(integritySource(), s); // should report - } - - void testIntegritySinkAnnotNoReport(String s) { - integritySink(s, integritySource()); // should not report - } - -} diff --git a/infer/tests/codetoanalyze/java/infer/issues.exp b/infer/tests/codetoanalyze/java/infer/issues.exp index 72e618196..b9f046e49 100644 --- a/infer/tests/codetoanalyze/java/infer/issues.exp +++ b/infer/tests/codetoanalyze/java/infer/issues.exp @@ -271,31 +271,6 @@ codetoanalyze/java/infer/ReturnValueIgnored.java, void ReturnValueIgnored.return codetoanalyze/java/infer/SuppressLintExample.java, void SuppressAllWarnigsInTheClass.shouldNotReportNPE(), 2, NULL_DEREFERENCE, [start of procedure shouldNotReportNPE()] codetoanalyze/java/infer/SuppressLintExample.java, void SuppressAllWarnigsInTheClass.shouldNotReportResourceLeak(), 2, RESOURCE_LEAK, [start of procedure shouldNotReportResourceLeak()] codetoanalyze/java/infer/SuppressLintExample.java, void SuppressLintExample.shouldReportNPE(), 2, NULL_DEREFERENCE, [start of procedure shouldReportNPE()] -codetoanalyze/java/infer/TaintExample.java, InputStream TaintExample.socketIgnoreExceptionNoVerify(SSLSocketFactory), 9, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure socketIgnoreExceptionNoVerify(...),start of procedure throwExceptionIfNoVerify(...),Taking true branch,exception javax.net.ssl.SSLException,return from a call to void TaintExample.throwExceptionIfNoVerify(SSLSocket,String),Switch condition is true. Entering switch case] -codetoanalyze/java/infer/TaintExample.java, InputStream TaintExample.socketNotVerifiedSimple(SSLSocketFactory), 3, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure socketNotVerifiedSimple(...)] -codetoanalyze/java/infer/TaintExample.java, InputStream TaintExample.socketVerifiedForgotToCheckRetval(SSLSocketFactory,HostnameVerifier,SSLSession), 6, RETURN_VALUE_IGNORED, [start of procedure socketVerifiedForgotToCheckRetval(...)] -codetoanalyze/java/infer/TaintExample.java, InputStream TaintExample.socketVerifiedForgotToCheckRetval(SSLSocketFactory,HostnameVerifier,SSLSession), 7, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure socketVerifiedForgotToCheckRetval(...)] -codetoanalyze/java/infer/TaintExample.java, InputStream TaintExample.taintingShouldNotPreventInference1(SSLSocketFactory), 4, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure taintingShouldNotPreventInference1(...),start of procedure socketNotVerifiedSimple(...),return from a call to InputStream TaintExample.socketNotVerifiedSimple(SSLSocketFactory),Skipped call: function or method not found] -codetoanalyze/java/infer/TaintExample.java, Socket TaintExample.callReadInputStreamCauseTaintError(SSLSocketFactory), 3, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure callReadInputStreamCauseTaintError(...)] -codetoanalyze/java/infer/TaintExample.java, void TaintExample.contentValuesPutWithTaintedString(ContentValues,SharedPreferences,String,String), 2, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure contentValuesPutWithTaintedString(...)] -codetoanalyze/java/infer/TaintExample.java, void TaintExample.interprocTaintErrorWithModelMethods1(), 1, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure interprocTaintErrorWithModelMethods1(),start of procedure returnTaintedSourceModelMethods(),return from a call to Object TaintExample.returnTaintedSourceModelMethods()] -codetoanalyze/java/infer/TaintExample.java, void TaintExample.interprocTaintErrorWithModelMethods2(), 1, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure interprocTaintErrorWithModelMethods2()] -codetoanalyze/java/infer/TaintExample.java, void TaintExample.interprocTaintErrorWithModelMethods3(), 1, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure interprocTaintErrorWithModelMethods3(),start of procedure returnTaintedSourceModelMethods(),return from a call to Object TaintExample.returnTaintedSourceModelMethods()] -codetoanalyze/java/infer/TaintExample.java, void TaintExample.interprocTaintErrorWithModelMethodsUndefined1(), 1, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure interprocTaintErrorWithModelMethodsUndefined1(),start of procedure returnTaintedSourceModelMethodsUndefined(),return from a call to Object TaintExample.returnTaintedSourceModelMethodsUndefined()] -codetoanalyze/java/infer/TaintExample.java, void TaintExample.interprocTaintErrorWithModelMethodsUndefined2(), 1, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure interprocTaintErrorWithModelMethodsUndefined2()] -codetoanalyze/java/infer/TaintExample.java, void TaintExample.interprocTaintErrorWithModelMethodsUndefined3(), 1, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure interprocTaintErrorWithModelMethodsUndefined3(),start of procedure returnTaintedSourceModelMethodsUndefined(),return from a call to Object TaintExample.returnTaintedSourceModelMethodsUndefined()] -codetoanalyze/java/infer/TaintExample.java, void TaintExample.simpleTaintErrorWithModelMethods(), 2, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure simpleTaintErrorWithModelMethods()] -codetoanalyze/java/infer/TaintExample.java, void TaintExample.simpleTaintErrorWithModelMethodsUndefined(), 2, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure simpleTaintErrorWithModelMethodsUndefined(),Skipped call: function or method not found] -codetoanalyze/java/infer/TaintExample.java, void TaintExample.testIntegritySinkAnnotReport(String), 1, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure testIntegritySinkAnnotReport(...),start of procedure integritySource(),return from a call to String TaintExample.integritySource()] -codetoanalyze/java/infer/TaintExample.java, void TaintExample.testIntegritySourceAnnot(), 1, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure testIntegritySourceAnnot(),start of procedure integritySource(),return from a call to String TaintExample.integritySource()] -codetoanalyze/java/infer/TaintExample.java, void TaintExample.testIntegritySourceInstanceFieldAnnot(), 2, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure testIntegritySourceInstanceFieldAnnot()] -codetoanalyze/java/infer/TaintExample.java, void TaintExample.testIntegritySourceStaticFieldAnnot(), 2, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure testIntegritySourceStaticFieldAnnot()] -codetoanalyze/java/infer/TaintExample.java, void TaintExample.testPrivacySinkAnnot1(), 2, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure testPrivacySinkAnnot1(),start of procedure privacySource(),return from a call to String TaintExample.privacySource()] -codetoanalyze/java/infer/TaintExample.java, void TaintExample.testPrivacySinkAnnot3(), 2, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure testPrivacySinkAnnot3(),start of procedure privacySource(),return from a call to String TaintExample.privacySource()] -codetoanalyze/java/infer/TaintExample.java, void TaintExample.testPrivacySourceAnnot(), 1, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure testPrivacySourceAnnot(),start of procedure privacySource(),return from a call to String TaintExample.privacySource()] -codetoanalyze/java/infer/TaintExample.java, void TaintExample.testPrivacySourceFieldAnnotPropagation(), 2, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure testPrivacySourceFieldAnnotPropagation()] -codetoanalyze/java/infer/TaintExample.java, void TaintExample.testPrivacySourceInstanceFieldAnnot(), 2, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure testPrivacySourceInstanceFieldAnnot()] -codetoanalyze/java/infer/TaintExample.java, void TaintExample.testPrivacySourceStaticFieldAnnot(), 2, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure testPrivacySourceStaticFieldAnnot()] codetoanalyze/java/infer/WriterLeaks.java, void WriterLeaks.bufferedWriterNotClosedAfterWrite(), 7, RESOURCE_LEAK, [start of procedure bufferedWriterNotClosedAfterWrite(),Skipped call: function or method not found,Skipped call: function or method not found,exception java.io.IOException] codetoanalyze/java/infer/WriterLeaks.java, void WriterLeaks.fileWriterNotClosedAfterWrite(), 6, RESOURCE_LEAK, [start of procedure fileWriterNotClosedAfterWrite(),Skipped call: function or method not found,exception java.io.IOException] codetoanalyze/java/infer/WriterLeaks.java, void WriterLeaks.outputStreamWriterNotClosedAfterWrite(), 6, RESOURCE_LEAK, [start of procedure outputStreamWriterNotClosedAfterWrite(),Skipped call: function or method not found,exception java.io.IOException] diff --git a/infer/tests/codetoanalyze/objc/errors/issues.exp b/infer/tests/codetoanalyze/objc/errors/issues.exp index 1cf9441e4..4ed91f404 100644 --- a/infer/tests/codetoanalyze/objc/errors/issues.exp +++ b/infer/tests/codetoanalyze/objc/errors/issues.exp @@ -110,11 +110,6 @@ codetoanalyze/objc/errors/npe/ivar_blocks.m, MyClass_ivar_npe, 1, IVAR_NOT_NULL_ codetoanalyze/objc/errors/npe/skip_method_with_nil_object.m, SkipMethodNilA_testBug:, 6, PARAMETER_NOT_NULL_CHECKED, [start of procedure testBug:,Message get_a with receiver nil returns nil.,Message skip_method with receiver nil returns nil.,Condition is false] codetoanalyze/objc/errors/property/main.c, property_main, 3, MEMORY_LEAK, [start of procedure property_main(),Skipped call: function or method not found] codetoanalyze/objc/errors/resource_leaks/Dispatch_sources.m, __objc_anonymous_block_ProcessContentsOfFile______2, 6, MEMORY_LEAK, [start of procedure block,Skipped call: function or method not found,Condition is true,Skipped call: function or method not found] -codetoanalyze/objc/errors/taint/sources.m, testNSHTTPCookie1, 5, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure testNSHTTPCookie1()] -codetoanalyze/objc/errors/taint/sources.m, testNSHTTPCookie2, 5, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure testNSHTTPCookie2()] -codetoanalyze/objc/errors/taint/sources.m, testNSHTTPCookie3, 5, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure testNSHTTPCookie3()] -codetoanalyze/objc/errors/taint/sources.m, testNSHTTPCookie4, 5, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure testNSHTTPCookie4()] -codetoanalyze/objc/errors/taint/viewController.m, ExampleDelegate_application:openURL:sourceApplication:annotation:, 7, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure application:openURL:sourceApplication:annotation:,start of procedure init,return from a call to VCA_init,start of procedure ExampleSanitizer(),Condition is false,return from a call to ExampleSanitizer,Condition is false,Condition is true] codetoanalyze/objc/shared/annotations/nonnull_annotations.m, A_test1:, 2, PARAMETER_NOT_NULL_CHECKED, [start of procedure test1:,Message child with receiver nil returns nil.] codetoanalyze/objc/shared/annotations/nonnull_annotations.m, A_test3:, 1, PARAMETER_NOT_NULL_CHECKED, [start of procedure test3:] codetoanalyze/objc/shared/annotations/nullable_annotations.m, User_otherUserName, 2, NULL_DEREFERENCE, [start of procedure otherUserName,Skipped call: function or method not found]