[quandary] vector and array access as sink

Summary: Useful for identifying user-controlled array accesses that could lead to buffer overflows

Reviewed By: mbouaziz

Differential Revision: D5520985

fbshipit-source-id: 92984f6

infer/src/IR/BUILTINS.mli

@@ -13,6 +13,8 @@ open! IStd
 module type S = sig
   type t
 
+  val __array_access : t
+
   val __assert_fail : t
 
   val __builtin_va_arg : t

infer/src/IR/BuiltinDecl.ml

@@ -30,6 +30,8 @@ let create_objc_class_method class_name method_name =
 
 let is_declared pname = Typ.Procname.Set.mem pname !builtin_decls
 
+let __array_access = create_procname "__array_access"
+
 let __assert_fail = create_procname "__assert_fail"
 
 let __builtin_va_arg = create_procname "__builtin_va_arg"

infer/src/backend/BuiltinDefn.ml

@@ -1030,6 +1030,9 @@ let execute___objc_dictionary_literal builtin_args =
   let pname = BuiltinDecl.__objc_dictionary_literal in
   execute_objc_NSDictionary_alloc_no_fail res' pname builtin_args
 
+(* only used in Quandary, so ok to skip *)
+let __array_access = Builtin.register BuiltinDecl.__array_access execute_skip
+
 let __assert_fail = Builtin.register BuiltinDecl.__assert_fail execute___assert_fail
 
 let __builtin_va_arg = Builtin.register BuiltinDecl.__builtin_va_arg execute___builtin_va_arg

infer/src/checkers/accessTree.ml

@@ -14,7 +14,8 @@ module L = Logging
 module type S = sig
   module TraceDomain : AbstractDomain.WithBottom
 
-  module AccessMap = AccessPath.AccessMap
+  module AccessMap : PrettyPrintable.PPMap with type key = AccessPath.access
+
   module BaseMap = AccessPath.BaseMap
 
   type node = TraceDomain.astate * tree
@@ -53,7 +54,21 @@ end
 
 module Make (TraceDomain : AbstractDomain.WithBottom) = struct
   module TraceDomain = TraceDomain
-  module AccessMap = AccessPath.AccessMap
+
+  module AccessMap = PrettyPrintable.MakePPMap (struct
+    type t = AccessPath.access
+
+    let compare a1 a2 =
+      match (a1, a2) with
+      | AccessPath.ArrayAccess (t1, _), AccessPath.ArrayAccess (t2, _)
+       -> (* ignore indexes *)
+          Typ.compare t1 t2
+      | _
+       -> AccessPath.compare_access a1 a2
+
+    let pp = AccessPath.pp_access
+  end)
+
   module BaseMap = AccessPath.BaseMap
 
   type node = (TraceDomain.astate * tree)

infer/src/checkers/accessTree.mli

@@ -13,7 +13,7 @@ open! IStd
 module type S = sig
   module TraceDomain : AbstractDomain.WithBottom
 
-  module AccessMap = AccessPath.AccessMap
+  module AccessMap : PrettyPrintable.PPMap with type key = AccessPath.access
   module BaseMap = AccessPath.BaseMap
 
   type node = TraceDomain.astate * tree

infer/src/quandary/ClangTrace.ml

@@ -84,17 +84,22 @@ module SourceKind = struct
      -> failwithf "Non-C++ procname %a in C++ analysis@." Typ.Procname.pp pname
 
   let get_tainted_formals pdesc _ =
+    let get_tainted_formals_ qualified_pname =
+      if String.Set.mem endpoints qualified_pname then
+        List.map
+          ~f:(fun (name, typ) -> (name, typ, Some (Endpoint (name, typ.Typ.desc))))
+          (Procdesc.get_formals pdesc)
+      else Source.all_formals_untainted pdesc
+    in
     match Procdesc.get_proc_name pdesc with
     | Typ.Procname.ObjC_Cpp objc as pname
      -> let qualified_pname =
           F.sprintf "%s::%s" (Typ.Procname.objc_cpp_get_class_name objc)
             (Typ.Procname.get_method pname)
         in
-        if String.Set.mem endpoints qualified_pname then
-          List.map
-            ~f:(fun (name, typ) -> (name, typ, Some (Endpoint (name, typ.Typ.desc))))
-            (Procdesc.get_formals pdesc)
-        else Source.all_formals_untainted pdesc
+        get_tainted_formals_ qualified_pname
+    | Typ.Procname.C _ as pname
+     -> get_tainted_formals_ (Typ.Procname.get_method pname)
     | _
      -> Source.all_formals_untainted pdesc
 
@@ -118,6 +123,7 @@ module CppSource = Source.Make (SourceKind)
 module SinkKind = struct
   type t =
     | Allocation  (** memory allocation *)
+    | BufferAccess  (** read/write an array *)
     | ShellExec  (** shell exec function *)
     | SQL  (** SQL query *)
     | Other  (** for testing or uncategorized sinks *)
@@ -143,7 +149,7 @@ module SinkKind = struct
   let taint_nth n kind actuals =
     if n < List.length actuals then Some (kind, IntSet.singleton n) else None
 
-  let taint_all actuals kind =
+  let taint_all kind actuals =
     Some (kind, IntSet.of_list (List.mapi ~f:(fun actual_num _ -> actual_num) actuals))
 
   (* return Some(sink kind) if [procedure_name] is in the list of externally specified sinks *)
@@ -158,20 +164,37 @@ module SinkKind = struct
             taint_nth n kind actuals
           with Failure _ ->
             (* couldn't parse the index, just taint everything *)
-            taint_all actuals kind
+            taint_all kind actuals
         else None)
       external_sinks
 
   let get pname actuals _ =
+    let is_buffer_class cpp_name =
+      (* assume it's a buffer class if it's "vector-y", "array-y", or "string-y". don't want to
+         report on accesses to maps etc., but also want to recognize custom vectors like fbvector
+         rather than overfitting to std::vector *)
+      let typename =
+        String.lowercase (Typ.Name.to_string (Typ.Procname.objc_cpp_get_class_type_name cpp_name))
+      in
+      String.is_substring ~substring:"vec" typename
+      || String.is_substring ~substring:"array" typename
+      || String.is_substring ~substring:"string" typename
+    in
     match pname with
-    | Typ.Procname.ObjC_Cpp _
-     -> get_external_sink pname actuals
+    | Typ.Procname.ObjC_Cpp cpp_name -> (
+      match Typ.Procname.get_method pname with
+      | "operator[]" when is_buffer_class cpp_name
+        -> taint_nth 1 BufferAccess actuals
+      | _
+        -> get_external_sink pname actuals )
+    | Typ.Procname.C _ when Typ.Procname.equal pname BuiltinDecl.__array_access
+      -> taint_all BufferAccess actuals
     | Typ.Procname.C _ -> (
       match Typ.Procname.to_string pname with
       | "execl" | "execlp" | "execle" | "execv" | "execve" | "execvp" | "system"
-       -> taint_all actuals ShellExec
+       -> taint_all ShellExec actuals
       | "brk" | "calloc" | "malloc" | "realloc" | "sbrk"
-       -> taint_all actuals Allocation
+       -> taint_all Allocation actuals
       | _
        -> get_external_sink pname actuals )
     | Typ.Procname.Block _
@@ -186,6 +209,8 @@ module SinkKind = struct
       ( match kind with
       | Allocation
        -> "Allocation"
+      | BufferAccess
+       -> "BufferAccess"
       | ShellExec
        -> "ShellExec"
       | SQL
@@ -208,11 +233,14 @@ include Trace.Make (struct
       || String.is_substring ~substring:"char*" lowercase_typ
     in
     match (Source.kind source, Sink.kind sink) with
+    | Endpoint _, BufferAccess
+     -> (* untrusted data from an endpoint flowing into a buffer *)
+        true
     | Endpoint (_, typ), (ShellExec | SQL)
      -> (* untrusted string data flowing to shell exec/SQL *)
         is_stringy typ
-    | (EnvironmentVariable | File), (ShellExec | SQL)
-     -> (* untrusted environment var or file data flowing to shell exec *)
+    | (EnvironmentVariable | File), (BufferAccess | ShellExec | SQL)
+     -> (* untrusted environment var or file data flowing to buffer or code injection *)
         true
     | (Endpoint _ | EnvironmentVariable | File), Allocation
      -> (* untrusted data flowing to memory allocation *)
@@ -234,6 +262,6 @@ include Trace.Make (struct
         true
     | _, Other
      -> true
-    | Unknown, (Allocation | ShellExec | SQL)
+    | Unknown, (Allocation | BufferAccess | ShellExec | SQL)
      -> false
 end)

infer/src/quandary/TaintAnalysis.ml

@@ -344,6 +344,36 @@ module Make (TaintSpecification : TaintSpec.S) = struct
       TaintDomain.trace_fold add_to_caller_tree summary caller_access_tree
 
     let exec_instr (astate: Domain.astate) (proc_data: extras ProcData.t) _ (instr: HilInstr.t) =
+      (* not all sinks are function calls; we might want to treat an array or field access as a
+         sink too. do this by pretending an access is a call to a dummy function and using the
+         existing machinery for adding function call sinks *)
+      let add_sinks_for_access_path (_, accesses) loc astate =
+        let add_sinks_for_access astate_acc = function
+          | AccessPath.FieldAccess _ | AccessPath.ArrayAccess (_, [])
+           -> astate_acc
+          | AccessPath.ArrayAccess (_, indexes)
+           -> let dummy_call_site = CallSite.make BuiltinDecl.__array_access loc in
+              let dummy_actuals =
+                List.map ~f:(fun index_ap -> HilExp.AccessPath index_ap) indexes
+              in
+              let sinks =
+                TraceDomain.Sink.get dummy_call_site dummy_actuals proc_data.ProcData.tenv
+              in
+              match sinks with
+              | None
+               -> astate_acc
+              | Some sink
+               -> add_sink sink dummy_actuals astate proc_data dummy_call_site
+        in
+        List.fold ~f:add_sinks_for_access ~init:astate accesses
+      in
+      let add_sinks_for_exp exp loc astate =
+        match exp with
+        | HilExp.AccessPath access_path
+         -> add_sinks_for_access_path access_path loc astate
+        | _
+         -> astate
+      in
       let exec_write lhs_access_path rhs_exp astate =
         let rhs_node =
           Option.value (hil_exp_get_node rhs_exp astate proc_data) ~default:TaintDomain.empty_node
@@ -363,10 +393,16 @@ module Make (TaintSpecification : TaintSpec.S) = struct
        -> (* similar to the case above; the Java frontend translates "return no exception" as
              `return null` in a void function *)
           astate
-      | Assign (lhs_access_path, rhs_exp, _)
-       -> exec_write lhs_access_path rhs_exp astate
+      | Assign (lhs_access_path, rhs_exp, loc)
+       -> add_sinks_for_exp rhs_exp loc astate |> add_sinks_for_access_path lhs_access_path loc
+          |> exec_write lhs_access_path rhs_exp
+      | Assume (assume_exp, _, _, loc)
+       -> add_sinks_for_exp assume_exp loc astate
       | Call (ret_opt, Direct called_pname, actuals, call_flags, callee_loc)
-       -> let handle_model callee_pname access_tree model =
+       -> let astate =
+            List.fold ~f:(fun acc exp -> add_sinks_for_exp exp callee_loc acc) actuals ~init:astate
+          in
+          let handle_model callee_pname access_tree model =
             let is_variadic =
               match callee_pname with
               | Typ.Procname.Java pname -> (
@@ -545,8 +581,13 @@ module Make (TaintSpecification : TaintSpec.S) = struct
        -> astate
   end
 
+  module HilConfig : LowerHil.HilConfig = struct
+    (* we want this so we can treat array accesses as sinks *)
+    let include_array_indexes = true
+  end
+
   module Analyzer =
-    AbstractInterpreter.Make (ProcCfg.Exceptional) (LowerHil.MakeDefault (TransferFunctions))
+    AbstractInterpreter.Make (ProcCfg.Exceptional) (LowerHil.Make (TransferFunctions) (HilConfig))
 
   let make_summary {ProcData.pdesc; extras= {formal_map}} access_tree =
     let is_java = Typ.Procname.is_java (Procdesc.get_proc_name pdesc) in

infer/tests/codetoanalyze/cpp/quandary/arrays.cpp

@@ -7,8 +7,41 @@
  * of patent rights can be found in the PATENTS file in the same directory.
  */
 
+#include <array>
+#include <string>
+
+extern int __infer_taint_source();
+extern void skip(int i, int j);
+
 namespace arrays {
 
+void array_sink1_bad(int arr[]) {
+  int source = __infer_taint_source();
+  arr[source] = 2;
+}
+
+int array_sink2_bad(int arr[]) {
+  int source = __infer_taint_source();
+  return arr[source];
+}
+
+int array_sink3_bad(int arr[]) { return arr[1 + __infer_taint_source()]; }
+
+void array_sink4_bad(int arr[]) {
+  int source = __infer_taint_source();
+  skip(1, arr[source]);
+}
+
+void std_array_sink_bad(std::array<int, 2> arr) {
+  int source = __infer_taint_source();
+  arr[source] = 2;
+}
+
+void std_string_sink_bad(std::string str) {
+  int source = __infer_taint_source();
+  str[source] = 'a';
+}
+
 // these examples used to crash the HIL conversion
 char index_of_literal_ok1() { return "foo"[1]; }
 

infer/tests/codetoanalyze/cpp/quandary/issues.exp

@@ -5,6 +5,12 @@ codetoanalyze/cpp/quandary/allocs.cpp, allocs::untrusted_malloc_bad, 0, QUANDARY
 codetoanalyze/cpp/quandary/allocs.cpp, allocs::untrusted_reaalloc_bad1, 0, QUANDARY_TAINT_ERROR, [Return from allocs::allocation_source,Call to realloc]
 codetoanalyze/cpp/quandary/allocs.cpp, allocs::untrusted_reaalloc_bad2, 0, QUANDARY_TAINT_ERROR, [Return from allocs::allocation_source,Call to realloc]
 codetoanalyze/cpp/quandary/allocs.cpp, allocs::untrusted_sbrk_bad, 0, QUANDARY_TAINT_ERROR, [Return from allocs::allocation_source,Call to sbrk]
+codetoanalyze/cpp/quandary/arrays.cpp, arrays::array_sink1_bad, 2, QUANDARY_TAINT_ERROR, [Return from __infer_taint_source,Call to __array_access]
+codetoanalyze/cpp/quandary/arrays.cpp, arrays::array_sink2_bad, 2, QUANDARY_TAINT_ERROR, [Return from __infer_taint_source,Call to __array_access]
+codetoanalyze/cpp/quandary/arrays.cpp, arrays::array_sink3_bad, 0, QUANDARY_TAINT_ERROR, [Return from __infer_taint_source,Call to __array_access]
+codetoanalyze/cpp/quandary/arrays.cpp, arrays::array_sink4_bad, 2, QUANDARY_TAINT_ERROR, [Return from __infer_taint_source,Call to __array_access]
+codetoanalyze/cpp/quandary/arrays.cpp, arrays::std_array_sink_bad, 2, QUANDARY_TAINT_ERROR, [Return from __infer_taint_source,Call to std::array<int,_>_operator[]]
+codetoanalyze/cpp/quandary/arrays.cpp, arrays::std_string_sink_bad, 2, QUANDARY_TAINT_ERROR, [Return from __infer_taint_source,Call to std::basic_string<char,std::char_traits<char>,std::allocator<char>>_operator[]]
 codetoanalyze/cpp/quandary/basics.cpp, basics::Obj_endpoint, 1, QUANDARY_TAINT_ERROR, [Return from basics::Obj_endpoint,Call to basics::Obj_string_sink]
 codetoanalyze/cpp/quandary/basics.cpp, basics::Obj_endpoint, 2, QUANDARY_TAINT_ERROR, [Return from basics::Obj_endpoint,Call to __infer_taint_sink]
 codetoanalyze/cpp/quandary/basics.cpp, basics::object_source_sink_bad, 2, QUANDARY_TAINT_ERROR, [Return from basics::Obj_method_source,Call to basics::Obj_method_sink]
@@ -82,3 +88,5 @@ codetoanalyze/cpp/quandary/unknown_code.cpp, unknown_code::direct_bad, 2, QUANDA
 codetoanalyze/cpp/quandary/unknown_code.cpp, unknown_code::skip_indirect_bad, 3, QUANDARY_TAINT_ERROR, [Return from __infer_taint_source,Call to __infer_taint_sink]
 codetoanalyze/cpp/quandary/unknown_code.cpp, unknown_code::skip_pointer_bad, 3, QUANDARY_TAINT_ERROR, [Return from __infer_taint_source,Call to __infer_taint_sink]
 codetoanalyze/cpp/quandary/unknown_code.cpp, unknown_code::skip_value_bad, 3, QUANDARY_TAINT_ERROR, [Return from __infer_taint_source,Call to __infer_taint_sink]
+codetoanalyze/cpp/quandary/vectors.cpp, vectors::read_vector_bad, 2, QUANDARY_TAINT_ERROR, [Return from __infer_taint_source,Call to std::vector<int,std::allocator<int>>_operator[]]
+codetoanalyze/cpp/quandary/vectors.cpp, vectors::write_vector_bad, 2, QUANDARY_TAINT_ERROR, [Return from __infer_taint_source,Call to std::vector<int,std::allocator<int>>_operator[]]

infer/tests/codetoanalyze/cpp/quandary/vectors.cpp

@@ -0,0 +1,38 @@
+/*
+ * Copyright (c) 2017 - 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.
+ */
+
+#include <map>
+#include <vector>
+
+extern int __infer_taint_source();
+
+namespace vectors {
+
+void write_vector_bad(std::vector<int> vec) {
+  int source = __infer_taint_source();
+  vec[source] = 2;
+}
+
+int read_vector_bad(std::vector<int> vec) {
+  int source = __infer_taint_source();
+  return vec[source];
+}
+
+// don't care about map accesses
+void write_map_ok(std::map<int, int> map) {
+  int source = __infer_taint_source();
+  map[source] = 2;
+}
+
+void read_map_ok(std::map<int, int> map) {
+  int source = __infer_taint_source();
+  return map[source];
+}
+
+} // namespace vectors