QuandaryBO

Reviewed By: mbouaziz

Differential Revision: D9615368

fbshipit-source-id: 56888a18f

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)

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

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
 

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]

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

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

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 =

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

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) ] }

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

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

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) (Exceptions.compare_severity Exceptions.Like Exceptions.Info) ;
-  assert_equal (-1) ([%compare: Exceptions.severity] Exceptions.Info Exceptions.Advice) ;
+  assert_equal (-1) (Exceptions.compare_severity Exceptions.Info Exceptions.Advice) ;
-  assert_equal (-1) ([%compare: Exceptions.severity] Exceptions.Advice Exceptions.Warning) ;
+  assert_equal (-1) (Exceptions.compare_severity Exceptions.Advice Exceptions.Warning) ;
-  assert_equal (-1) ([%compare: Exceptions.severity] Exceptions.Warning Exceptions.Error)
+  assert_equal (-1) (Exceptions.compare_severity Exceptions.Warning Exceptions.Error)
 
 
 let tests = "severity_test_suite" >::: ["severity_order_tests" >:: order_tests]

infer/tests/codetoanalyze/cpp/quandaryBO/.inferconfig

@@ -0,0 +1,8 @@
+{
+  "quandary-sources": [
+    {
+      "procedure": "__infer_taint_source",
+      "kind": "Other"
+    }
+  ]
+}

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

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]

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);
+}