Summary: Using a dedicated abstract domain, like Quandary does, is more suitable for taint analysis. Reviewed By: sblackshear Differential Revision: D5473794 fbshipit-source-id: c917417master
Jeremy Dubreil
8 years ago
committed by
Facebook Github Bot
parent
fd4fbe163c
commit
f49d292c3b
@ -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);
|
|
||||||
}
|
|
||||||
|
|
||||||
}
|
|
||||||
@ -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();
|
|
||||||
}
|
|
||||||
|
|
||||||
}
|
|
||||||
@ -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;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
}
|
|
||||||
@ -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
|
|
||||||
@ -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
|
|
||||||
@ -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 = []
|
|
||||||
@ -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
|
|
||||||
@ -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
|
|
||||||
}
|
|
||||||
|
|
||||||
}
|
|
||||||
Loading…
Reference in new issue