From f6123cfac1435e748d601b321df75b1bef95b760 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Fri, 7 Feb 2020 06:19:42 -0800 Subject: [PATCH] [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 --- .../src/bufferoverrun/bufferOverrunDomain.ml | 120 +++++++++++++++--- .../src/bufferoverrun/bufferOverrunDomain.mli | 23 ++-- .../bufferOverrunProofObligations.ml | 28 ++-- .../bufferoverrun/bufferOverrunSemantics.ml | 7 +- infer/src/bufferoverrun/symb.ml | 6 + infer/src/bufferoverrun/symb.mli | 2 + 6 files changed, 146 insertions(+), 40 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index b6e8d1e68..93627a9fc 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/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 compare = Bool.compare + 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 pp fmt taint = if taint then F.fprintf fmt "(tainted)" - let of_bool x = x + 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 is_tainted x = x + + 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 param_of_path path = Param (SPathSet.singleton path) + + 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 diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.mli b/infer/src/bufferoverrun/bufferOverrunDomain.mli index fc9a24f59..df5c3e9b9 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.mli +++ b/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 *) diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml index 0b259baf0..d6aad56b2 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml +++ b/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 -> diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 6243e10d3..ca33eab7e 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/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 = diff --git a/infer/src/bufferoverrun/symb.ml b/infer/src/bufferoverrun/symb.ml index ea5fb4429..08f0bbf07 100644 --- a/infer/src/bufferoverrun/symb.ml +++ b/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) diff --git a/infer/src/bufferoverrun/symb.mli b/infer/src/bufferoverrun/symb.mli index d95b3559e..956db58bf 100644 --- a/infer/src/bufferoverrun/symb.mli +++ b/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