[inferbo] Make taint analysis inter-procedural

Summary: This diff makes the taint analysis in Inferbo inter-procedural: adding symbolic taint values and substitute them at function call statements.

Reviewed By: ezgicicek

Differential Revision: D19411022

fbshipit-source-id: 4ff9a590a

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -14,15 +14,11 @@ module F = Format
 module L = Logging
 module OndemandEnv = BufferOverrunOndemandEnv
 module SPath = Symb.SymbolPath
+module SPathSet = Symb.SymbolPathSet
 module Trace = BufferOverrunTrace
 module TraceSet = Trace.Set
 module LoopHeadLoc = Location
 
-type eval_sym_trace =
-  { eval_sym: Bounds.Bound.eval_sym
-  ; trace_of_sym: Symb.Symbol.t -> Trace.Set.t
-  ; eval_locpath: PowLoc.eval_locpath }
-
 module ItvThresholds = AbstractDomain.FiniteSet (struct
   include Z
 
@@ -93,9 +89,15 @@ module type TaintS = sig
 
   val pp : F.formatter -> t -> unit
 
-  val of_bool : bool -> t
-
   val is_tainted : t -> bool
+
+  val param_of_path : SPath.partial -> t
+
+  val tainted_of_path : SPath.partial -> t
+
+  type eval_taint = SPath.partial -> t
+
+  val subst : t -> eval_taint -> t
 end
 
 module Taint = struct
@@ -110,27 +112,99 @@ module Taint = struct
 
     let pp _ _ = ()
 
-    let of_bool _ = ()
-
     let is_tainted _ = false
+
+    let param_of_path _ = ()
+
+    let tainted_of_path _ = ()
+
+    type eval_taint = SPath.partial -> t
+
+    let subst _ _ = ()
   end
 
   module ServiceHandlerRequest = struct
-    include AbstractDomain.BooleanOr
+    type t =
+      | Param of SPathSet.t
+      | Tainted of SPathSet.t (* The path set of [Tainted] should be non-empty. *)
+    [@@deriving compare]
+
+    let pp f = function
+      | Param params ->
+          if SPathSet.is_empty params then F.pp_print_string f "not tainted"
+          else F.fprintf f "unknown taint from %a" SPathSet.pp params
+      | Tainted params ->
+          assert (not (SPathSet.is_empty params)) ;
+          F.fprintf f "tainted by %a" SPathSet.pp params
+
+
+    let leq ~lhs ~rhs =
+      match (lhs, rhs) with
+      | Param _, Tainted _ ->
+          true
+      | Tainted _, Param _ ->
+          false
+      | Param params1, Param params2 | Tainted params1, Tainted params2 ->
+          SPathSet.subset params1 params2
+
 
-    let compare = Bool.compare
+    let join x y =
+      match (x, y) with
+      | Param _, Tainted _ ->
+          y
+      | Tainted _, Param _ ->
+          x
+      | Param params1, Param params2 ->
+          Param (SPathSet.union params1 params2)
+      | Tainted params1, Tainted params2 ->
+          Tainted (SPathSet.union params1 params2)
+
+
+    let widen ~prev ~next ~num_iters:_ = join prev next
+
+    let bottom = Param SPathSet.empty
+
+    let is_bottom = function
+      | Param paths ->
+          SPathSet.is_empty paths
+      | Tainted paths ->
+          assert (not (SPathSet.is_empty paths)) ;
+          false
+
+
+    let is_tainted = function
+      | Tainted paths ->
+          assert (not (SPathSet.is_empty paths)) ;
+          true
+      | _ ->
+          false
 
-    let pp fmt taint = if taint then F.fprintf fmt "(tainted)"
 
-    let of_bool x = x
+    let param_of_path path = Param (SPathSet.singleton path)
 
-    let is_tainted x = x
+    let tainted_of_path path = Tainted (SPathSet.singleton path)
+
+    type eval_taint = SPath.partial -> t
+
+    let subst x eval_taint =
+      match x with
+      | Tainted _ ->
+          x
+      | Param params ->
+          let accum_subst path acc = join acc (eval_taint path) in
+          SPathSet.fold accum_subst params bottom
   end
 
   include ( val if Config.bo_service_handler_request then (module ServiceHandlerRequest)
                 else (module Unit) : TaintS )
 end
 
+type eval_sym_trace =
+  { eval_sym: Bounds.Bound.eval_sym
+  ; trace_of_sym: Symb.Symbol.t -> Trace.Set.t
+  ; eval_locpath: PowLoc.eval_locpath
+  ; eval_taint: Taint.eval_taint }
+
 module Val = struct
   type t =
     { itv: Itv.t
@@ -165,11 +239,15 @@ module Val = struct
       if not (ModeledRange.is_bottom range) then
         F.fprintf fmt " (modeled_range:%a)" ModeledRange.pp range
     in
+    let taint_pp fmt taint =
+      if Config.bo_service_handler_request && Config.bo_debug >= 3 then
+        F.fprintf fmt "(%a)" Taint.pp taint
+    in
     let trace_pp fmt traces =
       if Config.bo_debug >= 3 then F.fprintf fmt ", %a" TraceSet.pp traces
     in
     F.fprintf fmt "(%a%a%a%a%a, %a, %a%a)" Itv.pp x.itv itv_thresholds_pp x.itv_thresholds
-      itv_updated_by_pp x.itv_updated_by modeled_range_pp x.modeled_range Taint.pp x.taint PowLoc.pp
+      itv_updated_by_pp x.itv_updated_by modeled_range_pp x.modeled_range taint_pp x.taint PowLoc.pp
       x.powloc ArrayBlk.pp x.arrayblk trace_pp x.traces
 
 
@@ -500,7 +578,7 @@ module Val = struct
 
 
   let subst : t -> eval_sym_trace -> Location.t -> t =
-   fun x {eval_sym; trace_of_sym; eval_locpath} location ->
+   fun x {eval_sym; trace_of_sym; eval_locpath; eval_taint} location ->
     let symbols = get_symbols x in
     let traces_caller =
       Itv.SymbolSet.fold
@@ -512,6 +590,7 @@ module Val = struct
     let powloc_from_arrayblk, arrayblk = ArrayBlk.subst x.arrayblk eval_sym eval_locpath in
     { x with
       itv= Itv.subst x.itv eval_sym
+    ; taint= Taint.subst x.taint eval_taint
     ; powloc= PowLoc.join powloc powloc_from_arrayblk
     ; arrayblk
     ; traces }
@@ -586,9 +665,10 @@ module Val = struct
       (if may_last_field then ", may_last_field" else "")
       (if is_java then ", is_java" else "") ;
     let taint =
-      Taint.of_bool
-        ( Config.bo_service_handler_request && (not is_java) && Lazy.force_val is_service_handler
-        && SPath.is_request path )
+      if (not Config.bo_service_handler_request) || is_java then Taint.bottom
+      else if Lazy.force_val is_service_handler && SPath.is_request path then
+        Taint.tainted_of_path path
+      else Taint.param_of_path path
     in
     match typ.Typ.desc with
     | Tint (IBool | IChar | ISChar | IUChar) ->
@@ -648,7 +728,7 @@ module Val = struct
           let length = Itv.of_length_path ~is_void:false path in
           of_java_array_alloc allocsite ~length ~traces
       | Some JavaInteger ->
-          itv_val ~non_int:false ~taint:(Taint.of_bool false)
+          itv_val ~non_int:false ~taint:Taint.bottom
       | None ->
           let l = Loc.of_path path in
           let traces = traces_of_loc l in

infer/src/bufferoverrun/bufferOverrunDomain.mli

@@ -8,12 +8,6 @@
 open! IStd
 open AbstractDomain.Types
 
-(** type for on-demand symbol evaluation in Inferbo *)
-type eval_sym_trace =
-  { eval_sym: Bounds.Bound.eval_sym  (** evaluating symbol *)
-  ; trace_of_sym: Symb.Symbol.t -> BufferOverrunTrace.Set.t  (** getting traces of symbol *)
-  ; eval_locpath: AbsLoc.PowLoc.eval_locpath  (** evaluating path *) }
-
 module ItvThresholds : AbstractDomain.FiniteSetS with type elt = Z.t
 (** Set of integers for threshold widening *)
 
@@ -46,13 +40,26 @@ module type TaintS = sig
 
   val pp : Format.formatter -> t -> unit
 
-  val of_bool : bool -> t
-
   val is_tainted : t -> bool
+
+  val param_of_path : Symb.SymbolPath.partial -> t
+
+  val tainted_of_path : Symb.SymbolPath.partial -> t
+
+  type eval_taint = Symb.SymbolPath.partial -> t
+
+  val subst : t -> eval_taint -> t
 end
 
 module Taint : TaintS
 
+(** type for on-demand symbol evaluation in Inferbo *)
+type eval_sym_trace =
+  { eval_sym: Bounds.Bound.eval_sym  (** evaluating symbol *)
+  ; trace_of_sym: Symb.Symbol.t -> BufferOverrunTrace.Set.t  (** getting traces of symbol *)
+  ; eval_locpath: AbsLoc.PowLoc.eval_locpath  (** evaluating path *)
+  ; eval_taint: Taint.eval_taint  (** evaluating taint of path *) }
+
 module Val : sig
   type t =
     { itv: Itv.t  (** Interval *)

infer/src/bufferoverrun/bufferOverrunProofObligations.ml

@@ -108,7 +108,10 @@ module AllocSizeCondition = struct
 
   let get_symbols {length} = ItvPure.get_symbols length
 
-  let pp fmt {length} = F.fprintf fmt "alloc(%a)" ItvPure.pp length
+  let pp fmt {length; taint} =
+    F.fprintf fmt "alloc(%a)" ItvPure.pp length ;
+    if Config.bo_debug >= 3 then F.fprintf fmt "(%a)" Dom.Taint.pp taint
+
 
   let pp_description ~markup fmt {length} =
     F.fprintf fmt "Length: %a" (ItvPure.pp_mark ~markup) length
@@ -192,9 +195,10 @@ module AllocSizeCondition = struct
                 else {report_issue_type= NotIssue; propagate} ) )
 
 
-  let subst eval_sym {length; can_be_zero; taint} =
+  let subst eval_sym eval_taint {length; can_be_zero; taint} =
     match ItvPure.subst length eval_sym with
     | NonBottom length ->
+        let taint = Dom.Taint.subst taint eval_taint in
         Some {length; can_be_zero; taint}
     | Bottom ->
         None
@@ -222,7 +226,8 @@ module ArrayAccessCondition = struct
     in
     let cmp = if c.last_included then "<=" else "<" in
     F.fprintf fmt "%t%a %s %a" pp_offset ItvPure.pp c.idx cmp ItvPure.pp
-      (ItvPure.make_positive c.size)
+      (ItvPure.make_positive c.size) ;
+    if Config.bo_debug >= 3 then F.fprintf fmt "(%a)" Dom.Taint.pp c.taint
 
 
   let pp_description : markup:bool -> F.formatter -> t -> unit =
@@ -396,8 +401,8 @@ module ArrayAccessCondition = struct
       {report_issue_type; propagate= is_symbolic}
 
 
-  let subst : Bound.eval_sym -> t -> t option =
-   fun eval_sym c ->
+  let subst : Bound.eval_sym -> Dom.Taint.eval_taint -> t -> t option =
+   fun eval_sym eval_taint c ->
     match
       (ItvPure.subst c.offset eval_sym, ItvPure.subst c.idx eval_sym, ItvPure.subst c.size eval_sym)
     with
@@ -406,7 +411,8 @@ module ArrayAccessCondition = struct
           c.void_ptr || ItvPure.has_void_ptr_symb offset || ItvPure.has_void_ptr_symb idx
           || ItvPure.has_void_ptr_symb size
         in
-        Some {c with offset; idx; size; void_ptr}
+        let taint = Dom.Taint.subst c.taint eval_taint in
+        Some {c with offset; idx; size; void_ptr; taint}
     | _ ->
         None
 end
@@ -616,11 +622,11 @@ module Condition = struct
         BinaryOperationCondition.get_symbols c
 
 
-  let subst eval_sym = function
+  let subst eval_sym eval_taint = function
     | AllocSize c ->
-        AllocSizeCondition.subst eval_sym c |> make_alloc_size
+        AllocSizeCondition.subst eval_sym eval_taint c |> make_alloc_size
     | ArrayAccess c ->
-        ArrayAccessCondition.subst eval_sym c |> make_array_access
+        ArrayAccessCondition.subst eval_sym eval_taint c |> make_array_access
     | BinaryOperation c ->
         BinaryOperationCondition.subst eval_sym c |> make_binary_operation
 
@@ -746,8 +752,8 @@ module ConditionWithTrace = struct
         call_site
     with
     | `Reachable reachability -> (
-        let {Dom.eval_sym; trace_of_sym} = eval_sym_trace ~mode:Sem.EvalPOCond in
-        match Condition.subst eval_sym cwt.cond with
+        let {Dom.eval_sym; eval_taint; trace_of_sym} = eval_sym_trace ~mode:Sem.EvalPOCond in
+        match Condition.subst eval_sym eval_taint cwt.cond with
         | None ->
             None
         | Some cond ->

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -484,7 +484,12 @@ let mk_eval_sym_trace ?(is_params_ref = false) integer_type_widths
     if Itv.eq itv Itv.bot then TraceSet.bottom else traces
   in
   let eval_locpath ~mode partial = eval_locpath ~mode params partial caller_mem in
-  fun ~mode -> {eval_sym= eval_sym ~mode; trace_of_sym; eval_locpath= eval_locpath ~mode}
+  let eval_taint ~mode path = eval_sympath_partial ~mode params path caller_mem |> Val.get_taint in
+  fun ~mode ->
+    { eval_sym= eval_sym ~mode
+    ; trace_of_sym
+    ; eval_locpath= eval_locpath ~mode
+    ; eval_taint= eval_taint ~mode }
 
 
 let mk_eval_sym_mode ~mode integer_type_widths callee_formals actual_exps caller_mem =

infer/src/bufferoverrun/symb.ml

@@ -414,3 +414,9 @@ module SymbolMap = struct
     | exception Exit ->
         false
 end
+
+module SymbolPathSet = PrettyPrintable.MakePPSet (struct
+  type t = SymbolPath.partial [@@deriving compare]
+
+  let pp = SymbolPath.pp_partial
+end)

infer/src/bufferoverrun/symb.mli

@@ -137,3 +137,5 @@ module SymbolMap : sig
 
   val for_all2 : f:(key -> 'a option -> 'b option -> bool) -> 'a t -> 'b t -> bool
 end
+
+module SymbolPathSet : PrettyPrintable.PPSet with type elt = SymbolPath.partial