From 06e0f6fbc9f5f415f2ea2e27d04c58bdbe1879f3 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Tue, 20 Dec 2016 09:28:54 -0800 Subject: [PATCH] [quandary] support tainted formals Summary: We currently can only model the return values of functions as sources. In order to model inputs of endpoints as sources, we need the capability to treat the formals of certain functions as sources too. This diff adds that capability by adding a function for getting the tainted sources to the source module, then using that info in the analysis. Reviewed By: jeremydubreil Differential Revision: D4314738 fbshipit-source-id: dd7d423 --- infer/src/checkers/Source.ml | 7 ++- infer/src/checkers/Source.mli | 6 +- infer/src/quandary/CppTrace.ml | 3 + infer/src/quandary/JavaTrace.ml | 35 ++++++++++++ infer/src/quandary/TaintAnalysis.ml | 33 ++++++----- infer/src/unit/TaintTests.ml | 1 + infer/src/unit/TraceTests.ml | 1 + .../java/quandary/TaintedFormals.java | 56 +++++++++++++++++++ .../codetoanalyze/java/quandary/issues.exp | 6 ++ 9 files changed, 129 insertions(+), 19 deletions(-) create mode 100644 infer/tests/codetoanalyze/java/quandary/TaintedFormals.java 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)]