From e715d48c12cb55d44c27e01b60bea6a72c7735df Mon Sep 17 00:00:00 2001 From: Julian Sutherland Date: Tue, 11 Sep 2018 09:32:20 -0700 Subject: [PATCH] QuandaryBO Reviewed By: mbouaziz Differential Revision: D9615368 fbshipit-source-id: 56888a18f --- Makefile | 2 +- infer/src/IR/Errlog.ml | 24 +++++++ infer/src/IR/Errlog.mli | 9 +++ infer/src/backend/InferPrint.ml | 6 +- infer/src/base/Config.ml | 7 ++ infer/src/base/Config.mli | 2 + infer/src/base/IssueType.ml | 4 ++ infer/src/base/IssueType.mli | 4 ++ infer/src/checkers/registerCheckers.ml | 6 +- infer/src/quandary/quandaryBO.ml | 71 +++++++++++++++++++ infer/src/quandary/quandaryBO.mli | 10 +++ infer/src/unit/SeverityTests.ml | 8 +-- .../codetoanalyze/cpp/quandaryBO/.inferconfig | 8 +++ .../codetoanalyze/cpp/quandaryBO/Makefile | 19 +++++ .../codetoanalyze/cpp/quandaryBO/issues.exp | 6 ++ .../cpp/quandaryBO/tainted_index.cpp | 26 +++++++ 16 files changed, 204 insertions(+), 8 deletions(-) create mode 100644 infer/src/quandary/quandaryBO.ml create mode 100644 infer/src/quandary/quandaryBO.mli create mode 100644 infer/tests/codetoanalyze/cpp/quandaryBO/.inferconfig create mode 100644 infer/tests/codetoanalyze/cpp/quandaryBO/Makefile create mode 100644 infer/tests/codetoanalyze/cpp/quandaryBO/issues.exp create mode 100644 infer/tests/codetoanalyze/cpp/quandaryBO/tainted_index.cpp diff --git a/Makefile b/Makefile index 764ce8945..e8a243cf3 100644 --- a/Makefile +++ b/Makefile @@ -47,7 +47,7 @@ BUILD_SYSTEMS_TESTS += \ DIRECT_TESTS += \ c_biabduction c_bufferoverrun c_errors c_frontend c_performance c_uninit \ - cpp_bufferoverrun cpp_errors cpp_frontend cpp_liveness cpp_ownership cpp_quandary \ + cpp_bufferoverrun cpp_errors cpp_frontend cpp_liveness cpp_ownership cpp_quandary cpp_quandaryBO \ cpp_racerd cpp_siof cpp_uninit cpp_nullable cpp_conflicts cpp_linters-for-test-only \ ifneq ($(BUCK),no) diff --git a/infer/src/IR/Errlog.ml b/infer/src/IR/Errlog.ml index a70d93e7e..92d0c3d38 100644 --- a/infer/src/IR/Errlog.ml +++ b/infer/src/IR/Errlog.ml @@ -68,6 +68,15 @@ type node = type err_key = {severity: Exceptions.severity; err_name: IssueType.t; err_desc: Localise.error_desc} [@@deriving compare] +let merge_err_key err_key1 err_key2 ~merge_issues ~merge_descriptions = + let max_sev sev1 sev2 = if Exceptions.compare_severity sev1 sev2 >= 0 then sev1 else sev2 in + { severity= max_sev err_key1.severity err_key2.severity + ; err_name= merge_issues err_key1.err_name err_key2.err_name + ; err_desc= + Localise.verbatim_desc + (merge_descriptions err_key1.err_desc.descriptions err_key2.err_desc.descriptions) } + + (** Data associated to a specific error *) type err_data = { node_id: int @@ -86,6 +95,21 @@ type err_data = let compare_err_data err_data1 err_data2 = Location.compare err_data1.loc err_data2.loc +let merge_err_data err_data1 _ = + { node_id= 0 + ; node_key= None + ; session= 0 + ; loc= {err_data1.loc with col= -1} + ; loc_in_ml_source= None + ; loc_trace= [] + ; err_class= Exceptions.Checker + ; visibility= Exceptions.Exn_user + ; linters_def_file= None + ; doc_url= None + ; access= None + ; extras= None } + + module ErrDataSet = (* set err_data with no repeated loc *) Caml.Set.Make (struct type t = err_data diff --git a/infer/src/IR/Errlog.mli b/infer/src/IR/Errlog.mli index afebd1d83..e1b939572 100644 --- a/infer/src/IR/Errlog.mli +++ b/infer/src/IR/Errlog.mli @@ -43,6 +43,13 @@ type err_key = private {severity: Exceptions.severity; err_name: IssueType.t; err_desc: Localise.error_desc} [@@deriving compare] +val merge_err_key : + err_key + -> err_key + -> merge_issues:(IssueType.t -> IssueType.t -> IssueType.t) + -> merge_descriptions:(string list -> string list -> string) + -> err_key + (** Data associated to a specific error *) type err_data = private { node_id: int @@ -58,6 +65,8 @@ type err_data = private ; access: string option ; extras: Jsonbug_t.extra option } +val merge_err_data : err_data -> err_data -> err_data + (** Type of the error log *) type t diff --git a/infer/src/backend/InferPrint.ml b/infer/src/backend/InferPrint.ml index b5ff8a752..f603af37b 100644 --- a/infer/src/backend/InferPrint.ml +++ b/infer/src/backend/InferPrint.ml @@ -1042,13 +1042,17 @@ let pp_summary_and_issues formats_by_report_kind issue_formats = iterate_summaries (fun summary -> all_issues := process_summary filters formats_by_report_kind linereader stats summary !all_issues ) ; + all_issues := Issue.sort_filter_issues !all_issues ; + ( if Config.quandaryBO then + let quandaryBO_issues = QuandaryBO.get_issues !all_issues in + all_issues := List.rev_append !all_issues quandaryBO_issues ) ; List.iter ~f:(fun ({Issue.proc_name} as issue) -> let error_filter = error_filter filters proc_name in List.iter ~f:(fun issue_format -> pp_issue_in_format issue_format error_filter issue) issue_formats ) - (Issue.sort_filter_issues !all_issues) ; + !all_issues ; if Config.precondition_stats then PreconditionStats.pp_stats () ; List.iter [Config.lint_issues_dir_name; Config.starvation_issues_dir_name; Config.racerd_issues_dir_name] diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index ff490bd8f..a6ce84fde 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -665,6 +665,7 @@ and ( annotation_reachability , ownership , printf_args , quandary + , quandaryBO , racerd , resource_leak , siof @@ -718,6 +719,9 @@ and ( annotation_reachability For, example, this checker will warn about the type error in `printf(\"Hello %d\", \ \"world\")`" and quandary = mk_checker ~long:"quandary" ~default:false "the quandary taint analysis" + and quandaryBO = + mk_checker ~long:"quandaryBO" ~default:false + "[EXPERIMENTAL] The quandaryBO tainted buffer access analysis" and racerd = mk_checker ~long:"racerd" ~deprecated:["-threadsafety"] ~default:true "the RacerD thread safety analysis" @@ -782,6 +786,7 @@ and ( annotation_reachability , ownership , printf_args , quandary + , quandaryBO , racerd , resource_leak , siof @@ -2830,6 +2835,8 @@ and project_root = !project_root and quandary = !quandary +and quandaryBO = !quandaryBO + and quandary_endpoints = !quandary_endpoints and quandary_sanitizers = !quandary_sanitizers diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index f9c575cc8..899d9bcab 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -538,6 +538,8 @@ val progress_bar : [`MultiLine | `Plain | `Quiet] val quandary : bool +val quandaryBO : bool + val quandary_endpoints : Yojson.Basic.json val quandary_sanitizers : Yojson.Basic.json diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml index 3fddfb9a4..6c0170524 100644 --- a/infer/src/base/IssueType.ml +++ b/infer/src/base/IssueType.ml @@ -355,6 +355,10 @@ let symexec_memory_error = from_string "Symexec_memory_error" ~hum:"Symbolic Execution Memory Error" +let tainted_buffer_access = from_string "TAINTED_BUFFER_ACCESS" + +let tainted_memory_allocation = from_string "TAINTED_MEMORY_ALLOCATION" + let thread_safety_violation = from_string "THREAD_SAFETY_VIOLATION" let unary_minus_applied_to_unsigned_expression = diff --git a/infer/src/base/IssueType.mli b/infer/src/base/IssueType.mli index 2645f7307..a22a39851 100644 --- a/infer/src/base/IssueType.mli +++ b/infer/src/base/IssueType.mli @@ -259,6 +259,10 @@ val static_initialization_order_fiasco : t val symexec_memory_error : t +val tainted_buffer_access : t + +val tainted_memory_allocation : t + val thread_safety_violation : t val unary_minus_applied_to_unsigned_expression : t diff --git a/infer/src/checkers/registerCheckers.ml b/infer/src/checkers/registerCheckers.ml index 573e4f21e..65f456ecb 100644 --- a/infer/src/checkers/registerCheckers.ml +++ b/infer/src/checkers/registerCheckers.ml @@ -44,7 +44,9 @@ let all_checkers = [ (DynamicDispatch Interproc.analyze_procedure, Language.Clang) ; (DynamicDispatch Interproc.analyze_procedure, Language.Java) ] } ; { name= "buffer overrun" - ; active= Config.bufferoverrun && not Config.cost (* Cost analysis already triggers Inferbo *) + ; active= + (Config.bufferoverrun || Config.quandaryBO) && not Config.cost + (* Cost analysis already triggers Inferbo *) ; callbacks= [ (Procedure BufferOverrunChecker.checker, Language.Clang) ; (Procedure BufferOverrunChecker.checker, Language.Java) ] } @@ -76,7 +78,7 @@ let all_checkers = ; active= Config.ownership ; callbacks= [(Procedure Ownership.checker, Language.Clang)] } ; { name= "quandary" - ; active= Config.quandary + ; active= Config.quandary || Config.quandaryBO ; callbacks= [ (Procedure JavaTaintAnalysis.checker, Language.Java) ; (Procedure ClangTaintAnalysis.checker, Language.Clang) ] } diff --git a/infer/src/quandary/quandaryBO.ml b/infer/src/quandary/quandaryBO.ml new file mode 100644 index 000000000..fd54dc8c9 --- /dev/null +++ b/infer/src/quandary/quandaryBO.ml @@ -0,0 +1,71 @@ +(* + * Copyright (c) 2018-present, Facebook, Inc. + * + * 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 get_issues all_issues = + let quandary_bug_names = + IssueType.[untrusted_buffer_access; untrusted_heap_allocation; untrusted_variable_length_array] + in + let inferbo_bug_names = + IssueType. + [ buffer_overrun_l1 + ; buffer_overrun_l2 + ; buffer_overrun_l3 + ; buffer_overrun_l4 + ; buffer_overrun_l5 + ; buffer_overrun_s2 + ; buffer_overrun_u5 + ; inferbo_alloc_is_big + ; inferbo_alloc_is_zero + ; inferbo_alloc_is_negative + ; inferbo_alloc_may_be_big + ; inferbo_alloc_may_be_negative ] + in + let is_quandary_issue issue = + List.mem quandary_bug_names issue.Issue.err_key.err_name ~equal:IssueType.equal + in + let is_inferbo_issue issue = + List.mem inferbo_bug_names issue.Issue.err_key.err_name ~equal:IssueType.equal + in + let quandary_issues, inferBO_issues = + List.fold all_issues ~init:([], []) ~f:(fun (q_issues, iBO_issues) issue -> + if is_quandary_issue issue then (issue :: q_issues, iBO_issues) + else if is_inferbo_issue issue then (q_issues, issue :: iBO_issues) + else (q_issues, iBO_issues) ) + in + let matching_issues quandary_issue inferbo_issue = + SourceFile.equal quandary_issue.Issue.proc_location.file inferbo_issue.Issue.proc_location.file + && Int.equal quandary_issue.Issue.proc_location.line inferbo_issue.Issue.proc_location.line + in + let paired_issues = + (* Can be computed more efficiently (in n*log(n)) by using a Map mapping + file name + line number to quandary_issues to match with inferbo_issues *) + List.concat_map quandary_issues ~f:(fun quandary_issue -> + List.filter_map inferBO_issues ~f:(fun inferbo_issue -> + if matching_issues quandary_issue inferbo_issue then + Some (quandary_issue, inferbo_issue) + else None ) ) + in + let merge_issues (issue1, issue2) = + { Issue.proc_name= issue1.Issue.proc_name + ; proc_location= {issue1.Issue.proc_location with col= -1} + ; err_key= + Errlog.merge_err_key issue1.Issue.err_key issue2.Issue.err_key + ~merge_issues:(fun issue1 _ -> + if IssueType.equal issue1 IssueType.untrusted_buffer_access then + IssueType.tainted_buffer_access + else IssueType.tainted_memory_allocation ) + ~merge_descriptions:(fun descs1 descs2 -> + String.concat + ( "QuandaryBO error. Quandary error(s):\n" + :: (descs1 @ ("InferBO error(s):\n" :: descs2)) ) ) + ; err_data= Errlog.merge_err_data issue1.Issue.err_data issue2.Issue.err_data } + in + (* Can merge List.map, List.concat_map and List.filter_map into a single fold. *) + let quandaryBO_issues = List.map ~f:merge_issues paired_issues in + quandaryBO_issues diff --git a/infer/src/quandary/quandaryBO.mli b/infer/src/quandary/quandaryBO.mli new file mode 100644 index 000000000..2e0c1bacc --- /dev/null +++ b/infer/src/quandary/quandaryBO.mli @@ -0,0 +1,10 @@ +(* + * Copyright (c) 2018-present, Facebook, Inc. + * + * 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 get_issues : Issue.t list -> Issue.t list diff --git a/infer/src/unit/SeverityTests.ml b/infer/src/unit/SeverityTests.ml index 1b8c1f8d3..422f09bfe 100644 --- a/infer/src/unit/SeverityTests.ml +++ b/infer/src/unit/SeverityTests.ml @@ -9,10 +9,10 @@ open! IStd open OUnit2 let order_tests _ = - assert_equal (-1) ([%compare: Exceptions.severity] Exceptions.Like Exceptions.Info) ; - assert_equal (-1) ([%compare: Exceptions.severity] Exceptions.Info Exceptions.Advice) ; - assert_equal (-1) ([%compare: Exceptions.severity] Exceptions.Advice Exceptions.Warning) ; - assert_equal (-1) ([%compare: Exceptions.severity] Exceptions.Warning Exceptions.Error) + assert_equal (-1) (Exceptions.compare_severity Exceptions.Like Exceptions.Info) ; + assert_equal (-1) (Exceptions.compare_severity Exceptions.Info Exceptions.Advice) ; + assert_equal (-1) (Exceptions.compare_severity Exceptions.Advice Exceptions.Warning) ; + assert_equal (-1) (Exceptions.compare_severity Exceptions.Warning Exceptions.Error) let tests = "severity_test_suite" >::: ["severity_order_tests" >:: order_tests] diff --git a/infer/tests/codetoanalyze/cpp/quandaryBO/.inferconfig b/infer/tests/codetoanalyze/cpp/quandaryBO/.inferconfig new file mode 100644 index 000000000..e6e9ac25e --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/quandaryBO/.inferconfig @@ -0,0 +1,8 @@ +{ + "quandary-sources": [ + { + "procedure": "__infer_taint_source", + "kind": "Other" + } + ] +} diff --git a/infer/tests/codetoanalyze/cpp/quandaryBO/Makefile b/infer/tests/codetoanalyze/cpp/quandaryBO/Makefile new file mode 100644 index 000000000..a0ba203ee --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/quandaryBO/Makefile @@ -0,0 +1,19 @@ +# Copyright (c) 2016-present, Facebook, Inc. +# +# This source code is licensed under the MIT license found in the +# LICENSE file in the root directory of this source tree. + +TESTS_DIR = ../../.. + +ANALYZER = checkers +# see explanations in cpp/errors/Makefile for the custom isystem +CLANG_OPTIONS = -x c++ -std=c++11 -nostdinc++ -isystem$(ROOT_DIR) -isystem$(CLANG_INCLUDES)/c++/v1/ -c +INFER_OPTIONS = \ + -F --quandaryBO-only --passthroughs --debug-exceptions \ + --project-root $(TESTS_DIR) \ + +INFERPRINT_OPTIONS = --issues-tests + +SOURCES = $(wildcard *.cpp) + +include $(TESTS_DIR)/clang.make diff --git a/infer/tests/codetoanalyze/cpp/quandaryBO/issues.exp b/infer/tests/codetoanalyze/cpp/quandaryBO/issues.exp new file mode 100644 index 000000000..864542147 --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/quandaryBO/issues.exp @@ -0,0 +1,6 @@ +codetoanalyze/cpp/quandaryBO/tainted_index.cpp, basic_bad, 3, BUFFER_OVERRUN_U5, no_bucket, ERROR, [ArrayDeclaration,Unknown value from: __infer_taint_source,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: 10] +codetoanalyze/cpp/quandaryBO/tainted_index.cpp, basic_bad, 3, TAINTED_BUFFER_ACCESS, no_bucket, ERROR, [] +codetoanalyze/cpp/quandaryBO/tainted_index.cpp, basic_bad, 3, UNTRUSTED_BUFFER_ACCESS, no_bucket, ERROR, [Return from __infer_taint_source,Call to __array_access with tainted index 0] +codetoanalyze/cpp/quandaryBO/tainted_index.cpp, multi_level_bad, 2, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Call,Unknown value from: __infer_taint_source,Assignment,Return,Assignment,Call,ArrayDeclaration,Parameter: i,ArrayAccess: Offset: [1, +oo] Size: 10 by call to `multi_level_sink_bad` ] +codetoanalyze/cpp/quandaryBO/tainted_index.cpp, multi_level_bad, 2, TAINTED_BUFFER_ACCESS, no_bucket, ERROR, [] +codetoanalyze/cpp/quandaryBO/tainted_index.cpp, multi_level_bad, 2, UNTRUSTED_BUFFER_ACCESS, no_bucket, ERROR, [Return from __infer_taint_source with tainted data return*,Return from multi_level_source_bad,Call to multi_level_sink_bad with tainted index 0,Call to __array_access with tainted index 0] diff --git a/infer/tests/codetoanalyze/cpp/quandaryBO/tainted_index.cpp b/infer/tests/codetoanalyze/cpp/quandaryBO/tainted_index.cpp new file mode 100644 index 000000000..b60f55142 --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/quandaryBO/tainted_index.cpp @@ -0,0 +1,26 @@ +/* + * Copyright (c) 2018-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ +extern int __infer_taint_source(); + +void basic_bad() { + int arr[10]; + int source = __infer_taint_source(); + arr[source] = 2; +} + +int multi_level_source_bad() { return __infer_taint_source(); } + +void multi_level_sink_bad(int i) { + int arr[10]; + if (i > 0) + arr[i] = 2; +} + +void multi_level_bad() { + int i = multi_level_source_bad(); + multi_level_sink_bad(i); +}