[inferbo] Check tainted value is used in array accesses or malloc

Summary:
This diff introduces two issue types: `BUFFER_OVERRUN_T1` and `INFERBO_ALLOC_IS_TAINTED`, which
denotes tainted values are used in array accesses and memory allocations, respectively.

Note that the taint analysis is intra-procedural for now.

Reviewed By: ezgicicek

Differential Revision: D19410536

fbshipit-source-id: af85148ec

infer/man/man1/infer-full.txt

@@ -366,6 +366,7 @@ OPTIONS
              BUFFER_OVERRUN_L5 (disabled by default),
              BUFFER_OVERRUN_R2 (enabled by default),
              BUFFER_OVERRUN_S2 (enabled by default),
+             BUFFER_OVERRUN_T1 (enabled by default),
              BUFFER_OVERRUN_U5 (disabled by default),
              Bad_footprint (enabled by default),
              CAPTURED_STRONG_SELF (enabled by default),
@@ -440,6 +441,7 @@ OPTIONS
              INFERBO_ALLOC_IS_ZERO (enabled by default),
              INFERBO_ALLOC_MAY_BE_BIG (enabled by default),
              INFERBO_ALLOC_MAY_BE_NEGATIVE (enabled by default),
+             INFERBO_ALLOC_MAY_BE_TAINTED (enabled by default),
              INFINITE_ALLOCATION (disabled by default),
              INFINITE_EXECUTION_TIME (disabled by default),
              INHERENTLY_DANGEROUS_FUNCTION (enabled by default),

infer/man/man1/infer-report.txt

@@ -95,6 +95,7 @@ OPTIONS
              BUFFER_OVERRUN_L5 (disabled by default),
              BUFFER_OVERRUN_R2 (enabled by default),
              BUFFER_OVERRUN_S2 (enabled by default),
+             BUFFER_OVERRUN_T1 (enabled by default),
              BUFFER_OVERRUN_U5 (disabled by default),
              Bad_footprint (enabled by default),
              CAPTURED_STRONG_SELF (enabled by default),
@@ -169,6 +170,7 @@ OPTIONS
              INFERBO_ALLOC_IS_ZERO (enabled by default),
              INFERBO_ALLOC_MAY_BE_BIG (enabled by default),
              INFERBO_ALLOC_MAY_BE_NEGATIVE (enabled by default),
+             INFERBO_ALLOC_MAY_BE_TAINTED (enabled by default),
              INFINITE_ALLOCATION (disabled by default),
              INFINITE_EXECUTION_TIME (disabled by default),
              INHERENTLY_DANGEROUS_FUNCTION (enabled by default),

infer/man/man1/infer.txt

@@ -366,6 +366,7 @@ OPTIONS
              BUFFER_OVERRUN_L5 (disabled by default),
              BUFFER_OVERRUN_R2 (enabled by default),
              BUFFER_OVERRUN_S2 (enabled by default),
+             BUFFER_OVERRUN_T1 (enabled by default),
              BUFFER_OVERRUN_U5 (disabled by default),
              Bad_footprint (enabled by default),
              CAPTURED_STRONG_SELF (enabled by default),
@@ -440,6 +441,7 @@ OPTIONS
              INFERBO_ALLOC_IS_ZERO (enabled by default),
              INFERBO_ALLOC_MAY_BE_BIG (enabled by default),
              INFERBO_ALLOC_MAY_BE_NEGATIVE (enabled by default),
+             INFERBO_ALLOC_MAY_BE_TAINTED (enabled by default),
              INFINITE_ALLOCATION (disabled by default),
              INFINITE_EXECUTION_TIME (disabled by default),
              INHERENTLY_DANGEROUS_FUNCTION (enabled by default),

infer/src/base/IssueType.ml

@@ -137,6 +137,8 @@ let buffer_overrun_r2 = register_from_string "BUFFER_OVERRUN_R2"
 
 let buffer_overrun_s2 = register_from_string "BUFFER_OVERRUN_S2"
 
+let buffer_overrun_t1 = register_from_string "BUFFER_OVERRUN_T1"
+
 let buffer_overrun_u5 = register_from_string ~enabled:false "BUFFER_OVERRUN_U5"
 
 let cannot_star = register_from_string "Cannot_star"
@@ -318,6 +320,8 @@ let inferbo_alloc_may_be_big = register_from_string "INFERBO_ALLOC_MAY_BE_BIG"
 
 let inferbo_alloc_may_be_negative = register_from_string "INFERBO_ALLOC_MAY_BE_NEGATIVE"
 
+let inferbo_alloc_may_be_tainted = register_from_string "INFERBO_ALLOC_MAY_BE_TAINTED"
+
 let infinite_cost_call ~kind = register_from_cost_string ~enabled:false "INFINITE_%s" ~kind
 
 let inherently_dangerous_function = register_from_string "INHERENTLY_DANGEROUS_FUNCTION"

infer/src/base/IssueType.mli

@@ -66,6 +66,9 @@ val buffer_overrun_r2 : t
 
 val buffer_overrun_s2 : t
 
+val buffer_overrun_t1 : t
+(** Tainted values is used in array accesses, causing buffer over/underruns *)
+
 val buffer_overrun_u5 : t
 
 val cannot_star : t
@@ -191,6 +194,8 @@ val inferbo_alloc_may_be_big : t
 
 val inferbo_alloc_may_be_negative : t
 
+val inferbo_alloc_may_be_tainted : t
+
 val infinite_cost_call : kind:CostKind.t -> t
 
 val inherently_dangerous_function : t

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -89,15 +89,21 @@ end
 module type TaintS = sig
   include AbstractDomain.WithBottom
 
+  val compare : t -> t -> int
+
   val pp : F.formatter -> t -> unit
 
   val of_bool : bool -> t
+
+  val is_tainted : t -> bool
 end
 
 module Taint = struct
   module Unit = struct
     include AbstractDomain.Empty
 
+    let compare _ _ = 0
+
     let bottom = ()
 
     let is_bottom _ = true
@@ -105,14 +111,20 @@ module Taint = struct
     let pp _ _ = ()
 
     let of_bool _ = ()
+
+    let is_tainted _ = false
   end
 
   module ServiceHandlerRequest = struct
     include AbstractDomain.BooleanOr
 
+    let compare = Bool.compare
+
     let pp fmt taint = if taint then F.fprintf fmt "(tainted)"
 
     let of_bool x = x
+
+    let is_tainted x = x
   end
 
   include ( val if Config.bo_service_handler_request then (module ServiceHandlerRequest)
@@ -234,6 +246,8 @@ module Val = struct
 
   let get_all_locs : t -> PowLoc.t = fun x -> PowLoc.join x.powloc (get_array_locs x)
 
+  let get_taint : t -> Taint.t = fun x -> x.taint
+
   let get_traces : t -> TraceSet.t = fun x -> x.traces
 
   let of_itv ?(traces = TraceSet.bottom) ?(taint = Taint.bottom) itv = {bot with itv; taint; traces}

infer/src/bufferoverrun/bufferOverrunDomain.mli

@@ -42,9 +42,13 @@ end
 module type TaintS = sig
   include AbstractDomain.WithBottom
 
+  val compare : t -> t -> int
+
   val pp : Format.formatter -> t -> unit
 
   val of_bool : bool -> t
+
+  val is_tainted : t -> bool
 end
 
 module Taint : TaintS
@@ -121,6 +125,8 @@ module Val : sig
 
   val get_pow_loc : t -> AbsLoc.PowLoc.t
 
+  val get_taint : t -> Taint.t
+
   val get_traces : t -> BufferOverrunTrace.Set.t
 
   val set_array_length : Location.t -> length:t -> t -> t

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -82,9 +82,11 @@ let check_alloc_size ~can_be_zero size_exp {location; integer_type_widths} mem c
   | Bottom ->
       cond_set
   | NonBottom length ->
+      let taint = Dom.Val.get_taint v_length in
       let traces = Dom.Val.get_traces v_length in
       let latest_prune = Dom.Mem.get_latest_prune mem in
-      PO.ConditionSet.add_alloc_size location ~can_be_zero ~length traces latest_prune cond_set
+      PO.ConditionSet.add_alloc_size location ~can_be_zero ~length ~taint traces latest_prune
+        cond_set
 
 
 let fgets str_exp num_exp =

infer/src/bufferoverrun/bufferOverrunProofObligations.ml

@@ -95,12 +95,16 @@ module ConditionTrace = struct
   let for_summary : _ t0 -> summary_t = fun ct -> {ct with cond_trace= ()}
 end
 
-type report_issue_type = NotIssue | Issue of IssueType.t | SymbolicIssue
+type report_issue_type =
+  | NotIssue
+  | Issue of IssueType.t
+  | SymbolicIssue
+  | TaintedIssue of IssueType.t
 
 type checked_condition = {report_issue_type: report_issue_type; propagate: bool}
 
 module AllocSizeCondition = struct
-  type t = {length: ItvPure.t; can_be_zero: bool} [@@deriving compare]
+  type t = {length: ItvPure.t; can_be_zero: bool; taint: Dom.Taint.t} [@@deriving compare]
 
   let get_symbols {length} = ItvPure.get_symbols length
 
@@ -110,8 +114,8 @@ module AllocSizeCondition = struct
     F.fprintf fmt "Length: %a" (ItvPure.pp_mark ~markup) length
 
 
-  let make ~can_be_zero ~length =
-    if ItvPure.is_invalid length then None else Some {length; can_be_zero}
+  let make ~can_be_zero ~length ~taint =
+    if ItvPure.is_invalid length then None else Some {length; can_be_zero; taint}
 
 
   let have_similar_bounds x y =
@@ -151,50 +155,59 @@ module AllocSizeCondition = struct
 
   let itv_big = ItvPure.of_int 1_000_000
 
-  let check {length; can_be_zero} =
-    match ItvPure.xcompare ~lhs:length ~rhs:ItvPure.zero with
-    | `Equal | `RightSubsumesLeft ->
-        if can_be_zero then {report_issue_type= NotIssue; propagate= false}
-        else {report_issue_type= Issue IssueType.inferbo_alloc_is_zero; propagate= false}
-    | `LeftSmallerThanRight ->
-        {report_issue_type= Issue IssueType.inferbo_alloc_is_negative; propagate= false}
-    | _ -> (
-        let is_symbolic = ItvPure.is_symbolic length in
-        match ItvPure.xcompare ~lhs:length ~rhs:ItvPure.mone with
-        | `Equal | `LeftSmallerThanRight | `RightSubsumesLeft ->
-            {report_issue_type= Issue IssueType.inferbo_alloc_is_negative; propagate= false}
-        | `LeftSubsumesRight when Bound.is_not_infty (ItvPure.lb length) ->
-            { report_issue_type= Issue IssueType.inferbo_alloc_may_be_negative
-            ; propagate= is_symbolic }
-        | cmp_mone -> (
-          match ItvPure.xcompare ~lhs:length ~rhs:itv_big with
-          | `Equal | `RightSmallerThanLeft | `RightSubsumesLeft ->
-              {report_issue_type= Issue IssueType.inferbo_alloc_is_big; propagate= false}
-          | `LeftSubsumesRight when Bound.is_not_infty (ItvPure.ub length) ->
-              {report_issue_type= Issue IssueType.inferbo_alloc_may_be_big; propagate= is_symbolic}
-          | cmp_big ->
-              let propagate =
-                match (cmp_mone, cmp_big) with
-                | (`NotComparable | `LeftSubsumesRight), _ | _, (`NotComparable | `LeftSubsumesRight)
-                  ->
-                    is_symbolic
-                | _ ->
-                    false
-              in
-              if propagate then {report_issue_type= SymbolicIssue; propagate}
-              else {report_issue_type= NotIssue; propagate} ) )
-
-
-  let subst eval_sym {length; can_be_zero} =
+  let check {length; can_be_zero; taint} =
+    if Config.bo_service_handler_request && Dom.Taint.is_tainted taint then
+      {report_issue_type= TaintedIssue IssueType.inferbo_alloc_may_be_tainted; propagate= false}
+    else
+      match ItvPure.xcompare ~lhs:length ~rhs:ItvPure.zero with
+      | `Equal | `RightSubsumesLeft ->
+          if can_be_zero then {report_issue_type= NotIssue; propagate= false}
+          else {report_issue_type= Issue IssueType.inferbo_alloc_is_zero; propagate= false}
+      | `LeftSmallerThanRight ->
+          {report_issue_type= Issue IssueType.inferbo_alloc_is_negative; propagate= false}
+      | _ -> (
+          let is_symbolic = ItvPure.is_symbolic length in
+          match ItvPure.xcompare ~lhs:length ~rhs:ItvPure.mone with
+          | `Equal | `LeftSmallerThanRight | `RightSubsumesLeft ->
+              {report_issue_type= Issue IssueType.inferbo_alloc_is_negative; propagate= false}
+          | `LeftSubsumesRight when Bound.is_not_infty (ItvPure.lb length) ->
+              { report_issue_type= Issue IssueType.inferbo_alloc_may_be_negative
+              ; propagate= is_symbolic }
+          | cmp_mone -> (
+            match ItvPure.xcompare ~lhs:length ~rhs:itv_big with
+            | `Equal | `RightSmallerThanLeft | `RightSubsumesLeft ->
+                {report_issue_type= Issue IssueType.inferbo_alloc_is_big; propagate= false}
+            | `LeftSubsumesRight when Bound.is_not_infty (ItvPure.ub length) ->
+                {report_issue_type= Issue IssueType.inferbo_alloc_may_be_big; propagate= is_symbolic}
+            | cmp_big ->
+                let propagate =
+                  match (cmp_mone, cmp_big) with
+                  | (`NotComparable | `LeftSubsumesRight), _
+                  | _, (`NotComparable | `LeftSubsumesRight) ->
+                      is_symbolic
+                  | _ ->
+                      false
+                in
+                if propagate then {report_issue_type= SymbolicIssue; propagate}
+                else {report_issue_type= NotIssue; propagate} ) )
+
+
+  let subst eval_sym {length; can_be_zero; taint} =
     match ItvPure.subst length eval_sym with
     | NonBottom length ->
-        Some {length; can_be_zero}
+        Some {length; can_be_zero; taint}
     | Bottom ->
         None
 end
 
 module ArrayAccessCondition = struct
-  type t = {offset: ItvPure.t; idx: ItvPure.t; size: ItvPure.t; last_included: bool; void_ptr: bool}
+  type t =
+    { offset: ItvPure.t
+    ; idx: ItvPure.t
+    ; size: ItvPure.t
+    ; last_included: bool
+    ; void_ptr: bool
+    ; taint: Dom.Taint.t }
   [@@deriving compare]
 
   let get_symbols c =
@@ -227,12 +240,18 @@ module ArrayAccessCondition = struct
       pp_offset (ItvPure.pp_mark ~markup) (ItvPure.make_positive c.size)
 
 
-  let make : offset:ItvPure.t -> idx:ItvPure.t -> size:ItvPure.t -> last_included:bool -> t option =
-   fun ~offset ~idx ~size ~last_included ->
+  let make :
+         offset:ItvPure.t
+      -> idx:ItvPure.t
+      -> size:ItvPure.t
+      -> last_included:bool
+      -> taint:Dom.Taint.t
+      -> t option =
+   fun ~offset ~idx ~size ~last_included ~taint ->
     if ItvPure.is_invalid offset || ItvPure.is_invalid idx || ItvPure.is_invalid size then None
     else
       let void_ptr = ItvPure.has_void_ptr_symb offset || ItvPure.has_void_ptr_symb size in
-      Some {offset; idx; size; last_included; void_ptr}
+      Some {offset; idx; size; last_included; void_ptr; taint}
 
 
   let have_similar_bounds {offset= loff; idx= lidx; size= lsiz; last_included= lcol}
@@ -350,6 +369,9 @@ module ArrayAccessCondition = struct
     (* il >= 0 and iu < sl, definitely not an error *)
     if Boolean.is_true not_overrun && Boolean.is_true not_underrun then
       {report_issue_type= NotIssue; propagate= false} (* iu < 0 or il >= su, definitely an error *)
+    else if Config.bo_service_handler_request && Dom.Taint.is_tainted c.taint then
+      {report_issue_type= Issue IssueType.buffer_overrun_t1; propagate= false}
+      (* tainted values are used in array accesses *)
     else if Boolean.is_false not_overrun || Boolean.is_false not_underrun then
       {report_issue_type= Issue IssueType.buffer_overrun_l1; propagate= false}
       (* su <= iu < +oo, most probably an error *)
@@ -764,7 +786,7 @@ module ConditionWithTrace = struct
   let check cwt =
     let ({report_issue_type; propagate} as checked) = Condition.check cwt.cond cwt.trace in
     match report_issue_type with
-    | NotIssue | SymbolicIssue ->
+    | NotIssue | SymbolicIssue | TaintedIssue _ ->
         checked
     | Issue issue_type ->
         let issue_type = set_u5 cwt issue_type in
@@ -785,7 +807,7 @@ module ConditionWithTrace = struct
     match checked.report_issue_type with
     | NotIssue | SymbolicIssue ->
         ()
-    | Issue issue_type ->
+    | TaintedIssue issue_type | Issue issue_type ->
         report cwt.cond cwt.trace issue_type
 
 
@@ -797,7 +819,7 @@ module ConditionWithTrace = struct
           match report_issue_type with
           | NotIssue ->
               assert false
-          | SymbolicIssue ->
+          | SymbolicIssue | TaintedIssue _ ->
               reported
           | Issue issue_type ->
               Some (Reported.make issue_type)
@@ -880,17 +902,17 @@ module ConditionSet = struct
         join_one condset (check_one cwt)
 
 
-  let add_array_access location ~offset ~idx ~size ~last_included ~idx_traces ~arr_traces
+  let add_array_access location ~offset ~idx ~size ~last_included ~taint ~idx_traces ~arr_traces
       ~latest_prune condset =
-    ArrayAccessCondition.make ~offset ~idx ~size ~last_included
+    ArrayAccessCondition.make ~offset ~idx ~size ~last_included ~taint
     |> Condition.make_array_access
     |> add_opt location
          (ValTrace.Issue.(binary location ArrayAccess) idx_traces arr_traces)
          latest_prune condset
 
 
-  let add_alloc_size location ~can_be_zero ~length val_traces latest_prune condset =
-    AllocSizeCondition.make ~can_be_zero ~length
+  let add_alloc_size location ~can_be_zero ~length ~taint val_traces latest_prune condset =
+    AllocSizeCondition.make ~can_be_zero ~length ~taint
     |> Condition.make_alloc_size
     |> add_opt location (ValTrace.Issue.alloc location val_traces) latest_prune condset
 

infer/src/bufferoverrun/bufferOverrunProofObligations.mli

@@ -38,6 +38,7 @@ module ConditionSet : sig
     -> idx:ItvPure.t
     -> size:ItvPure.t
     -> last_included:bool
+    -> taint:BufferOverrunDomain.Taint.t
     -> idx_traces:BufferOverrunTrace.Set.t
     -> arr_traces:BufferOverrunTrace.Set.t
     -> latest_prune:BufferOverrunDomain.LatestPrune.t
@@ -48,6 +49,7 @@ module ConditionSet : sig
        Location.t
     -> can_be_zero:bool
     -> length:ItvPure.t
+    -> taint:BufferOverrunDomain.Taint.t
     -> BufferOverrunTrace.Set.t
     -> BufferOverrunDomain.LatestPrune.t
     -> checked_t

infer/src/bufferoverrun/bufferOverrunUtils.ml

@@ -235,11 +235,11 @@ module Exec = struct
 end
 
 module Check = struct
-  let check_access ~size ~idx ~offset ~arr_traces ~idx_traces ~last_included ~latest_prune location
-      cond_set =
+  let check_access ~size ~idx ~offset ~arr_traces ~idx_traces ~last_included ~taint ~latest_prune
+      location cond_set =
     match (size, idx) with
     | NonBottom length, NonBottom idx ->
-        PO.ConditionSet.add_array_access location ~size:length ~offset ~idx ~last_included
+        PO.ConditionSet.add_array_access location ~size:length ~offset ~idx ~last_included ~taint
           ~idx_traces ~arr_traces ~latest_prune cond_set
     | _ ->
         cond_set
@@ -260,7 +260,10 @@ module Check = struct
         offset
 
 
+  let get_taint arr idx = Dom.Taint.join (Dom.Val.get_taint arr) (Dom.Val.get_taint idx)
+
   let array_access ~arr ~idx ~is_plus ~last_included ~latest_prune location cond_set =
+    let taint = get_taint arr idx in
     let idx_traces = Dom.Val.get_traces idx in
     let idx =
       let idx_itv = Dom.Val.get_itv idx in
@@ -271,8 +274,8 @@ module Check = struct
       let size = ArrayBlk.ArrInfo.get_size arr_info in
       let offset = offsetof arr_info in
       log_array_access allocsite size offset idx ;
-      check_access ~size ~idx ~offset ~arr_traces ~idx_traces ~last_included ~latest_prune location
-        acc
+      check_access ~size ~idx ~offset ~arr_traces ~idx_traces ~last_included ~taint ~latest_prune
+        location acc
     in
     ArrayBlk.fold array_access1 (Dom.Val.get_array_blk arr) cond_set
 
@@ -290,6 +293,7 @@ module Check = struct
 
 
   let array_access_byte ~arr ~idx ~is_plus ~last_included ~latest_prune location cond_set =
+    let taint = get_taint arr idx in
     let idx_traces = Dom.Val.get_traces idx in
     let idx =
       let idx_itv = Dom.Val.get_itv idx in
@@ -300,8 +304,8 @@ module Check = struct
       let size = ArrayBlk.ArrInfo.byte_size arr_info in
       let offset = offsetof arr_info in
       log_array_access allocsite size offset idx ;
-      check_access ~size ~idx ~offset ~arr_traces ~idx_traces ~last_included ~latest_prune location
-        acc
+      check_access ~size ~idx ~offset ~arr_traces ~idx_traces ~last_included ~taint ~latest_prune
+        location acc
     in
     ArrayBlk.fold array_access_byte1 (Dom.Val.get_array_blk arr) cond_set