From 33dab9c32d6c30f8970bc27314447265ad0a6d68 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Mon, 15 Jun 2020 12:29:08 -0700 Subject: [PATCH] [CCBM] Add reporting with examples (3/3) Summary: This diff adds a prototype of a new checker that collects config checkings between markers. Basically, what the checker is doing is a taint analysis. * Taint source: function calls of "marker start" * Taint sink: function calls of config checking * Taint remove: function calls of "marker end" By the taint analysis, the analysis results will say that which taints can reach to the sink. In other words, which marker ID that has been started can reach to the config checks, before marker's ending. I am separating the diff into three steps: (1/3) Add basic abstract semantics (2/3) Add trace information (3/3) Add reporting with test examples Reviewed By: jvillard Differential Revision: D21998170 fbshipit-source-id: e7759f62f --- Makefile | 4 +- infer/man/man1/infer-full.txt | 1 + infer/man/man1/infer-report.txt | 1 + infer/man/man1/infer.txt | 1 + infer/src/base/IssueType.ml | 6 + infer/src/base/IssueType.mli | 2 + .../checkers/ConfigChecksBetweenMarkers.ml | 113 +++++++++++++----- .../java/fb-gk-interaction/Makefile | 13 ++ 8 files changed, 108 insertions(+), 33 deletions(-) create mode 100644 infer/tests/codetoanalyze/java/fb-gk-interaction/Makefile diff --git a/Makefile b/Makefile index 6a5531cfb..837deee00 100644 --- a/Makefile +++ b/Makefile @@ -175,7 +175,9 @@ DIRECT_TESTS += \ java_topl \ ifeq ($(IS_FACEBOOK_TREE),yes) -DIRECT_TESTS += java_fb-performance +DIRECT_TESTS += \ + java_fb-gk-interaction \ + java_fb-performance endif ifneq ($(ANT),no) diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index 0228aace6..bdb5b8a9b 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -400,6 +400,7 @@ OPTIONS COMPONENT_WITH_UNCONVENTIONAL_SUPERCLASS (enabled by default), CONDITION_ALWAYS_FALSE (disabled by default), CONDITION_ALWAYS_TRUE (disabled by default), + CONFIG_CHECKS_BETWEEN_MARKERS (disabled by default), CONSTANT_ADDRESS_DEREFERENCE (disabled by default), CREATE_INTENT_FROM_URI (enabled by default), CROSS_SITE_SCRIPTING (enabled by default), diff --git a/infer/man/man1/infer-report.txt b/infer/man/man1/infer-report.txt index 62ccce1af..6c392af97 100644 --- a/infer/man/man1/infer-report.txt +++ b/infer/man/man1/infer-report.txt @@ -120,6 +120,7 @@ OPTIONS COMPONENT_WITH_UNCONVENTIONAL_SUPERCLASS (enabled by default), CONDITION_ALWAYS_FALSE (disabled by default), CONDITION_ALWAYS_TRUE (disabled by default), + CONFIG_CHECKS_BETWEEN_MARKERS (disabled by default), CONSTANT_ADDRESS_DEREFERENCE (disabled by default), CREATE_INTENT_FROM_URI (enabled by default), CROSS_SITE_SCRIPTING (enabled by default), diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index dba76b4dd..7017e8b8d 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -400,6 +400,7 @@ OPTIONS COMPONENT_WITH_UNCONVENTIONAL_SUPERCLASS (enabled by default), CONDITION_ALWAYS_FALSE (disabled by default), CONDITION_ALWAYS_TRUE (disabled by default), + CONFIG_CHECKS_BETWEEN_MARKERS (disabled by default), CONSTANT_ADDRESS_DEREFERENCE (disabled by default), CREATE_INTENT_FROM_URI (enabled by default), CROSS_SITE_SCRIPTING (enabled by default), diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml index bc15677c4..b234823cb 100644 --- a/infer/src/base/IssueType.ml +++ b/infer/src/base/IssueType.ml @@ -409,6 +409,12 @@ let condition_always_true = ~user_documentation:"A condition expression is **always** evaluated to true." +let config_checks_between_markers = + register_from_string ~enabled:false ~id:"CONFIG_CHECKS_BETWEEN_MARKERS" Advice + ConfigChecksBetweenMarkers + ~user_documentation:"A config checking is done between a marker's start and end" + + let constant_address_dereference = register_from_string ~enabled:false ~id:"CONSTANT_ADDRESS_DEREFERENCE" Warning Pulse ~user_documentation:[%blob "../../documentation/issues/CONSTANT_ADDRESS_DEREFERENCE.md"] diff --git a/infer/src/base/IssueType.mli b/infer/src/base/IssueType.mli index 85e48585f..43b15b6e8 100644 --- a/infer/src/base/IssueType.mli +++ b/infer/src/base/IssueType.mli @@ -152,6 +152,8 @@ val condition_always_false : t val condition_always_true : t +val config_checks_between_markers : t + val constant_address_dereference : t val create_intent_from_uri : t diff --git a/infer/src/checkers/ConfigChecksBetweenMarkers.ml b/infer/src/checkers/ConfigChecksBetweenMarkers.ml index 2e52fe36d..296071c49 100644 --- a/infer/src/checkers/ConfigChecksBetweenMarkers.ml +++ b/infer/src/checkers/ConfigChecksBetweenMarkers.ml @@ -67,12 +67,19 @@ module Trace = struct (** [Trace] is additional information, thus which should not affect analysis operation *) - let leq ~lhs:_ ~rhs:_ = true - let join x _y = x let widen ~prev ~next ~num_iters:_ = join prev next + let make_desc = function + | MarkerStart marker -> + F.asprintf "Marker %a start" IntLit.pp marker + | ConfigCheck gk_switch -> + F.asprintf "Config %a is checked" ConfigName.pp gk_switch + + + let call_desc callee = F.asprintf "Function %a is called" Procname.pp callee + let marker_start marker = MarkerStart marker let config_check config = ConfigCheck config @@ -82,23 +89,41 @@ module Trace = struct let add_call callee location ~from ~callee_trace = Call {callee; location; from; callee_trace} let singleton kind location = add_elem kind location Empty + + let make_err_trace x = + let rec make_err_trace ~depth x acc ~cont = + match x with + | Empty -> + cont acc + | Elem {kind; location; from} -> + let acc = Errlog.make_trace_element depth location (make_desc kind) [] :: acc in + make_err_trace ~depth from acc ~cont + | Call {callee; location; from; callee_trace} -> + make_err_trace ~depth:(depth + 1) callee_trace acc ~cont:(fun acc -> + let acc = Errlog.make_trace_element depth location (call_desc callee) [] :: acc in + make_err_trace ~depth from acc ~cont ) + in + make_err_trace ~depth:0 x [] ~cont:Fn.id end -module TraceWithNothing = struct - type t = {trace: Trace.t} +module Reported = AbstractDomain.BooleanOr - let pp f {trace} = Trace.pp f trace +module TraceWithReported = struct + type t = {trace: Trace.t; reported: Reported.t} - let leq ~lhs ~rhs = Trace.leq ~lhs:lhs.trace ~rhs:rhs.trace + let pp f {trace; reported} = + F.fprintf f "@[@[trace:@ %a@]@\n@[reported:@ %a@]@]" Trace.pp trace Reported.pp reported - let join x y = {trace= Trace.join x.trace y.trace} - let widen ~prev ~next ~num_iters = - {trace= Trace.widen ~prev:prev.trace ~next:next.trace ~num_iters} + let leq ~lhs ~rhs = Reported.leq ~lhs:lhs.reported ~rhs:rhs.reported + + let join x y = if leq ~lhs:x ~rhs:y then y else x + + let widen ~prev ~next ~num_iters:_ = join prev next end module MarkerSet = struct - include AbstractDomain.Map (IntLit) (TraceWithNothing) + include AbstractDomain.Map (IntLit) (TraceWithReported) let pp f x = if is_empty x then F.pp_print_string f "{ }" @@ -114,28 +139,45 @@ module MarkerSet = struct let add_trace new_trace location x = - map (fun {trace} -> {trace= Trace.add_elem new_trace location trace}) x + map + (fun ({trace} as trace_with_reported) -> + {trace_with_reported with trace= Trace.add_elem new_trace location trace} ) + x let join_on_call callee_pname ?config_check_trace location ~callee ~caller = merge (fun _marker callee_trace caller_trace -> - let add_call {TraceWithNothing.trace= callee_trace} = - let from = - Option.value_map caller_trace ~default:Trace.Empty ~f:(fun {TraceWithNothing.trace} -> - trace ) + let add_call {TraceWithReported.trace= callee_trace; reported= callee_reported} = + let from, caller_reported = + Option.value_map caller_trace ~default:(Trace.Empty, false) + ~f:(fun {TraceWithReported.trace; reported} -> (trace, reported)) in let trace = Trace.add_call callee_pname location ~from ~callee_trace in - Some {TraceWithNothing.trace} + Some {TraceWithReported.trace; reported= Reported.join callee_reported caller_reported} in match (callee_trace, config_check_trace) with | None, None -> caller_trace | None, Some config_check_trace -> - add_call {TraceWithNothing.trace= config_check_trace} + add_call {TraceWithReported.trace= config_check_trace; reported= false} | Some callee_trace, _ -> add_call callee_trace ) callee caller + + + let report {InterproceduralAnalysis.proc_desc; err_log} config location markers = + let report_on_marker marker ({TraceWithReported.trace; reported} as trace_reported) = + if reported then trace_reported + else + let desc = + F.asprintf "Config %a is checked inside marker %a" ConfigName.pp config IntLit.pp marker + in + Reporting.log_issue proc_desc err_log ~loc:location ~ltr:(Trace.make_err_trace trace) + ConfigChecksBetweenMarkers IssueType.config_checks_between_markers desc ; + {TraceWithReported.trace; reported= true} + in + mapi report_on_marker markers end module InvMarkerSet = AbstractDomain.InvertedSet (IntLit) @@ -174,8 +216,8 @@ module Context = struct let call_marker_start marker location {started_markers; ended_markers} = let trace = Trace.singleton (Trace.marker_start marker) location in - let trace_dom = {TraceWithNothing.trace} in - { started_markers= MarkerSet.add marker trace_dom started_markers + let trace_with_reported = {TraceWithReported.trace; reported= false} in + { started_markers= MarkerSet.add marker trace_with_reported started_markers ; ended_markers= InvMarkerSet.remove marker ended_markers } @@ -276,11 +318,16 @@ module Dom = struct {astate with context= Context.call_marker_end marker context} - let call_config_check id location ({mem; context; config_checks} as astate) = + let call_config_check analysis_data id location ({mem; context; config_checks} as astate) = match Mem.find_opt id mem with | Some (NonTop config) -> let trace_elem = Trace.config_check config in let context = Context.call_config_check trace_elem location context in + let context = + { context with + started_markers= MarkerSet.report analysis_data config location context.started_markers + } + in let context_with_trace = {ContextWithTrace.context; trace= Trace.singleton trace_elem location} in @@ -290,7 +337,7 @@ module Dom = struct astate - let instantiate_callee ~callee + let instantiate_callee analysis_data ~callee ~callee_summary:{Summary.context= callee_context; config_checks= callee_config_checks} location ({context= caller_context; config_checks= caller_config_checks} as astate) = let context = @@ -303,6 +350,11 @@ module Dom = struct Context.instantiate_callee ~callee_pname:callee ~config_check_trace location ~callee_context ~caller_context in + let context = + { context with + started_markers= + MarkerSet.report analysis_data config location context.started_markers } + in let trace = Trace.add_call callee location ~from:Trace.Empty ~callee_trace:config_check_trace in @@ -315,15 +367,14 @@ module Dom = struct let to_summary {context; config_checks} = {Summary.context; config_checks} end -type analysis_data = {tenv: Tenv.t; get_summary: Procname.t -> Summary.t option} - module TransferFunctions = struct module CFG = ProcCfg.NormalOneInstrPerNode module Domain = Dom - type nonrec analysis_data = analysis_data + type analysis_data = Summary.t InterproceduralAnalysis.t - let exec_instr astate {tenv; get_summary} _node instr = + let exec_instr astate ({InterproceduralAnalysis.tenv; analyze_dependency} as analysis_data) _node + instr = match (instr : Sil.instr) with | Load {id; e= Lfield (Lvar config_class, config_name, _)} when FbGKInteraction.is_config_class config_class -> @@ -336,10 +387,10 @@ module TransferFunctions = struct Dom.call_marker_end marker astate | Call (_, Const (Cfun callee), _ :: (Var id, _) :: _, location, _) when FbGKInteraction.is_config_check tenv callee -> - Dom.call_config_check id location astate + Dom.call_config_check analysis_data id location astate | Call (_, Const (Cfun callee), _, location, _) -> - Option.value_map (get_summary callee) ~default:astate ~f:(fun callee_summary -> - Dom.instantiate_callee ~callee ~callee_summary location astate ) + Option.value_map (analyze_dependency callee) ~default:astate ~f:(fun (_, callee_summary) -> + Dom.instantiate_callee analysis_data ~callee ~callee_summary location astate ) | _ -> astate @@ -350,7 +401,5 @@ end module Analyzer = AbstractInterpreter.MakeWTO (TransferFunctions) -let checker {InterproceduralAnalysis.proc_desc; tenv; analyze_dependency} = - let open IOption.Let_syntax in - let get_summary pname = analyze_dependency pname >>| snd in - Analyzer.compute_post {tenv; get_summary} ~initial:Dom.init proc_desc >>| Dom.to_summary +let checker ({InterproceduralAnalysis.proc_desc} as analysis_data) = + Option.map (Analyzer.compute_post analysis_data ~initial:Dom.init proc_desc) ~f:Dom.to_summary diff --git a/infer/tests/codetoanalyze/java/fb-gk-interaction/Makefile b/infer/tests/codetoanalyze/java/fb-gk-interaction/Makefile new file mode 100644 index 000000000..d2971857e --- /dev/null +++ b/infer/tests/codetoanalyze/java/fb-gk-interaction/Makefile @@ -0,0 +1,13 @@ +# 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 = ../../.. + +INFER_OPTIONS = --config-checks-between-markers-only --debug-exceptions \ + --report-force-relative-path +INFERPRINT_OPTIONS = --issues-tests +SOURCES = $(wildcard *.java) + +include $(TESTS_DIR)/javac.make