diff --git a/infer/src/checkers/Source.ml b/infer/src/checkers/Source.ml index d6436beb3..f22dac8bc 100644 --- a/infer/src/checkers/Source.ml +++ b/infer/src/checkers/Source.ml @@ -18,8 +18,9 @@ module type S = sig val get_footprint_access_path: t -> AccessPath.t option - (** return Some (kind) if the call site is a taint source, None otherwise *) val get : CallSite.t -> t option + + val get_tainted_formals : Procdesc.t -> (Mangled.t * Typ.t * t option) list end module Dummy = struct @@ -37,8 +38,12 @@ module Dummy = struct let make_footprint _ _ = assert false let get_footprint_access_path _ = assert false + let get _ = None + let get_tainted_formals pdesc = + IList.map (fun (name, typ) -> name, typ, None) (Procdesc.get_formals pdesc) + module Kind = struct type nonrec t = t let compare = compare diff --git a/infer/src/checkers/Source.mli b/infer/src/checkers/Source.mli index e9949ecb8..487b056a3 100644 --- a/infer/src/checkers/Source.mli +++ b/infer/src/checkers/Source.mli @@ -18,8 +18,12 @@ module type S = sig val get_footprint_access_path: t -> AccessPath.t option - (** return Some (kind) if the call site is a taint source, None otherwise *) + (** return Some (source) if the call site is a taint source, None otherwise *) val get : CallSite.t -> t option + + (** return each formal of the function paired with either Some(source) if the formal is a taint + source, or None if the formal is not a taint source *) + val get_tainted_formals : Procdesc.t -> (Mangled.t * Typ.t * t option) list end module Dummy : S with type t = unit diff --git a/infer/src/quandary/CppTrace.ml b/infer/src/quandary/CppTrace.ml index c91e3371d..26d197d54 100644 --- a/infer/src/quandary/CppTrace.ml +++ b/infer/src/quandary/CppTrace.ml @@ -79,6 +79,9 @@ module CppSource = struct | pname -> failwithf "Non-C++ procname %a in C++ analysis@." Procname.pp pname + let get_tainted_formals pdesc = + IList.map (fun (name, typ) -> name, typ, None) (Procdesc.get_formals pdesc) + let with_callsite t callee_site = { t with site = callee_site; } diff --git a/infer/src/quandary/JavaTrace.ml b/infer/src/quandary/JavaTrace.ml index ecee33cb1..afeb565bb 100644 --- a/infer/src/quandary/JavaTrace.ml +++ b/infer/src/quandary/JavaTrace.ml @@ -81,6 +81,41 @@ module JavaSource = struct | pname when BuiltinDecl.is_declared pname -> None | pname -> failwithf "Non-Java procname %a in Java analysis@." Procname.pp pname + let get_tainted_formals pdesc = + let make_untainted (name, typ) = + name, typ, None in + let taint_formals_with_types type_strs kind pdesc formals = + let taint_formal_with_types ((formal_name, formal_typ) as formal) = + let matches_classname typ typ_str = match typ with + | Typ.Tptr (Tstruct typename, _) -> Typename.name typename = typ_str + | _ -> false in + if IList.mem matches_classname formal_typ type_strs + then + let site = CallSite.make (Procdesc.get_proc_name pdesc) (Procdesc.get_loc pdesc) in + formal_name, formal_typ, Some (make kind site) + else + make_untainted formal in + IList.map taint_formal_with_types formals in + + let formals = Procdesc.get_formals pdesc in + match Procdesc.get_proc_name pdesc with + | Procname.Java java_pname -> + begin + match Procname.java_get_class_name java_pname, Procname.java_get_method java_pname with + | "codetoanalyze.java.quandary.TaintedFormals", "taintedContextBad" -> + taint_formals_with_types + ["java.lang.Integer"; "java.lang.String"] + Other + pdesc + formals + | _ -> + IList.map make_untainted formals + end + | procname -> + failwithf + "Non-Java procedure %a where only Java procedures are expected" + Procname.pp procname + let with_callsite t callee_site = { t with site = callee_site; } diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml index 09a5e09a3..6028ce9a1 100644 --- a/infer/src/quandary/TaintAnalysis.ml +++ b/infer/src/quandary/TaintAnalysis.ml @@ -19,8 +19,8 @@ module Make (TaintSpecification : TaintSpec.S) = struct module TaintDomain = TaintSpecification.AccessTree module IdMapDomain = IdAccessPathMapDomain - (** map from formals to their position *) - type formal_map = int AccessPath.BaseMap.t + (** a map from a formal to its position and (optionally) whether we should treat it as a source *) + type formal_map = (int * TraceDomain.Source.t option) AccessPath.BaseMap.t module Summary = Summary.Make(struct type summary = QuandarySummary.t @@ -90,13 +90,6 @@ module Make (TaintSpecification : TaintSpec.S) = struct type extras = formal_map - let is_formal base formal_map = - AccessPath.BaseMap.mem base formal_map - - let is_rooted_in_environment ap formal_map = - let root, _ = AccessPath.extract ap in - is_formal root formal_map || is_global root - let resolve_id id_map id = try Some (IdMapDomain.find id id_map) with Not_found -> None @@ -116,8 +109,14 @@ module Make (TaintSpecification : TaintSpec.S) = struct Some (TaintDomain.make_normal_leaf trace) in let root, _ = AccessPath.extract access_path in try - let formal_num = AccessPath.BaseMap.find root proc_data.extras in - make_footprint_trace (make_footprint_access_path formal_num access_path) + let formal_num, taint_opt = AccessPath.BaseMap.find root proc_data.extras in + begin + match taint_opt with + | None -> + make_footprint_trace (make_footprint_access_path formal_num access_path) + | Some source -> + Some (TaintDomain.make_normal_leaf (TraceDomain.of_source source)) + end with Not_found -> if is_global root then make_footprint_trace access_path @@ -502,7 +501,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct (fun base node acc -> let base' = try - let formal_index = AccessPath.BaseMap.find base formal_map in + let formal_index, _ = AccessPath.BaseMap.find base formal_map in make_footprint_var formal_index, snd base with Not_found -> base in @@ -533,15 +532,15 @@ module Make (TaintSpecification : TaintSpec.S) = struct let make_extras pdesc = let pname = Procdesc.get_proc_name pdesc in - let attrs = Procdesc.get_attributes pdesc in let formals_with_nums = IList.mapi - (fun index (name, typ) -> + (fun index (name, typ, taint_opt) -> let pvar = Pvar.mk name pname in - AccessPath.base_of_pvar pvar typ, index) - attrs.ProcAttributes.formals in + AccessPath.base_of_pvar pvar typ, index, taint_opt) + (TraceDomain.Source.get_tainted_formals pdesc) in IList.fold_left - (fun formal_map (base, index) -> AccessPath.BaseMap.add base index formal_map) + (fun formal_map (base, index, taint_opt) -> + AccessPath.BaseMap.add base (index, taint_opt) formal_map) AccessPath.BaseMap.empty formals_with_nums in diff --git a/infer/src/unit/TaintTests.ml b/infer/src/unit/TaintTests.ml index b783ab505..dfc885cfb 100644 --- a/infer/src/unit/TaintTests.ml +++ b/infer/src/unit/TaintTests.ml @@ -45,6 +45,7 @@ module MockTrace = Trace.Make(struct then Some site else None + let get_tainted_formals _ = assert false let is_footprint _ = false let make_footprint _ = assert false let get_footprint_access_path _ = assert false diff --git a/infer/src/unit/TraceTests.ml b/infer/src/unit/TraceTests.ml index e1aba04bb..11f4ef73f 100644 --- a/infer/src/unit/TraceTests.ml +++ b/infer/src/unit/TraceTests.ml @@ -68,6 +68,7 @@ module MockSource = struct let make_footprint _ _ = Footprint let get _ = assert false + let get_tainted_formals _ = [] let get_footprint_access_path _ = assert false end diff --git a/infer/tests/codetoanalyze/java/quandary/TaintedFormals.java b/infer/tests/codetoanalyze/java/quandary/TaintedFormals.java new file mode 100644 index 000000000..0de06c20d --- /dev/null +++ b/infer/tests/codetoanalyze/java/quandary/TaintedFormals.java @@ -0,0 +1,56 @@ +/* + * 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. + */ + +package codetoanalyze.java.quandary; + +import com.facebook.infer.builtins.InferTaint; + +class Obj { + Object f; +} + +public class TaintedFormals { + + public void callSink(Object formal) { + InferTaint.inferSensitiveSink(formal); + } + + // taintedFormal1 and taintedFormal2 were are modeled as tainted + public void taintedContextBad(String taintedFormal1, Boolean untaintedFormal, Integer taintedFormal2) { + InferTaint.inferSensitiveSink(taintedFormal1); // should report here + InferTaint.inferSensitiveSink(taintedFormal2); // should report here + callSink(taintedFormal1); // should report here + callSink(taintedFormal2); // should report here + + InferTaint.inferSensitiveSink(untaintedFormal); // should not report here + } + + public Object taintedContextBad(String taintedFormal) { + return taintedFormal; + } + + public void callTaintedContextBad1(String formal) { + Object tainted = taintedContextBad(formal); + InferTaint.inferSensitiveSink(tainted); + } + + public void callTaintedContextBad2() { + taintedContextBad(null, (Boolean) InferTaint.inferSecretSource(), null); + } + + public void callTaintedContextOk1() { + taintedContextBad("foo", null, null); + } + + // shouldn't report here, otherwise we will double report + public void callTaintedContextOk2() { + taintedContextBad(null, null, new Integer(1)); + } + +} diff --git a/infer/tests/codetoanalyze/java/quandary/issues.exp b/infer/tests/codetoanalyze/java/quandary/issues.exp index 49c5e7e28..2b62f632c 100644 --- a/infer/tests/codetoanalyze/java/quandary/issues.exp +++ b/infer/tests/codetoanalyze/java/quandary/issues.exp @@ -175,4 +175,10 @@ codetoanalyze/java/quandary/Strings.java, void Strings.viaStringBufferIgnoreRetu codetoanalyze/java/quandary/Strings.java, void Strings.viaStringBuilderBad(), 3, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),call to void InferTaint.inferSensitiveSink(Object)] codetoanalyze/java/quandary/Strings.java, void Strings.viaStringBuilderIgnoreReturnBad(), 5, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),call to void InferTaint.inferSensitiveSink(Object)] codetoanalyze/java/quandary/Strings.java, void Strings.viaStringBuilderSugarBad(), 2, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),call to void InferTaint.inferSensitiveSink(Object)] +codetoanalyze/java/quandary/TaintedFormals.java, void TaintedFormals.callTaintedContextBad1(String), 2, QUANDARY_TAINT_ERROR, [return from Object TaintedFormals.taintedContextBad(String),return from Object TaintedFormals.taintedContextBad(String),call to void InferTaint.inferSensitiveSink(Object)] +codetoanalyze/java/quandary/TaintedFormals.java, void TaintedFormals.callTaintedContextBad2(), 1, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),call to void TaintedFormals.taintedContextBad(String,Boolean,Integer),call to void InferTaint.inferSensitiveSink(Object)] +codetoanalyze/java/quandary/TaintedFormals.java, void TaintedFormals.taintedContextBad(String,Boolean,Integer), 1, QUANDARY_TAINT_ERROR, [return from void TaintedFormals.taintedContextBad(String,Boolean,Integer),call to void InferTaint.inferSensitiveSink(Object)] +codetoanalyze/java/quandary/TaintedFormals.java, void TaintedFormals.taintedContextBad(String,Boolean,Integer), 2, QUANDARY_TAINT_ERROR, [return from void TaintedFormals.taintedContextBad(String,Boolean,Integer),call to void InferTaint.inferSensitiveSink(Object)] +codetoanalyze/java/quandary/TaintedFormals.java, void TaintedFormals.taintedContextBad(String,Boolean,Integer), 3, QUANDARY_TAINT_ERROR, [return from void TaintedFormals.taintedContextBad(String,Boolean,Integer),call to void TaintedFormals.callSink(Object),call to void InferTaint.inferSensitiveSink(Object)] +codetoanalyze/java/quandary/TaintedFormals.java, void TaintedFormals.taintedContextBad(String,Boolean,Integer), 4, QUANDARY_TAINT_ERROR, [return from void TaintedFormals.taintedContextBad(String,Boolean,Integer),call to void TaintedFormals.callSink(Object),call to void InferTaint.inferSensitiveSink(Object)] codetoanalyze/java/quandary/UnknownCode.java, void UnknownCode.propagateViaUnknownConstructorBad(), 4, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),call to void InferTaint.inferSensitiveSink(Object)]