diff --git a/Makefile b/Makefile index f91bed029..de830a8ab 100644 --- a/Makefile +++ b/Makefile @@ -74,6 +74,9 @@ DIRECT_TESTS += \ cpp_starvation \ cpp_uninit \ +ifeq ($(IS_FACEBOOK_TREE),yes) +DIRECT_TESTS += cpp_fb-taint +endif ifneq ($(BUCK),no) BUILD_SYSTEMS_TESTS += \ diff --git a/infer/man/man1/infer-analyze.txt b/infer/man/man1/infer-analyze.txt index 2cdf6210e..2624c1bed 100644 --- a/infer/man/man1/infer-analyze.txt +++ b/infer/man/man1/infer-analyze.txt @@ -356,6 +356,11 @@ BUCK OPTIONS BUFFER OVERRUN OPTIONS --bo-debug int Debug level for buffer-overrun checker (0-4) + + --bo-service-handler-request + Activates: [EXPERIMENTAL] Use taint flow of service handler + requests in buffer overflow checking. (Conversely: + --no-bo-service-handler-request) CLANG OPTIONS --annotation-reachability-cxx json Specify annotation reachability analyses to be performed on diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index c0f943d7c..87c093f37 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -129,6 +129,11 @@ OPTIONS --bo-debug int Debug level for buffer-overrun checker (0-4) See also infer-analyze(1). + --bo-service-handler-request + Activates: [EXPERIMENTAL] Use taint flow of service handler + requests in buffer overflow checking. (Conversely: + --no-bo-service-handler-request) See also infer-analyze(1). + --bootclasspath string Specify the Java bootclasspath See also infer-capture(1). diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index de44cc748..026067bdf 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -129,6 +129,11 @@ OPTIONS --bo-debug int Debug level for buffer-overrun checker (0-4) See also infer-analyze(1). + --bo-service-handler-request + Activates: [EXPERIMENTAL] Use taint flow of service handler + requests in buffer overflow checking. (Conversely: + --no-bo-service-handler-request) See also infer-analyze(1). + --bootclasspath string Specify the Java bootclasspath See also infer-capture(1). diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 7759b1a89..f44e541b5 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -1133,6 +1133,7 @@ and custom_symbols = and ( biabduction_models_mode , bo_debug + , bo_service_handler_request , deduplicate , developer_mode , debug @@ -1166,6 +1167,10 @@ and ( biabduction_models_mode CLOpt.mk_int ~default:0 ~long:"bo-debug" ~in_help:InferCommand.[(Analyze, manual_buffer_overrun)] "Debug level for buffer-overrun checker (0-4)" + and bo_service_handler_request = + CLOpt.mk_bool ~long:"bo-service-handler-request" + ~in_help:InferCommand.[(Analyze, manual_buffer_overrun)] + "[EXPERIMENTAL] Use taint flow of service handler requests in buffer overflow checking." and deduplicate = CLOpt.mk_bool ~long:"deduplicate" ~default:true ~in_help: @@ -1288,6 +1293,7 @@ and ( biabduction_models_mode in ( biabduction_models_mode , bo_debug + , bo_service_handler_request , deduplicate , developer_mode , debug @@ -2737,6 +2743,8 @@ and bootclasspath = !bootclasspath and bo_debug = !bo_debug +and bo_service_handler_request = !bo_service_handler_request + and buck = !buck and buck_blacklist = !buck_blacklist diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index a5b560e26..ade54831f 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -229,6 +229,8 @@ val biabduction_models_mode : bool val bo_debug : int +val bo_service_handler_request : bool + val bootclasspath : string option val buck : bool diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 1ecc7f965..4a2de52b4 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -86,12 +86,46 @@ module ModeledRange = struct let of_big_int ~trace z = NonBottom (Bounds.NonNegativeBound.of_big_int ~trace z) end +module type TaintS = sig + include AbstractDomain.WithBottom + + val pp : F.formatter -> t -> unit + + val of_bool : bool -> t +end + +module Taint = struct + module Unit = struct + include AbstractDomain.Empty + + let bottom = () + + let is_bottom _ = true + + let pp _ _ = () + + let of_bool _ = () + end + + module ServiceHandlerRequest = struct + include AbstractDomain.BooleanOr + + let pp fmt taint = if taint then F.fprintf fmt "(tainted)" + + let of_bool x = x + end + + include ( val if Config.bo_service_handler_request then (module ServiceHandlerRequest) + else (module Unit) : TaintS ) +end + module Val = struct type t = { itv: Itv.t ; itv_thresholds: ItvThresholds.t ; itv_updated_by: ItvUpdatedBy.t ; modeled_range: ModeledRange.t + ; taint: Taint.t ; powloc: PowLoc.t ; arrayblk: ArrayBlk.t ; traces: TraceSet.t } @@ -101,6 +135,7 @@ module Val = struct ; itv_thresholds= ItvThresholds.empty ; itv_updated_by= ItvUpdatedBy.bottom ; modeled_range= ModeledRange.bottom + ; taint= Taint.bottom ; powloc= PowLoc.bot ; arrayblk= ArrayBlk.bot ; traces= TraceSet.bottom } @@ -121,9 +156,9 @@ module Val = struct 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)" Itv.pp x.itv itv_thresholds_pp x.itv_thresholds - itv_updated_by_pp x.itv_updated_by modeled_range_pp x.modeled_range PowLoc.pp x.powloc - ArrayBlk.pp x.arrayblk trace_pp x.traces + 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 + x.powloc ArrayBlk.pp x.arrayblk trace_pp x.traces let unknown_from : Typ.t -> callee_pname:_ -> location:_ -> t = @@ -134,6 +169,7 @@ module Val = struct ; itv_thresholds= ItvThresholds.empty ; itv_updated_by= ItvUpdatedBy.Top ; modeled_range= ModeledRange.bottom + ; taint= Taint.bottom ; powloc= (if is_int then PowLoc.bottom else PowLoc.unknown) ; arrayblk= (if is_int then ArrayBlk.bottom else ArrayBlk.unknown) ; traces } @@ -146,6 +182,7 @@ module Val = struct && ItvThresholds.leq ~lhs:lhs.itv_thresholds ~rhs:rhs.itv_thresholds && ItvUpdatedBy.leq ~lhs:lhs.itv_updated_by ~rhs:rhs.itv_updated_by && ModeledRange.leq ~lhs:lhs.modeled_range ~rhs:rhs.modeled_range + && Taint.leq ~lhs:lhs.taint ~rhs:rhs.taint && PowLoc.leq ~lhs:lhs.powloc ~rhs:rhs.powloc && ArrayBlk.leq ~lhs:lhs.arrayblk ~rhs:rhs.arrayblk @@ -163,6 +200,7 @@ module Val = struct ItvUpdatedBy.widen ~prev:prev.itv_updated_by ~next:next.itv_updated_by ~num_iters ; modeled_range= ModeledRange.widen ~prev:prev.modeled_range ~next:next.modeled_range ~num_iters + ; taint= Taint.widen ~prev:prev.taint ~next:next.taint ~num_iters ; powloc= PowLoc.widen ~prev:prev.powloc ~next:next.powloc ~num_iters ; arrayblk= ArrayBlk.widen ~prev:prev.arrayblk ~next:next.arrayblk ~num_iters ; traces= TraceSet.join prev.traces next.traces } @@ -176,6 +214,7 @@ module Val = struct ; itv_thresholds= ItvThresholds.join x.itv_thresholds y.itv_thresholds ; itv_updated_by= ItvUpdatedBy.join x.itv_updated_by y.itv_updated_by ; modeled_range= ModeledRange.join x.modeled_range y.modeled_range + ; taint= Taint.join x.taint y.taint ; powloc= PowLoc.join x.powloc y.powloc ; arrayblk= ArrayBlk.join x.arrayblk y.arrayblk ; traces= TraceSet.join x.traces y.traces } @@ -197,7 +236,7 @@ module Val = struct let get_traces : t -> TraceSet.t = fun x -> x.traces - let of_itv ?(traces = TraceSet.bottom) itv = {bot with itv; traces} + let of_itv ?(traces = TraceSet.bottom) ?(taint = Taint.bottom) itv = {bot with itv; taint; traces} let of_int n = of_itv (Itv.of_int n) @@ -259,6 +298,7 @@ module Val = struct let itv_thresholds = ItvThresholds.join x.itv_thresholds y.itv_thresholds in let itv_updated_by = ItvUpdatedBy.join x.itv_updated_by y.itv_updated_by in let modeled_range = ModeledRange.join x.modeled_range y.modeled_range in + let taint = Taint.join x.taint y.taint in let traces = match f_trace with | Some f_trace -> @@ -272,7 +312,7 @@ module Val = struct | true, true | false, false -> TraceSet.join x.traces y.traces ) in - {bot with itv; itv_thresholds; itv_updated_by; modeled_range; traces} + {bot with itv; itv_thresholds; itv_updated_by; modeled_range; taint; traces} let lift_cmp_itv : (Itv.t -> Itv.t -> Boolean.t) -> Boolean.EqualOrder.t -> t -> t -> t = @@ -510,16 +550,16 @@ module Val = struct let cast typ v = {v with powloc= PowLoc.cast typ v.powloc} - let of_path tenv ~may_last_field integer_type_widths location typ path = + let of_path tenv ~may_last_field ~is_service_handler integer_type_widths location typ path = let traces_of_loc l = let trace = if Loc.is_global l then Trace.Global l else Trace.Parameter l in TraceSet.singleton location trace in - let itv_val ~non_int = + let itv_val ~non_int ~taint = let l = Loc.of_path path in let traces = traces_of_loc l in let unsigned = Typ.is_unsigned_int typ in - of_itv ~traces (Itv.of_normal_path ~unsigned ~non_int path) + of_itv ~traces ~taint (Itv.of_normal_path ~unsigned ~non_int path) in let ptr_to_c_array_alloc deref_path size = let allocsite = Allocsite.make_symbol deref_path in @@ -531,15 +571,20 @@ module Val = struct L.d_printfln_escaped "Val.of_path %a : %a%s%s" SPath.pp_partial path (Typ.pp Pp.text) typ (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 ) + in match typ.Typ.desc with | Tint (IBool | IChar | ISChar | IUChar) -> - let v = itv_val ~non_int:(Language.curr_language_is Java) in + let v = itv_val ~non_int:is_java ~taint in if Language.curr_language_is Java then set_itv_updated_by_unknown v else set_itv_updated_by_addition v | Tfloat _ | Tfun | TVar _ -> - itv_val ~non_int:true |> set_itv_updated_by_unknown + itv_val ~non_int:true ~taint |> set_itv_updated_by_unknown | Tint _ | Tvoid -> - itv_val ~non_int:false |> set_itv_updated_by_addition + itv_val ~non_int:false ~taint |> set_itv_updated_by_addition | Tptr (elt, _) -> if is_java || SPath.is_this path then let deref_kind = @@ -589,7 +634,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 + itv_val ~non_int:false ~taint:(Taint.of_bool false) | None -> let l = Loc.of_path path in let traces = traces_of_loc l in @@ -618,11 +663,14 @@ module Val = struct let on_demand : default:t -> ?typ:Typ.t -> OndemandEnv.t -> Loc.t -> t = - fun ~default ?typ {tenv; typ_of_param_path; may_last_field; entry_location; integer_type_widths} - l -> + fun ~default ?typ + {tenv; typ_of_param_path; may_last_field; entry_location; integer_type_widths; class_name} l -> let do_on_demand path typ = let may_last_field = may_last_field path in - of_path tenv ~may_last_field integer_type_widths entry_location typ path + let is_service_handler = + lazy (Option.exists class_name ~f:(FbPatternMatch.is_subtype_of_fb_service_handler tenv)) + in + of_path tenv ~may_last_field ~is_service_handler integer_type_widths entry_location typ path in match Loc.get_literal_string l with | Some s -> diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.mli b/infer/src/bufferoverrun/bufferOverrunDomain.mli index 21edb555d..aaa5a4f08 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.mli +++ b/infer/src/bufferoverrun/bufferOverrunDomain.mli @@ -39,12 +39,23 @@ module ModeledRange : sig val of_modeled_function : Procname.t -> Location.t -> Bounds.Bound.t -> t end +module type TaintS = sig + include AbstractDomain.WithBottom + + val pp : Format.formatter -> t -> unit + + val of_bool : bool -> t +end + +module Taint : TaintS + module Val : sig type t = { itv: Itv.t (** Interval *) ; itv_thresholds: ItvThresholds.t ; itv_updated_by: ItvUpdatedBy.t ; modeled_range: ModeledRange.t + ; taint: Taint.t ; powloc: AbsLoc.PowLoc.t (** Simple pointers *) ; arrayblk: ArrayBlk.t (** Array blocks *) ; traces: BufferOverrunTrace.Set.t } @@ -73,7 +84,7 @@ module Val : sig val of_int_lit : IntLit.t -> t - val of_itv : ?traces:BufferOverrunTrace.Set.t -> Itv.t -> t + val of_itv : ?traces:BufferOverrunTrace.Set.t -> ?taint:Taint.t -> Itv.t -> t val of_literal_string : Typ.IntegerWidths.t -> string -> t diff --git a/infer/src/bufferoverrun/bufferOverrunOndemandEnv.ml b/infer/src/bufferoverrun/bufferOverrunOndemandEnv.ml index 856a5f7ce..078801011 100644 --- a/infer/src/bufferoverrun/bufferOverrunOndemandEnv.ml +++ b/infer/src/bufferoverrun/bufferOverrunOndemandEnv.ml @@ -15,7 +15,8 @@ type t = ; typ_of_param_path: SPath.partial -> Typ.t option ; may_last_field: SPath.partial -> bool ; entry_location: Location.t - ; integer_type_widths: Typ.IntegerWidths.t } + ; integer_type_widths: Typ.IntegerWidths.t + ; class_name: Typ.name option } let mk pdesc = let formal_typs = @@ -84,4 +85,5 @@ let mk pdesc = true ) in let entry_location = Procdesc.Node.get_loc (Procdesc.get_start_node pdesc) in - {tenv; typ_of_param_path; may_last_field; entry_location; integer_type_widths} + let class_name = Procname.get_class_type_name (Procdesc.get_proc_name pdesc) in + {tenv; typ_of_param_path; may_last_field; entry_location; integer_type_widths; class_name} diff --git a/infer/src/bufferoverrun/bufferOverrunOndemandEnv.mli b/infer/src/bufferoverrun/bufferOverrunOndemandEnv.mli index 5388fb6eb..8d95df3bf 100644 --- a/infer/src/bufferoverrun/bufferOverrunOndemandEnv.mli +++ b/infer/src/bufferoverrun/bufferOverrunOndemandEnv.mli @@ -14,6 +14,7 @@ type t = ; may_last_field: Symb.SymbolPath.partial -> bool (** if the path is a last field of a class in C++ *) ; entry_location: Location.t (** location of entry node *) - ; integer_type_widths: Typ.IntegerWidths.t (** bit sizes of integer types *) } + ; integer_type_widths: Typ.IntegerWidths.t (** bit sizes of integer types *) + ; class_name: Typ.name option (** class name of the procedure being analyzed *) } val mk : Procdesc.t -> Tenv.t -> Typ.IntegerWidths.t -> t diff --git a/infer/src/bufferoverrun/symb.ml b/infer/src/bufferoverrun/symb.ml index 48b1ecc16..ea5fb4429 100644 --- a/infer/src/bufferoverrun/symb.ml +++ b/infer/src/bufferoverrun/symb.ml @@ -122,6 +122,11 @@ module SymbolPath = struct None + let is_request x = + Option.exists (get_pvar x) ~f:(fun pvar -> + String.equal (Pvar.get_simplified_name pvar) "request" ) + + let rec pp_partial_paren ~paren fmt = function | Pvar pvar -> if Config.bo_debug >= 3 then Pvar.pp_value fmt pvar else Pvar.pp_value_non_verbose fmt pvar diff --git a/infer/src/bufferoverrun/symb.mli b/infer/src/bufferoverrun/symb.mli index e21a44ad1..d95b3559e 100644 --- a/infer/src/bufferoverrun/symb.mli +++ b/infer/src/bufferoverrun/symb.mli @@ -69,6 +69,8 @@ module SymbolPath : sig val is_this : partial -> bool + val is_request : partial -> bool + val get_pvar : partial -> Pvar.t option val represents_multiple_values : partial -> bool diff --git a/infer/src/opensource/FbPatternMatch.ml b/infer/src/opensource/FbPatternMatch.ml new file mode 100644 index 000000000..97877ab14 --- /dev/null +++ b/infer/src/opensource/FbPatternMatch.ml @@ -0,0 +1,10 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd + +let is_subtype_of_fb_service_handler _tenv _name = false diff --git a/infer/src/opensource/FbPatternMatch.mli b/infer/src/opensource/FbPatternMatch.mli new file mode 100644 index 000000000..57a64a192 --- /dev/null +++ b/infer/src/opensource/FbPatternMatch.mli @@ -0,0 +1,10 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd + +val is_subtype_of_fb_service_handler : Tenv.t -> Typ.Name.t -> bool diff --git a/infer/tests/codetoanalyze/cpp/fb-taint/Makefile b/infer/tests/codetoanalyze/cpp/fb-taint/Makefile new file mode 100644 index 000000000..b793d168a --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/fb-taint/Makefile @@ -0,0 +1,20 @@ +# Copyright (c) Facebook, Inc. and its affiliates. +# +# This source code is licensed under the MIT license found in the +# LICENSE file in the root directory of this source tree. + +TESTS_DIR = ../../.. + +# see explanations in cpp/errors/Makefile for the custom isystem +CLANG_OPTIONS = -x c++ -std=c++11 -nostdinc++ -isystem$(CLANG_INCLUDES)/c++/v1/ -c +INFER_OPTIONS = --bufferoverrun-only --bo-service-handler-request --ml-buckets cpp --no-filtering \ + --debug-exceptions --project-root $(TESTS_DIR) --report-force-relative-path +INFERPRINT_OPTIONS = --issues-tests + +SOURCES = $(wildcard *.cpp) + +HEADERS = + +include $(TESTS_DIR)/clang.make + +infer-out/report.json: $(MAKEFILE_LIST)