From 788a600ed90a8ff4fd136ebee3f8a85c50e2a95b Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Mon, 15 Jun 2020 03:18:31 -0700 Subject: [PATCH] [inferbo] Add documentation of issues Reviewed By: jvillard Differential Revision: D22021568 fbshipit-source-id: 06babaf36 --- infer/documentation/issues/BUFFER_OVERRUN.md | 44 +++++++++++++ .../documentation/issues/INTEGER_OVERFLOW.md | 18 +++++ infer/src/base/IssueType.ml | 65 ++++++++++++++++--- 3 files changed, 117 insertions(+), 10 deletions(-) create mode 100644 infer/documentation/issues/BUFFER_OVERRUN.md create mode 100644 infer/documentation/issues/INTEGER_OVERFLOW.md diff --git a/infer/documentation/issues/BUFFER_OVERRUN.md b/infer/documentation/issues/BUFFER_OVERRUN.md new file mode 100644 index 000000000..33fc86c70 --- /dev/null +++ b/infer/documentation/issues/BUFFER_OVERRUN.md @@ -0,0 +1,44 @@ +Buffer overrun reports fall into several "buckets" corresponding to the expected precision of the +report. The higher the number, the more likely it is to be a false positive. + +* `L1`: The most faithful report, when it *must* be unsafe. For example, array size: `[5,5]`, + offset: `[3,3]`. + +* `L2`: Less faithful report than `L1`, when it *may* be unsafe. For example, array size:`[5,5]`, + offset: `[0,5]`. Note that the offset may be a safe value in the real execution, i.e. 0, 1, 2, + 3, 4. + +* `L5`: The least faithful report, when there is an interval top. For example, array size: + `[5,5]`, offset: `[-oo,+oo]`. + +* `L4`: More faithful report than `L5`, when there is an infinity value. For example, array size: + `[5,5]`, offset: `[0, +oo]`. + +* `L3`: The reports that are not included in the above cases. + +Other than them, there are some specific-purpose buffer overrun reports as follows. + +* `R2`: An array access is unsafe by *risky* array values from `strndup`. For example, suppose + there is a `strndup` call as follows. + + ```c + char* s1 = (char*)malloc(sizeof(char) * size); + for (int i = 0; i < size; i++) { + s1[i] = 'a'; + } + s1[5] = '\0'; + char* s2 = strndup(s1, size - 1); + s2[size - 1] = 'a'; + ``` + + Even if the second parameter of `strndup` is `size - 1`, the length of `s2` can be shorter than + `size` if there is the null character in the middle of `s1`. + +* `S2`: An array access is unsafe by symbolic values. For example, array size: `[n,n]`, offset + `[n,+oo]`. + +* `T1`: An array access is unsafe by tainted external values. This is experimental and will be + removed sooner or later. + +* `U5`: An array access is unsafe by unknown values, which are usually from unknown function + calls. diff --git a/infer/documentation/issues/INTEGER_OVERFLOW.md b/infer/documentation/issues/INTEGER_OVERFLOW.md new file mode 100644 index 000000000..7c5a63f1a --- /dev/null +++ b/infer/documentation/issues/INTEGER_OVERFLOW.md @@ -0,0 +1,18 @@ +Integer overflows reports fall into several "buckets" corresponding to the expected precision of the +report. The higher the number, the more likely it is to be a false positive. + +* `L1`: The most faithful report, when it *must* be unsafe. For example, + `[2147483647,2147483647] + [1,1]` in 32-bit signed integer type. + +* `L2`: Less faithful report than `L1`, when it *may* be unsafe. For example, + `[2147483647,2147483647] + [0,1]` in 32-bit signed integer type. Note that the integer of RHS + can be 0, which is safe. + +* `L5`: The reports that are not included in the above cases. + +Other than them, there as some specific-purpose buffer overrun reports as follows. + +* `R2`: A binary integer operation is unsafe by *risky* return values from `strndup`. + +* `U5`: A binary integer operation is unsafe by unknown values, which are usually from unknown + function calls. diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml index 018739e9e..692e1f413 100644 --- a/infer/src/base/IssueType.ml +++ b/infer/src/base/IssueType.ml @@ -252,28 +252,49 @@ let biabd_use_after_free = register_from_string ~hum:"Use After Free" ~id:"BIABD_USE_AFTER_FREE" Error Biabduction -let buffer_overrun_l1 = register_from_string ~id:"BUFFER_OVERRUN_L1" Error BufferOverrunChecker +let buffer_overrun_l1 = + register_from_string ~id:"BUFFER_OVERRUN_L1" Error BufferOverrunChecker + ~user_documentation:[%blob "../../documentation/issues/BUFFER_OVERRUN.md"] -let buffer_overrun_l2 = register_from_string ~id:"BUFFER_OVERRUN_L2" Error BufferOverrunChecker -let buffer_overrun_l3 = register_from_string ~id:"BUFFER_OVERRUN_L3" Error BufferOverrunChecker +let buffer_overrun_l2 = + register_from_string ~id:"BUFFER_OVERRUN_L2" Error BufferOverrunChecker + ~user_documentation:"See [BUFFER_OVERRUN_L1](#buffer_overrun_l1)" + + +let buffer_overrun_l3 = + register_from_string ~id:"BUFFER_OVERRUN_L3" Error BufferOverrunChecker + ~user_documentation:"See [BUFFER_OVERRUN_L1](#buffer_overrun_l1)" + let buffer_overrun_l4 = register_from_string ~enabled:false ~id:"BUFFER_OVERRUN_L4" Error BufferOverrunChecker + ~user_documentation:"See [BUFFER_OVERRUN_L1](#buffer_overrun_l1)" let buffer_overrun_l5 = register_from_string ~enabled:false ~id:"BUFFER_OVERRUN_L5" Error BufferOverrunChecker + ~user_documentation:"See [BUFFER_OVERRUN_L1](#buffer_overrun_l1)" + + +let buffer_overrun_r2 = + register_from_string ~id:"BUFFER_OVERRUN_R2" Error BufferOverrunChecker + ~user_documentation:"See [BUFFER_OVERRUN_L1](#buffer_overrun_l1)" + +let buffer_overrun_s2 = + register_from_string ~id:"BUFFER_OVERRUN_S2" Error BufferOverrunChecker + ~user_documentation:"See [BUFFER_OVERRUN_L1](#buffer_overrun_l1)" -let buffer_overrun_r2 = register_from_string ~id:"BUFFER_OVERRUN_R2" Error BufferOverrunChecker -let buffer_overrun_s2 = register_from_string ~id:"BUFFER_OVERRUN_S2" Error BufferOverrunChecker +let buffer_overrun_t1 = + register_from_string ~id:"BUFFER_OVERRUN_T1" Error BufferOverrunChecker + ~user_documentation:"See [BUFFER_OVERRUN_L1](#buffer_overrun_l1)" -let buffer_overrun_t1 = register_from_string ~id:"BUFFER_OVERRUN_T1" Error BufferOverrunChecker let buffer_overrun_u5 = register_from_string ~enabled:false ~id:"BUFFER_OVERRUN_U5" Error BufferOverrunChecker + ~user_documentation:"See [BUFFER_OVERRUN_L1](#buffer_overrun_l1)" let cannot_star = register_from_string ~visibility:Developer ~id:"Cannot_star" Error Biabduction @@ -357,10 +378,12 @@ let component_with_unconventional_superclass = let condition_always_false = register_from_string ~enabled:false ~id:"CONDITION_ALWAYS_FALSE" Warning BufferOverrunChecker + ~user_documentation:"A condition expression is **always** evaluated to false." let condition_always_true = register_from_string ~enabled:false ~id:"CONDITION_ALWAYS_TRUE" Warning BufferOverrunChecker + ~user_documentation:"A condition expression is **always** evaluated to true." let constant_address_dereference = @@ -578,26 +601,34 @@ let inefficient_keyset_iterator = let inferbo_alloc_is_big = register_from_string ~id:"INFERBO_ALLOC_IS_BIG" Error BufferOverrunChecker + ~user_documentation:"`malloc` is passed a large constant value." let inferbo_alloc_is_negative = register_from_string ~id:"INFERBO_ALLOC_IS_NEGATIVE" Error BufferOverrunChecker + ~user_documentation:"`malloc` is called with a negative size." let inferbo_alloc_is_zero = register_from_string ~id:"INFERBO_ALLOC_IS_ZERO" Error BufferOverrunChecker + ~user_documentation:"`malloc` is called with a zero size." let inferbo_alloc_may_be_big = register_from_string ~id:"INFERBO_ALLOC_MAY_BE_BIG" Error BufferOverrunChecker + ~user_documentation:"`malloc` *may* be called with a large value." let inferbo_alloc_may_be_negative = register_from_string ~id:"INFERBO_ALLOC_MAY_BE_NEGATIVE" Error BufferOverrunChecker + ~user_documentation:"`malloc` *may* be called with a negative value." let inferbo_alloc_may_be_tainted = register_from_string ~id:"INFERBO_ALLOC_MAY_BE_TAINTED" Error BufferOverrunChecker + ~user_documentation: + "`malloc` *may* be called with a tainted value from external sources. This is experimental \ + and will be removed sooner or later." let infinite_cost_call ~kind = register_from_cost_string ~enabled:false "INFINITE_%s" ~kind @@ -608,18 +639,29 @@ let inherently_dangerous_function = let insecure_intent_handling = register_from_string ~id:"INSECURE_INTENT_HANDLING" Error Quandary -let integer_overflow_l1 = register_from_string ~id:"INTEGER_OVERFLOW_L1" Error BufferOverrunChecker +let integer_overflow_l1 = + register_from_string ~id:"INTEGER_OVERFLOW_L1" Error BufferOverrunChecker + ~user_documentation:[%blob "../../documentation/issues/INTEGER_OVERFLOW.md"] + + +let integer_overflow_l2 = + register_from_string ~id:"INTEGER_OVERFLOW_L2" Error BufferOverrunChecker + ~user_documentation:"See [INTEGER_OVERFLOW_L1](#integer_overflow_l1)" -let integer_overflow_l2 = register_from_string ~id:"INTEGER_OVERFLOW_L2" Error BufferOverrunChecker let integer_overflow_l5 = register_from_string ~enabled:false ~id:"INTEGER_OVERFLOW_L5" Error BufferOverrunChecker + ~user_documentation:"See [INTEGER_OVERFLOW_L1](#integer_overflow_l1)" -let integer_overflow_r2 = register_from_string ~id:"INTEGER_OVERFLOW_R2" Error BufferOverrunChecker +let integer_overflow_r2 = + register_from_string ~id:"INTEGER_OVERFLOW_R2" Error BufferOverrunChecker + ~user_documentation:"See [INTEGER_OVERFLOW_L1](#integer_overflow_l1)" + let integer_overflow_u5 = register_from_string ~enabled:false ~id:"INTEGER_OVERFLOW_U5" Error BufferOverrunChecker + ~user_documentation:"See [INTEGER_OVERFLOW_L1](#integer_overflow_l1)" let interface_not_thread_safe = @@ -836,7 +878,10 @@ let _unavailable_api_in_supported_ios_sdk = let uninitialized_value = register_from_string ~id:"UNINITIALIZED_VALUE" Error Uninit -let unreachable_code_after = register_from_string ~id:"UNREACHABLE_CODE" Error BufferOverrunChecker +let unreachable_code_after = + register_from_string ~id:"UNREACHABLE_CODE" Error BufferOverrunChecker + ~user_documentation:"A program point is unreachable." + let use_after_delete = register_from_string ~id:"USE_AFTER_DELETE" Error Pulse