From cf6073a60c19c189fe97b0200312d27b279a875b Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Thu, 6 Feb 2020 08:57:50 -0800 Subject: [PATCH] [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 | 2 + infer/man/man1/infer-report.txt | 2 + infer/man/man1/infer.txt | 2 + infer/src/base/IssueType.ml | 4 + infer/src/base/IssueType.mli | 5 + .../src/bufferoverrun/bufferOverrunDomain.ml | 14 ++ .../src/bufferoverrun/bufferOverrunDomain.mli | 6 + .../src/bufferoverrun/bufferOverrunModels.ml | 4 +- .../bufferOverrunProofObligations.ml | 124 +++++++++++------- .../bufferOverrunProofObligations.mli | 2 + infer/src/bufferoverrun/bufferOverrunUtils.ml | 18 ++- 11 files changed, 124 insertions(+), 59 deletions(-) diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index 87c093f37..b8a473c3a 100644 --- a/infer/man/man1/infer-full.txt +++ b/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), diff --git a/infer/man/man1/infer-report.txt b/infer/man/man1/infer-report.txt index bb2573bb7..cc4d94e17 100644 --- a/infer/man/man1/infer-report.txt +++ b/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), diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index 026067bdf..e071a839d 100644 --- a/infer/man/man1/infer.txt +++ b/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), diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml index 809bdac00..3bb1e20b0 100644 --- a/infer/src/base/IssueType.ml +++ b/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" diff --git a/infer/src/base/IssueType.mli b/infer/src/base/IssueType.mli index b7e06008a..259c99401 100644 --- a/infer/src/base/IssueType.mli +++ b/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 diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 4a2de52b4..b6e8d1e68 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/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} diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.mli b/infer/src/bufferoverrun/bufferOverrunDomain.mli index aaa5a4f08..fc9a24f59 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.mli +++ b/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 diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index a18badeaa..008808a92 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/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 = diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml index e1ff1ba06..0b259baf0 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml +++ b/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 diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.mli b/infer/src/bufferoverrun/bufferOverrunProofObligations.mli index 5324b533f..d326469b5 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.mli +++ b/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 diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index c6a15cd32..d64ca8302 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/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