From f0c73c53fa4b88ddeb0484a01b05aa142a07dcf9 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Wed, 27 Sep 2023 15:00:56 +0200 Subject: [PATCH 01/22] Add support for 3rd param of memcpy --- src/analyses/libraryDesc.ml | 2 +- src/analyses/libraryFunctions.ml | 16 ++++++++-------- 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/src/analyses/libraryDesc.ml b/src/analyses/libraryDesc.ml index 94de4fbf82..2ff1169db8 100644 --- a/src/analyses/libraryDesc.ml +++ b/src/analyses/libraryDesc.ml @@ -62,7 +62,7 @@ type special = | Math of { fun_args: math; } | Memset of { dest: Cil.exp; ch: Cil.exp; count: Cil.exp; } | Bzero of { dest: Cil.exp; count: Cil.exp; } - | Memcpy of { dest: Cil.exp; src: Cil.exp } + | Memcpy of { dest: Cil.exp; src: Cil.exp; n: Cil.exp; } | Strcpy of { dest: Cil.exp; src: Cil.exp; n: Cil.exp option; } | Strcat of { dest: Cil.exp; src: Cil.exp; n: Cil.exp option; } | Strlen of Cil.exp diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 137a3103a5..575c036a23 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -12,12 +12,12 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("memset", special [__ "dest" [w]; __ "ch" []; __ "count" []] @@ fun dest ch count -> Memset { dest; ch; count; }); ("__builtin_memset", special [__ "dest" [w]; __ "ch" []; __ "count" []] @@ fun dest ch count -> Memset { dest; ch; count; }); ("__builtin___memset_chk", special [__ "dest" [w]; __ "ch" []; __ "count" []; drop "os" []] @@ fun dest ch count -> Memset { dest; ch; count; }); - ("memcpy", special [__ "dest" [w]; __ "src" [r]; drop "n" []] @@ fun dest src -> Memcpy { dest; src }); - ("__builtin_memcpy", special [__ "dest" [w]; __ "src" [r]; drop "n" []] @@ fun dest src -> Memcpy { dest; src }); - ("__builtin___memcpy_chk", special [__ "dest" [w]; __ "src" [r]; drop "n" []; drop "os" []] @@ fun dest src -> Memcpy { dest; src }); - ("memmove", special [__ "dest" [w]; __ "src" [r]; drop "count" []] @@ fun dest src -> Memcpy { dest; src }); - ("__builtin_memmove", special [__ "dest" [w]; __ "src" [r]; drop "count" []] @@ fun dest src -> Memcpy { dest; src }); - ("__builtin___memmove_chk", special [__ "dest" [w]; __ "src" [r]; drop "count" []; drop "os" []] @@ fun dest src -> Memcpy { dest; src }); + ("memcpy", special [__ "dest" [w]; __ "src" [r]; __ "n" []] @@ fun dest src n -> Memcpy { dest; src; n; }); + ("__builtin_memcpy", special [__ "dest" [w]; __ "src" [r]; __ "n" []] @@ fun dest src n -> Memcpy { dest; src; n; }); + ("__builtin___memcpy_chk", special [__ "dest" [w]; __ "src" [r]; __ "n" []; drop "os" []] @@ fun dest src n -> Memcpy { dest; src; n; }); + ("memmove", special [__ "dest" [w]; __ "src" [r]; __ "count" []] @@ fun dest src count -> Memcpy { dest; src; n = count; }); + ("__builtin_memmove", special [__ "dest" [w]; __ "src" [r]; __ "count" []] @@ fun dest src count -> Memcpy { dest; src; n = count; }); + ("__builtin___memmove_chk", special [__ "dest" [w]; __ "src" [r]; __ "count" []; drop "os" []] @@ fun dest src count -> Memcpy { dest; src; n = count; }); ("strcpy", special [__ "dest" [w]; __ "src" [r]] @@ fun dest src -> Strcpy { dest; src; n = None; }); ("__builtin_strcpy", special [__ "dest" [w]; __ "src" [r]] @@ fun dest src -> Strcpy { dest; src; n = None; }); ("__builtin___strcpy_chk", special [__ "dest" [w]; __ "src" [r]; drop "os" []] @@ fun dest src -> Strcpy { dest; src; n = None; }); @@ -452,8 +452,8 @@ let glibc_desc_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("strcasestr", unknown [drop "haystack" [r]; drop "needle" [r]]); ("inet_aton", unknown [drop "cp" [r]; drop "inp" [w]]); ("fopencookie", unknown [drop "cookie" []; drop "mode" [r]; drop "io_funcs" [s_deep]]); (* doesn't access cookie but passes it to io_funcs *) - ("mempcpy", special [__ "dest" [w]; __ "src" [r]; drop "n" []] @@ fun dest src -> Memcpy { dest; src }); - ("__builtin___mempcpy_chk", special [__ "dest" [w]; __ "src" [r]; drop "n" []; drop "os" []] @@ fun dest src -> Memcpy { dest; src }); + ("mempcpy", special [__ "dest" [w]; __ "src" [r]; __ "n" []] @@ fun dest src n -> Memcpy { dest; src; n; }); + ("__builtin___mempcpy_chk", special [__ "dest" [w]; __ "src" [r]; __ "n" []; drop "os" []] @@ fun dest src n -> Memcpy { dest; src; n; }); ] let linux_userspace_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ From 6e7c00edaf5891050401b8f3f87a2d07333dca6a Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Fri, 29 Sep 2023 11:54:52 +0200 Subject: [PATCH 02/22] Add out-of-bounds check for memset and memcpy --- src/analyses/base.ml | 81 ++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 79 insertions(+), 2 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index c4fdd633d3..49f61fdd1e 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2026,6 +2026,80 @@ struct M.warn ~category:(Behavior (Undefined InvalidMemoryDeallocation)) ~tags:[CWE 761] "Free of memory not at start of buffer in function %s for pointer %a" special_fn.vname d_exp ptr | _ -> M.warn ~category:MessageCategory.Analyzer "Pointer %a in function %s doesn't evaluate to a valid address." d_exp ptr special_fn.vname + (* Get the size of the smallest memory that dest points-to *) + let get_min_size_of_dest ctx dest = + let intdom_of_int x = + ID.of_int (Cilfacade.ptrdiff_ikind ()) (Z.of_int x) + in + let points_to_heap_only = + match ctx.ask (Queries.MayPointTo dest) with + | a when not (AD.is_top a) -> + AD.for_all (function + | Addr (v, _) -> ctx.ask (Queries.IsHeapVar v) + | _ -> false + ) a + | _ -> false + in + if points_to_heap_only then + (* Ask for BlobSize from the base address (the second field set to true) in order to avoid BlobSize giving us bot *) + ctx.ask (Queries.BlobSize {exp = dest; base_address = true}) + else + match ctx.ask (Queries.MayPointTo dest) with + | a when not (Queries.AD.is_top a) -> + let pts_list = Queries.AD.elements a in + let pts_elems_to_sizes (addr: Queries.AD.elt) = + begin match addr with + | Addr (v, _) -> + begin match v.vtype with + | TArray (item_typ, _, _) -> + let item_typ_size_in_bytes = (bitsSizeOf item_typ) / 8 in + let item_typ_size_in_bytes = intdom_of_int item_typ_size_in_bytes in + begin match ctx.ask (Queries.EvalLength dest) with + | `Lifted arr_len -> `Lifted (ID.mul item_typ_size_in_bytes arr_len) + | `Bot -> `Bot + | `Top -> `Top + end + | _ -> + let type_size_in_bytes = (bitsSizeOf v.vtype) / 8 in + `Lifted (intdom_of_int type_size_in_bytes) + end + | _ -> `Top + end + in + (* Map each points-to-set element to its size *) + let pts_sizes = List.map pts_elems_to_sizes pts_list in + (* Take the smallest of all sizes that ptr's contents may have *) + begin match pts_sizes with + | [] -> `Bot + | [x] -> x + | x::xs -> List.fold_left (fun acc elem -> + if ValueDomainQueries.ID.compare acc elem >= 0 then elem else acc + ) x xs + end + | _ -> + M.warn "Pointer %a has a points-to-set of top. An invalid memory access might occur" d_exp dest; + `Top + + (* Used for memset() and memcpy() out-of-bounds checks *) + let check_count ctx fun_name dest n = + let (behavior:MessageCategory.behavior) = Undefined MemoryOutOfBoundsAccess in + let cwe_number = 823 in + let dest_size = get_min_size_of_dest ctx dest in + let eval_n = ctx.ask (Queries.EvalInt n) in + match ValueDomainQueries.ID.is_top dest_size, ValueDomainQueries.ID.is_top eval_n with + | true, _ -> + AnalysisState.svcomp_may_invalid_deref := true; + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of dest %a in function %s is unknown. Memory out-of-bounds access might occur" d_exp dest fun_name + | _, true -> + AnalysisState.svcomp_may_invalid_deref := true; + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Count parameter, passed to function %s is unknown. Memory out-of-bounds access might occur" fun_name + | false, false -> + if dest_size < eval_n then begin + AnalysisState.svcomp_may_invalid_deref := true; + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of dest in function %s is %a (in bytes). Count is %a (in bytes). Memory out-of-bounds access must occur" fun_name ValueDomainQueries.ID.pretty dest_size ValueDomainQueries.ID.pretty eval_n + end + + let special ctx (lv:lval option) (f: varinfo) (args: exp list) = let invalidate_ret_lv st = match lv with | Some lv -> @@ -2093,7 +2167,8 @@ struct in let st = match desc.special args, f.vname with | Memset { dest; ch; count; }, _ -> - (* TODO: check count *) + (* Check count *) + check_count ctx f.vname dest count; let eval_ch = eval_rv (Analyses.ask_of_ctx ctx) gs st ch in let dest_a, dest_typ = addr_type_of_exp dest in let value = @@ -2110,7 +2185,9 @@ struct let dest_a, dest_typ = addr_type_of_exp dest in let value = VD.zero_init_value dest_typ in set ~ctx (Analyses.ask_of_ctx ctx) gs st dest_a dest_typ value - | Memcpy { dest = dst; src }, _ -> + | Memcpy { dest = dst; src; n; }, _ -> + (* Check n *) + check_count ctx f.vname dst n; memory_copying dst src (* strcpy(dest, src); *) | Strcpy { dest = dst; src; n = None }, _ -> From 5ed769f22598ed1aeb5cb36038ffc94cb1c49b55 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Fri, 29 Sep 2023 11:55:16 +0200 Subject: [PATCH 03/22] Add regr. test case for memset and memcpy out-of-bounds --- .../77-mem-oob/06-memset-memcpy-oob.c | 20 +++++++++++++++++++ 1 file changed, 20 insertions(+) create mode 100644 tests/regression/77-mem-oob/06-memset-memcpy-oob.c diff --git a/tests/regression/77-mem-oob/06-memset-memcpy-oob.c b/tests/regression/77-mem-oob/06-memset-memcpy-oob.c new file mode 100644 index 0000000000..84a46c75ba --- /dev/null +++ b/tests/regression/77-mem-oob/06-memset-memcpy-oob.c @@ -0,0 +1,20 @@ +// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval +#include +#include + +int main(int argc, char const *argv[]) { + int *a = malloc(10 * sizeof(int)); //Size is 40 bytes, assuming a 4-byte int + int *b = malloc(15 * sizeof(int)); //Size is 60 bytes, assuming a 4-byte int + + memset(a, 0, 40); //NOWARN + memset(a, 0, 10 * sizeof(int)); //NOWARN + memset(a, 0, 41); //WARN + memset(a, 0, 40000000); //WARN + + memcpy(a, b, 40); //NOWARN + memcpy(a, b, 10 * sizeof(int)); //NOWARN + memcpy(a, b, 41); //WARN + memcpy(a, b, 40000000); //WARN + memcpy(a, b, 15 * sizeof(int)); //WARN + return 0; +} From 12bee2749dcba9ae933c657cb991ffb3ea292013 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Fri, 29 Sep 2023 13:22:37 +0200 Subject: [PATCH 04/22] Add temporary fix for failing MacOS CI job --- tests/regression/77-mem-oob/06-memset-memcpy-oob.c | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/tests/regression/77-mem-oob/06-memset-memcpy-oob.c b/tests/regression/77-mem-oob/06-memset-memcpy-oob.c index 84a46c75ba..1050c199e0 100644 --- a/tests/regression/77-mem-oob/06-memset-memcpy-oob.c +++ b/tests/regression/77-mem-oob/06-memset-memcpy-oob.c @@ -1,4 +1,5 @@ -// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval +// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval --disable warn.info +// TODO: The "--disable warn.info" part is a temporary fix and needs to be removed once the MacOS CI job is fixed #include #include From 391c6ce91678ba93085d6f8081fa4ee1aa54936d Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Fri, 29 Sep 2023 16:41:42 +0200 Subject: [PATCH 05/22] Change memset/memcpy count warning from must to may --- src/analyses/base.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 49f61fdd1e..605d0f0993 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2096,7 +2096,7 @@ struct | false, false -> if dest_size < eval_n then begin AnalysisState.svcomp_may_invalid_deref := true; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of dest in function %s is %a (in bytes). Count is %a (in bytes). Memory out-of-bounds access must occur" fun_name ValueDomainQueries.ID.pretty dest_size ValueDomainQueries.ID.pretty eval_n + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of dest in function %s is %a (in bytes). Count is %a (in bytes). Memory out-of-bounds access may occur" fun_name ValueDomainQueries.ID.pretty dest_size ValueDomainQueries.ID.pretty eval_n end From fae72563a48b8b7a344395e8f6d75d76630bc8c9 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Fri, 29 Sep 2023 16:51:05 +0200 Subject: [PATCH 06/22] Use ID.lt to compare dest size with count --- src/analyses/base.ml | 24 +++++++++++++++++------- 1 file changed, 17 insertions(+), 7 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 605d0f0993..9e35694ff8 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2086,17 +2086,27 @@ struct let cwe_number = 823 in let dest_size = get_min_size_of_dest ctx dest in let eval_n = ctx.ask (Queries.EvalInt n) in - match ValueDomainQueries.ID.is_top dest_size, ValueDomainQueries.ID.is_top eval_n with - | true, _ -> + match dest_size, eval_n with + | `Top, _ -> AnalysisState.svcomp_may_invalid_deref := true; M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of dest %a in function %s is unknown. Memory out-of-bounds access might occur" d_exp dest fun_name - | _, true -> + | _, `Top -> AnalysisState.svcomp_may_invalid_deref := true; M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Count parameter, passed to function %s is unknown. Memory out-of-bounds access might occur" fun_name - | false, false -> - if dest_size < eval_n then begin - AnalysisState.svcomp_may_invalid_deref := true; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of dest in function %s is %a (in bytes). Count is %a (in bytes). Memory out-of-bounds access may occur" fun_name ValueDomainQueries.ID.pretty dest_size ValueDomainQueries.ID.pretty eval_n + | `Bot, _ -> + AnalysisState.svcomp_may_invalid_deref := true; + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of dest %a in function %s is bottom. Memory out-of-bounds access might occur" d_exp dest fun_name + | _, `Bot -> + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Count parameter, passed to function %s is bottom" fun_name + | `Lifted ds, `Lifted en -> + begin match ID.to_bool (ID.lt ds en) with + | Some true -> + AnalysisState.svcomp_may_invalid_deref := true; + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of dest in function %s is %a (in bytes). Count is %a (in bytes). Memory out-of-bounds access may occur" fun_name ValueDomainQueries.ID.pretty dest_size ValueDomainQueries.ID.pretty eval_n + | Some false -> () + | None -> + AnalysisState.svcomp_may_invalid_deref := true; + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Could not compare size of dest (%a) with count (%a) in function %s. Memory out-of-bounds access may occur" ID.pretty ds ID.pretty en fun_name end From 655362e70a7d0c2a42c4dba910e5c67de1aee1c9 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Fri, 29 Sep 2023 16:53:39 +0200 Subject: [PATCH 07/22] Use join to combine all points-to elements sizes --- src/analyses/base.ml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 9e35694ff8..22fce826f5 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2072,9 +2072,7 @@ struct begin match pts_sizes with | [] -> `Bot | [x] -> x - | x::xs -> List.fold_left (fun acc elem -> - if ValueDomainQueries.ID.compare acc elem >= 0 then elem else acc - ) x xs + | x::xs -> List.fold_left ValueDomainQueries.ID.join x xs end | _ -> M.warn "Pointer %a has a points-to-set of top. An invalid memory access might occur" d_exp dest; From 2534945eec78d99658cc2bf5b420af35580b7fe3 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Fri, 29 Sep 2023 17:03:45 +0200 Subject: [PATCH 08/22] Do not ingore offsets when calling BlobSize for memset/memcpy --- src/analyses/base.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 22fce826f5..255f82cb99 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2041,8 +2041,7 @@ struct | _ -> false in if points_to_heap_only then - (* Ask for BlobSize from the base address (the second field set to true) in order to avoid BlobSize giving us bot *) - ctx.ask (Queries.BlobSize {exp = dest; base_address = true}) + ctx.ask (Queries.BlobSize {exp = dest; base_address = false}) else match ctx.ask (Queries.MayPointTo dest) with | a when not (Queries.AD.is_top a) -> From 033913b760c0220d7057c830c3bfe2bc3a964069 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Fri, 29 Sep 2023 17:05:39 +0200 Subject: [PATCH 09/22] Change name to get_size_of_dest which makes more sense --- src/analyses/base.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 255f82cb99..d510389338 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2026,8 +2026,8 @@ struct M.warn ~category:(Behavior (Undefined InvalidMemoryDeallocation)) ~tags:[CWE 761] "Free of memory not at start of buffer in function %s for pointer %a" special_fn.vname d_exp ptr | _ -> M.warn ~category:MessageCategory.Analyzer "Pointer %a in function %s doesn't evaluate to a valid address." d_exp ptr special_fn.vname - (* Get the size of the smallest memory that dest points-to *) - let get_min_size_of_dest ctx dest = + (* Get the size of the memory that dest points-to *) + let get_size_of_dest ctx dest = let intdom_of_int x = ID.of_int (Cilfacade.ptrdiff_ikind ()) (Z.of_int x) in From 4ec98951e641b5862b1caebd88514e3bd4a064f0 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Fri, 29 Sep 2023 17:20:41 +0200 Subject: [PATCH 10/22] Add exception handling for ID operations --- src/analyses/base.ml | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index d510389338..01fb24d862 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2054,7 +2054,11 @@ struct let item_typ_size_in_bytes = (bitsSizeOf item_typ) / 8 in let item_typ_size_in_bytes = intdom_of_int item_typ_size_in_bytes in begin match ctx.ask (Queries.EvalLength dest) with - | `Lifted arr_len -> `Lifted (ID.mul item_typ_size_in_bytes arr_len) + | `Lifted arr_len -> + begin + try `Lifted (ID.mul item_typ_size_in_bytes arr_len) + with IntDomain.ArithmeticOnIntegerBot _ -> `Bot + end | `Bot -> `Bot | `Top -> `Top end @@ -2096,7 +2100,13 @@ struct | _, `Bot -> M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Count parameter, passed to function %s is bottom" fun_name | `Lifted ds, `Lifted en -> - begin match ID.to_bool (ID.lt ds en) with + let dest_size_lt_count = + begin + try ID.lt ds en + with IntDomain.ArithmeticOnIntegerBot _ -> ID.bot_of @@ Cilfacade.ptrdiff_ikind () + end + in + begin match ID.to_bool dest_size_lt_count with | Some true -> AnalysisState.svcomp_may_invalid_deref := true; M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of dest in function %s is %a (in bytes). Count is %a (in bytes). Memory out-of-bounds access may occur" fun_name ValueDomainQueries.ID.pretty dest_size ValueDomainQueries.ID.pretty eval_n From 1e69b64cbf7b3d93c92129e61a1173340d94125d Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Fri, 29 Sep 2023 17:21:10 +0200 Subject: [PATCH 11/22] Fix wrong name use --- src/analyses/base.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 01fb24d862..26959e6aa3 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2085,7 +2085,7 @@ struct let check_count ctx fun_name dest n = let (behavior:MessageCategory.behavior) = Undefined MemoryOutOfBoundsAccess in let cwe_number = 823 in - let dest_size = get_min_size_of_dest ctx dest in + let dest_size = get_size_of_dest ctx dest in let eval_n = ctx.ask (Queries.EvalInt n) in match dest_size, eval_n with | `Top, _ -> From 49dcac98eac518e8bd2070b542e05f1730c48970 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sat, 30 Sep 2023 00:38:35 +0200 Subject: [PATCH 12/22] Fix incompatible ikinds --- src/analyses/base.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 26959e6aa3..d56d6653c6 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2055,8 +2055,9 @@ struct let item_typ_size_in_bytes = intdom_of_int item_typ_size_in_bytes in begin match ctx.ask (Queries.EvalLength dest) with | `Lifted arr_len -> + let arr_len_casted = ID.cast_to (Cilfacade.ptrdiff_ikind ()) arr_len in begin - try `Lifted (ID.mul item_typ_size_in_bytes arr_len) + try `Lifted (ID.mul item_typ_size_in_bytes arr_len_casted) with IntDomain.ArithmeticOnIntegerBot _ -> `Bot end | `Bot -> `Bot @@ -2100,9 +2101,11 @@ struct | _, `Bot -> M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Count parameter, passed to function %s is bottom" fun_name | `Lifted ds, `Lifted en -> + let casted_ds = ID.cast_to (Cilfacade.ptrdiff_ikind ()) ds in + let casted_en = ID.cast_to (Cilfacade.ptrdiff_ikind ()) en in let dest_size_lt_count = begin - try ID.lt ds en + try ID.lt casted_ds casted_en with IntDomain.ArithmeticOnIntegerBot _ -> ID.bot_of @@ Cilfacade.ptrdiff_ikind () end in From 87dadd265c5a8af8f8087307ef31aa41de51ff56 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sat, 30 Sep 2023 23:43:27 +0200 Subject: [PATCH 13/22] Add more and more sophisticated memset and memcpy tests --- .../77-mem-oob/06-memset-memcpy-oob.c | 21 -------- tests/regression/77-mem-oob/06-memset-oob.c | 54 +++++++++++++++++++ tests/regression/77-mem-oob/07-memcpy-oob.c | 53 ++++++++++++++++++ 3 files changed, 107 insertions(+), 21 deletions(-) delete mode 100644 tests/regression/77-mem-oob/06-memset-memcpy-oob.c create mode 100644 tests/regression/77-mem-oob/06-memset-oob.c create mode 100644 tests/regression/77-mem-oob/07-memcpy-oob.c diff --git a/tests/regression/77-mem-oob/06-memset-memcpy-oob.c b/tests/regression/77-mem-oob/06-memset-memcpy-oob.c deleted file mode 100644 index 1050c199e0..0000000000 --- a/tests/regression/77-mem-oob/06-memset-memcpy-oob.c +++ /dev/null @@ -1,21 +0,0 @@ -// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval --disable warn.info -// TODO: The "--disable warn.info" part is a temporary fix and needs to be removed once the MacOS CI job is fixed -#include -#include - -int main(int argc, char const *argv[]) { - int *a = malloc(10 * sizeof(int)); //Size is 40 bytes, assuming a 4-byte int - int *b = malloc(15 * sizeof(int)); //Size is 60 bytes, assuming a 4-byte int - - memset(a, 0, 40); //NOWARN - memset(a, 0, 10 * sizeof(int)); //NOWARN - memset(a, 0, 41); //WARN - memset(a, 0, 40000000); //WARN - - memcpy(a, b, 40); //NOWARN - memcpy(a, b, 10 * sizeof(int)); //NOWARN - memcpy(a, b, 41); //WARN - memcpy(a, b, 40000000); //WARN - memcpy(a, b, 15 * sizeof(int)); //WARN - return 0; -} diff --git a/tests/regression/77-mem-oob/06-memset-oob.c b/tests/regression/77-mem-oob/06-memset-oob.c new file mode 100644 index 0000000000..931f7eaa8c --- /dev/null +++ b/tests/regression/77-mem-oob/06-memset-oob.c @@ -0,0 +1,54 @@ +// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval --disable warn.info +// TODO: The "--disable warn.info" part is a temporary fix and needs to be removed once the MacOS CI job is fixed +#include +#include +#include + +typedef struct s { + int a; + char b; +} s; + +int main(int argc, char const *argv[]) { + int *a = malloc(10 * sizeof(int)); //Size is 40 bytes, assuming a 4-byte int + + memset(a, 0, 40); //NOWARN + memset(a, 0, 10 * sizeof(int)); //NOWARN + memset(a, 0, 41); //WARN + memset(a, 0, 40000000); //WARN + + int d; + + if (argc == 15) { + int c = 55; + a = &c; + memset(a, 0, argv[5]); //WARN + } else if (argv[2] == 2) { + a = &d; + } + + memset(a, 0, 40); //WARN + + int input; + scanf("%d", &input); + memset(a, 0, input); //WARN + + + + int *b = malloc(15 * sizeof(int)); //Size is 60 bytes, assuming a 4-byte int + memset(b, 0, 60); //NOWARN + b += 1; + memset(b, 0, 60); //WARN + + + + s *s_ptr = malloc(sizeof(s)); + memset(s_ptr, 0, sizeof(s)); //NOWARN + memset(s_ptr->a, 0, sizeof(s)); //WARN + memset(s_ptr->b, 0, sizeof(s)); //WARN + + s_ptr = s_ptr->a; + memset(s_ptr, 0, sizeof(s)); //WARN + + return 0; +} diff --git a/tests/regression/77-mem-oob/07-memcpy-oob.c b/tests/regression/77-mem-oob/07-memcpy-oob.c new file mode 100644 index 0000000000..012f92996e --- /dev/null +++ b/tests/regression/77-mem-oob/07-memcpy-oob.c @@ -0,0 +1,53 @@ +// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval --disable warn.info +// TODO: The "--disable warn.info" part is a temporary fix and needs to be removed once the MacOS CI job is fixed +#include +#include + +typedef struct s { + int a; + char b; +} s; + +int main(int argc, char const *argv[]) { + int *a = malloc(10 * sizeof(int)); //Size is 40 bytes, assuming a 4-byte int + int *b = malloc(15 * sizeof(int)); //Size is 60 bytes, assuming a 4-byte int + + memcpy(a, b, 40); //NOWARN + memcpy(a, b, 10 * sizeof(int)); //NOWARN + memcpy(a, b, 41); //WARN + memcpy(a, b, 40000000); //WARN + memcpy(a, b, 15 * sizeof(int)); //WARN + + int d; + + if (*argv == 42) { + a = &d; + } else if (*(argv + 5)) { + int random = rand(); + a = &random; + memcpy(a, b, 40); //WARN + } + + memcpy(a, b, 40); //WARN + memcpy(a, b, sizeof(a)); //WARN + + memcpy(b, a, 60); //NOWARN + b += 1; + memcpy(b, a, 60); //WARN + + + s *s_ptr = malloc(sizeof(s)); + memcpy(s_ptr, a, sizeof(s)); //NOWARN + memcpy(s_ptr->a, 0, sizeof(s)); //WARN + memcpy(s_ptr->b, 0, sizeof(s)); //WARN + + memcpy(s_ptr, a, 40); //WARN + memcpy(s_ptr, a, 60); //WARN + memcpy(s_ptr, b, 40); //WARN + memcpy(s_ptr, b, 60); //WARN + + s_ptr = s_ptr->b; + memcpy(s_ptr, a, sizeof(s)); //WARN + + return 0; +} From 9e9b5e35d395a6b8e79fb186d9c5fcea68ca8db9 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sun, 1 Oct 2023 00:14:58 +0200 Subject: [PATCH 14/22] Add memset/memcpy test case with arrays --- .../77-mem-oob/08-memset-memcpy-array.c | 43 +++++++++++++++++++ 1 file changed, 43 insertions(+) create mode 100644 tests/regression/77-mem-oob/08-memset-memcpy-array.c diff --git a/tests/regression/77-mem-oob/08-memset-memcpy-array.c b/tests/regression/77-mem-oob/08-memset-memcpy-array.c new file mode 100644 index 0000000000..f231ba2dc4 --- /dev/null +++ b/tests/regression/77-mem-oob/08-memset-memcpy-array.c @@ -0,0 +1,43 @@ +// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval --disable warn.info +// TODO: The "--disable warn.info" part is a temporary fix and needs to be removed once the MacOS CI job is fixed +#include +#include + +int main(int argc, char const *argv[]) { + int arr[42]; // Size should be 168 bytes (with 4 byte ints) + int *b = arr; + + + memset(b, 0, 168); //NOWARN + memset(b, 0, sizeof(arr)); //NOWARN + memset(b, 0, 169); //WARN + memset(b, 0, sizeof(arr) + 1); //WARN + + int *c = malloc(sizeof(arr)); // Size should be 168 bytes (with 4 byte ints) + memcpy(b, c, 168); //NOWARN + memcpy(b, c, sizeof(arr)); //NOWARN + memcpy(b, c, 169); //WARN + memcpy(b, c, sizeof(arr) + 1); //WARN + + int d; + + if (*argv == 42) { + b = &d; + memset(b, 0, 168); //WARN + memcpy(b, c, 168); //WARN + } else if (*(argv + 5)) { + int random = rand(); + b = &random; + memset(b, 0, 168); //WARN + memcpy(b, c, 168); //WARN + } + + memset(b, 0, sizeof(arr)); //WARN + memcpy(b, c, sizeof(arr)); //WARN + memset(b, 0, sizeof(int)); //NOWARN + memcpy(b, c, sizeof(int)); //NOWARN + memset(b, 0, sizeof(int) + 1); //WARN + memcpy(b, c, sizeof(int) + 1); //WARN + + return 0; +} From 5ca357d3ee1412ef0d9907b966b732fda99cb927 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sun, 1 Oct 2023 17:14:55 +0200 Subject: [PATCH 15/22] Fix some bugs in memOutOfBounds and move memset/memcpy checks there --- src/analyses/base.ml | 97 ------------------- src/analyses/memOutOfBounds.ml | 170 ++++++++++++++++++++++++--------- 2 files changed, 127 insertions(+), 140 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index d56d6653c6..57c32fa3bc 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2026,99 +2026,6 @@ struct M.warn ~category:(Behavior (Undefined InvalidMemoryDeallocation)) ~tags:[CWE 761] "Free of memory not at start of buffer in function %s for pointer %a" special_fn.vname d_exp ptr | _ -> M.warn ~category:MessageCategory.Analyzer "Pointer %a in function %s doesn't evaluate to a valid address." d_exp ptr special_fn.vname - (* Get the size of the memory that dest points-to *) - let get_size_of_dest ctx dest = - let intdom_of_int x = - ID.of_int (Cilfacade.ptrdiff_ikind ()) (Z.of_int x) - in - let points_to_heap_only = - match ctx.ask (Queries.MayPointTo dest) with - | a when not (AD.is_top a) -> - AD.for_all (function - | Addr (v, _) -> ctx.ask (Queries.IsHeapVar v) - | _ -> false - ) a - | _ -> false - in - if points_to_heap_only then - ctx.ask (Queries.BlobSize {exp = dest; base_address = false}) - else - match ctx.ask (Queries.MayPointTo dest) with - | a when not (Queries.AD.is_top a) -> - let pts_list = Queries.AD.elements a in - let pts_elems_to_sizes (addr: Queries.AD.elt) = - begin match addr with - | Addr (v, _) -> - begin match v.vtype with - | TArray (item_typ, _, _) -> - let item_typ_size_in_bytes = (bitsSizeOf item_typ) / 8 in - let item_typ_size_in_bytes = intdom_of_int item_typ_size_in_bytes in - begin match ctx.ask (Queries.EvalLength dest) with - | `Lifted arr_len -> - let arr_len_casted = ID.cast_to (Cilfacade.ptrdiff_ikind ()) arr_len in - begin - try `Lifted (ID.mul item_typ_size_in_bytes arr_len_casted) - with IntDomain.ArithmeticOnIntegerBot _ -> `Bot - end - | `Bot -> `Bot - | `Top -> `Top - end - | _ -> - let type_size_in_bytes = (bitsSizeOf v.vtype) / 8 in - `Lifted (intdom_of_int type_size_in_bytes) - end - | _ -> `Top - end - in - (* Map each points-to-set element to its size *) - let pts_sizes = List.map pts_elems_to_sizes pts_list in - (* Take the smallest of all sizes that ptr's contents may have *) - begin match pts_sizes with - | [] -> `Bot - | [x] -> x - | x::xs -> List.fold_left ValueDomainQueries.ID.join x xs - end - | _ -> - M.warn "Pointer %a has a points-to-set of top. An invalid memory access might occur" d_exp dest; - `Top - - (* Used for memset() and memcpy() out-of-bounds checks *) - let check_count ctx fun_name dest n = - let (behavior:MessageCategory.behavior) = Undefined MemoryOutOfBoundsAccess in - let cwe_number = 823 in - let dest_size = get_size_of_dest ctx dest in - let eval_n = ctx.ask (Queries.EvalInt n) in - match dest_size, eval_n with - | `Top, _ -> - AnalysisState.svcomp_may_invalid_deref := true; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of dest %a in function %s is unknown. Memory out-of-bounds access might occur" d_exp dest fun_name - | _, `Top -> - AnalysisState.svcomp_may_invalid_deref := true; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Count parameter, passed to function %s is unknown. Memory out-of-bounds access might occur" fun_name - | `Bot, _ -> - AnalysisState.svcomp_may_invalid_deref := true; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of dest %a in function %s is bottom. Memory out-of-bounds access might occur" d_exp dest fun_name - | _, `Bot -> - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Count parameter, passed to function %s is bottom" fun_name - | `Lifted ds, `Lifted en -> - let casted_ds = ID.cast_to (Cilfacade.ptrdiff_ikind ()) ds in - let casted_en = ID.cast_to (Cilfacade.ptrdiff_ikind ()) en in - let dest_size_lt_count = - begin - try ID.lt casted_ds casted_en - with IntDomain.ArithmeticOnIntegerBot _ -> ID.bot_of @@ Cilfacade.ptrdiff_ikind () - end - in - begin match ID.to_bool dest_size_lt_count with - | Some true -> - AnalysisState.svcomp_may_invalid_deref := true; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of dest in function %s is %a (in bytes). Count is %a (in bytes). Memory out-of-bounds access may occur" fun_name ValueDomainQueries.ID.pretty dest_size ValueDomainQueries.ID.pretty eval_n - | Some false -> () - | None -> - AnalysisState.svcomp_may_invalid_deref := true; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Could not compare size of dest (%a) with count (%a) in function %s. Memory out-of-bounds access may occur" ID.pretty ds ID.pretty en fun_name - end - let special ctx (lv:lval option) (f: varinfo) (args: exp list) = let invalidate_ret_lv st = match lv with @@ -2187,8 +2094,6 @@ struct in let st = match desc.special args, f.vname with | Memset { dest; ch; count; }, _ -> - (* Check count *) - check_count ctx f.vname dest count; let eval_ch = eval_rv (Analyses.ask_of_ctx ctx) gs st ch in let dest_a, dest_typ = addr_type_of_exp dest in let value = @@ -2206,8 +2111,6 @@ struct let value = VD.zero_init_value dest_typ in set ~ctx (Analyses.ask_of_ctx ctx) gs st dest_a dest_typ value | Memcpy { dest = dst; src; n; }, _ -> - (* Check n *) - check_count ctx f.vname dst n; memory_copying dst src (* strcpy(dest, src); *) | Strcpy { dest = dst; src; n = None }, _ -> diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index 94c16e9c94..ae0faedb9a 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -6,6 +6,7 @@ open MessageCategory module AS = AnalysisState module VDQ = ValueDomainQueries +module ID = IntDomain.IntDomTuple (* Note: @@ -27,11 +28,11 @@ struct (* HELPER FUNCTIONS *) let intdom_of_int x = - IntDomain.IntDomTuple.of_int (Cilfacade.ptrdiff_ikind ()) (Z.of_int x) + ID.of_int (Cilfacade.ptrdiff_ikind ()) (Z.of_int x) let to_index ?typ offs = let idx_of_int x = - IntDomain.IntDomTuple.of_int (Cilfacade.ptrdiff_ikind ()) (Z.of_int (x / 8)) + ID.of_int (Cilfacade.ptrdiff_ikind ()) (Z.of_int (x / 8)) in let rec offset_to_index_offset ?typ offs = match offs with | `NoOffset -> idx_of_int 0 @@ -40,7 +41,7 @@ struct let bits_offset, _size = GoblintCil.bitsOffset (TComp (field.fcomp, [])) field_as_offset in let bits_offset = idx_of_int bits_offset in let remaining_offset = offset_to_index_offset ~typ:field.ftype o in - IntDomain.IntDomTuple.add bits_offset remaining_offset + ID.add bits_offset remaining_offset | `Index (x, o) -> let (item_typ, item_size_in_bits) = match Option.map unrollType typ with @@ -48,11 +49,11 @@ struct let item_size_in_bits = bitsSizeOf item_typ in (Some item_typ, idx_of_int item_size_in_bits) | _ -> - (None, IntDomain.IntDomTuple.top_of @@ Cilfacade.ptrdiff_ikind ()) + (None, ID.top_of @@ Cilfacade.ptrdiff_ikind ()) in - let bits_offset = IntDomain.IntDomTuple.mul item_size_in_bits x in + let bits_offset = ID.mul item_size_in_bits x in let remaining_offset = offset_to_index_offset ?typ:item_typ o in - IntDomain.IntDomTuple.add bits_offset remaining_offset + ID.add bits_offset remaining_offset in offset_to_index_offset ?typ offs @@ -115,30 +116,33 @@ struct let item_typ_size_in_bytes = (bitsSizeOf item_typ) / 8 in let item_typ_size_in_bytes = intdom_of_int item_typ_size_in_bytes in begin match ctx.ask (Queries.EvalLength ptr) with - | `Lifted arr_len -> `Lifted (IntDomain.IntDomTuple.mul item_typ_size_in_bytes arr_len) - | `Bot -> VDQ.ID.bot () - | `Top -> VDQ.ID.top () + | `Lifted arr_len -> + let arr_len_casted = ID.cast_to (Cilfacade.ptrdiff_ikind ()) arr_len in + begin + try `Lifted (ID.mul item_typ_size_in_bytes arr_len_casted) + with IntDomain.ArithmeticOnIntegerBot _ -> `Bot + end + | `Bot -> `Bot + | `Top -> `Top end | _ -> let type_size_in_bytes = (bitsSizeOf v.vtype) / 8 in `Lifted (intdom_of_int type_size_in_bytes) end - | _ -> VDQ.ID.top () + | _ -> `Top end in (* Map each points-to-set element to its size *) let pts_sizes = List.map pts_elems_to_sizes pts_list in (* Take the smallest of all sizes that ptr's contents may have *) begin match pts_sizes with - | [] -> VDQ.ID.bot () + | [] -> `Bot | [x] -> x - | x::xs -> List.fold_left (fun acc elem -> - if VDQ.ID.compare acc elem >= 0 then elem else acc - ) x xs + | x::xs -> List.fold_left VDQ.ID.join x xs end | _ -> M.warn "Pointer %a has a points-to-set of top. An invalid memory access might occur" d_exp ptr; - VDQ.ID.top () + `Top let get_ptr_deref_type ptr_typ = match ptr_typ with @@ -155,7 +159,7 @@ struct let eval_offset = VDQ.ID.of_int (Cilfacade.ptrdiff_ikind ()) eval_offset in let ptr_contents_typ_size_in_bytes = size_of_type_in_bytes ptr_contents_typ in match eval_offset with - | `Lifted i -> `Lifted (IntDomain.IntDomTuple.mul i ptr_contents_typ_size_in_bytes) + | `Lifted i -> `Lifted (ID.mul i ptr_contents_typ_size_in_bytes) | `Top -> `Top | `Bot -> `Bot @@ -167,12 +171,12 @@ struct let bits_offset, _size = GoblintCil.bitsOffset (TComp (field.fcomp, [])) field_as_offset in let bytes_offset = intdom_of_int (bits_offset / 8) in let remaining_offset = offs_to_idx field.ftype o in - IntDomain.IntDomTuple.add bytes_offset remaining_offset + ID.add bytes_offset remaining_offset | `Index (x, o) -> let typ_size_in_bytes = size_of_type_in_bytes typ in - let bytes_offset = IntDomain.IntDomTuple.mul typ_size_in_bytes x in + let bytes_offset = ID.mul typ_size_in_bytes x in let remaining_offset = offs_to_idx typ o in - IntDomain.IntDomTuple.add bytes_offset remaining_offset + ID.add bytes_offset remaining_offset let rec get_addr_offs ctx ptr = match ctx.ask (Queries.MayPointTo ptr) with @@ -183,17 +187,17 @@ struct begin match VDQ.AD.is_empty a with | true -> M.warn "Pointer %a has an empty points-to-set" d_exp ptr; - IntDomain.IntDomTuple.top_of @@ Cilfacade.ptrdiff_ikind () + ID.top_of @@ Cilfacade.ptrdiff_ikind () | false -> if VDQ.AD.exists (function - | Addr (_, o) -> IntDomain.IntDomTuple.is_bot @@ offs_to_idx t o + | Addr (_, o) -> ID.is_bot @@ offs_to_idx t o | _ -> false ) a then ( (* TODO: Uncomment once staging-memsafety branch changes are applied *) (* set_mem_safety_flag InvalidDeref; *) M.warn "Pointer %a has a bot address offset. An invalid memory access may occur" d_exp ptr ) else if VDQ.AD.exists (function - | Addr (_, o) -> IntDomain.IntDomTuple.is_bot @@ offs_to_idx t o + | Addr (_, o) -> ID.is_bot @@ offs_to_idx t o | _ -> false ) a then ( (* TODO: Uncomment once staging-memsafety branch changes are applied *) @@ -204,16 +208,16 @@ struct (* Hence, we can just pick one element and obtain its offset *) begin match VDQ.AD.choose a with | Addr (_, o) -> offs_to_idx t o - | _ -> IntDomain.IntDomTuple.top_of @@ Cilfacade.ptrdiff_ikind () + | _ -> ID.top_of @@ Cilfacade.ptrdiff_ikind () end end | None -> M.error "Expression %a doesn't have pointer type" d_exp ptr; - IntDomain.IntDomTuple.top_of @@ Cilfacade.ptrdiff_ikind () + ID.top_of @@ Cilfacade.ptrdiff_ikind () end | _ -> M.warn "Pointer %a has a points-to-set of top. An invalid memory access might occur" d_exp ptr; - IntDomain.IntDomTuple.top_of @@ Cilfacade.ptrdiff_ikind () + ID.top_of @@ Cilfacade.ptrdiff_ikind () and check_lval_for_oob_access ctx ?(is_implicitly_derefed = false) lval = if not @@ lval_contains_a_ptr lval then () @@ -242,15 +246,30 @@ struct let ptr_contents_type = get_ptr_deref_type ptr_type in match ptr_contents_type with | Some t -> - begin match VDQ.ID.is_top ptr_size with - | true -> + begin match ptr_size, addr_offs with + | `Top, _ -> AS.svcomp_may_invalid_deref := true; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer %a not known. Memory out-of-bounds access might occur due to pointer arithmetic" d_exp lval_exp - | false -> - let offs = `Lifted addr_offs in - if ptr_size < offs then begin - AS.svcomp_may_invalid_deref := true; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer is %a (in bytes). It is offset by %a (in bytes) due to pointer arithmetic. Memory out-of-bounds access must occur" VDQ.ID.pretty ptr_size VDQ.ID.pretty offs + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer %a is top. Memory out-of-bounds access might occur due to pointer arithmetic" d_exp lval_exp + | `Bot, _ -> + AS.svcomp_may_invalid_deref := true; + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer %a is bot. Memory out-of-bounds access might occur due to pointer arithmetic" d_exp lval_exp + | `Lifted ps, ao -> + let casted_ps = ID.cast_to (Cilfacade.ptrdiff_ikind ()) ps in + let casted_ao = ID.cast_to (Cilfacade.ptrdiff_ikind ()) ao in + let ptr_size_lt_offs = + begin + try ID.lt casted_ps casted_ao + with IntDomain.ArithmeticOnIntegerBot _ -> ID.bot_of @@ Cilfacade.ptrdiff_ikind () + end + in + begin match ID.to_bool ptr_size_lt_offs with + | Some true -> + AnalysisState.svcomp_may_invalid_deref := true; + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer is %a (in bytes). It is offset by %a (in bytes) due to pointer arithmetic. Memory out-of-bounds access must occur" ID.pretty casted_ps ID.pretty casted_ao + | Some false -> () + | None -> + AnalysisState.svcomp_may_invalid_deref := true; + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Could not compare size of pointer (%a) (in bytes) with offset by (%a) (in bytes). Memory out-of-bounds access might occur" ID.pretty casted_ps ID.pretty casted_ao end end | _ -> M.error "Expression %a is not a pointer" d_exp lval_exp @@ -296,27 +315,87 @@ struct let offset_size = eval_ptr_offset_in_binop ctx e2 t in (* Make sure to add the address offset to the binop offset *) let offset_size_with_addr_size = match offset_size with - | `Lifted os -> `Lifted (IntDomain.IntDomTuple.add os addr_offs) + | `Lifted os -> + let casted_os = ID.cast_to (Cilfacade.ptrdiff_ikind ()) os in + let casted_ao = ID.cast_to (Cilfacade.ptrdiff_ikind ()) addr_offs in + `Lifted (ID.add casted_os casted_ao) | `Top -> `Top | `Bot -> `Bot in - begin match VDQ.ID.is_top ptr_size, VDQ.ID.is_top offset_size_with_addr_size with - | true, _ -> + begin match ptr_size, offset_size_with_addr_size with + | `Top, _ -> + AS.svcomp_may_invalid_deref := true; + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer %a in expression %a is top. Memory out-of-bounds access might occur" d_exp e1 d_exp binopexp + | _, `Top -> AS.svcomp_may_invalid_deref := true; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer %a in expression %a not known. Memory out-of-bounds access might occur" d_exp e1 d_exp binopexp - | _, true -> + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Operand value for pointer arithmetic in expression %a is top. Memory out-of-bounds access might occur" d_exp binopexp + | `Bot, _ -> AS.svcomp_may_invalid_deref := true; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Operand value for pointer arithmetic in expression %a not known. Memory out-of-bounds access might occur" d_exp binopexp - | false, false -> - if ptr_size < offset_size_with_addr_size then begin - AS.svcomp_may_invalid_deref := true; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer in expression %a is %a (in bytes). It is offset by %a (in bytes). Memory out-of-bounds access must occur" d_exp binopexp VDQ.ID.pretty ptr_size VDQ.ID.pretty offset_size_with_addr_size + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer %a in expression %a is bottom. Memory out-of-bounds access might occur" d_exp e1 d_exp binopexp + | _, `Bot -> + AS.svcomp_may_invalid_deref := true; + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Operand value for pointer arithmetic in expression %a is bottom. Memory out-of-bounds access might occur" d_exp binopexp + | `Lifted ps, `Lifted o -> + let casted_ps = ID.cast_to (Cilfacade.ptrdiff_ikind ()) ps in + let casted_o = ID.cast_to (Cilfacade.ptrdiff_ikind ()) o in + let ptr_size_lt_offs = + begin + try ID.lt casted_ps casted_o + with IntDomain.ArithmeticOnIntegerBot _ -> ID.bot_of @@ Cilfacade.ptrdiff_ikind () + end + in + begin match ID.to_bool ptr_size_lt_offs with + | Some true -> + AS.svcomp_may_invalid_deref := true; + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer in expression %a is %a (in bytes). It is offset by %a (in bytes). Memory out-of-bounds access must occur" d_exp binopexp ID.pretty casted_ps ID.pretty casted_o + | Some false -> () + | None -> + AnalysisState.svcomp_may_invalid_deref := true; + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Could not compare pointer size (%a) with offset (%a). Memory out-of-bounds access may occur" ID.pretty casted_ps ID.pretty casted_o end end | _ -> M.error "Binary expression %a doesn't have a pointer" d_exp binopexp end | _ -> () + let check_count ctx fun_name dest n = + let (behavior:MessageCategory.behavior) = Undefined MemoryOutOfBoundsAccess in + let cwe_number = 823 in + let dest_size = get_size_of_ptr_target ctx dest in + let eval_n = ctx.ask (Queries.EvalInt n) in + let addr_offs = get_addr_offs ctx dest in + match dest_size, eval_n with + | `Top, _ -> + AnalysisState.svcomp_may_invalid_deref := true; + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of dest %a in function %s is unknown. Memory out-of-bounds access might occur" d_exp dest fun_name + | _, `Top -> + AnalysisState.svcomp_may_invalid_deref := true; + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Count parameter, passed to function %s is unknown. Memory out-of-bounds access might occur" fun_name + | `Bot, _ -> + AnalysisState.svcomp_may_invalid_deref := true; + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of dest %a in function %s is bottom. Memory out-of-bounds access might occur" d_exp dest fun_name + | _, `Bot -> + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Count parameter, passed to function %s is bottom" fun_name + | `Lifted ds, `Lifted en -> + let casted_ds = ID.cast_to (Cilfacade.ptrdiff_ikind ()) ds in + let casted_en = ID.cast_to (Cilfacade.ptrdiff_ikind ()) en in + let casted_ao = ID.cast_to (Cilfacade.ptrdiff_ikind ()) addr_offs in + let dest_size_lt_count = + begin + try ID.lt casted_ds (ID.add casted_en casted_ao) + with IntDomain.ArithmeticOnIntegerBot _ -> ID.bot_of @@ Cilfacade.ptrdiff_ikind () + end + in + begin match ID.to_bool dest_size_lt_count with + | Some true -> + AnalysisState.svcomp_may_invalid_deref := true; + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of dest in function %s is %a (in bytes) with an address offset of %a (in bytes). Count is %a (in bytes). Memory out-of-bounds access may occur" fun_name ID.pretty casted_ds ID.pretty casted_ao ID.pretty casted_en + | Some false -> () + | None -> + AnalysisState.svcomp_may_invalid_deref := true; + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Could not compare size of dest (%a) with address offset (%a) count (%a) in function %s. Memory out-of-bounds access may occur" ID.pretty casted_ds ID.pretty casted_ao ID.pretty casted_en fun_name + end + (* TRANSFER FUNCTIONS *) @@ -344,6 +423,11 @@ struct in Option.iter (fun x -> check_lval_for_oob_access ctx x) lval; List.iter (fun arg -> check_exp_for_oob_access ctx ~is_implicitly_derefed:(is_arg_implicitly_derefed arg) arg) arglist; + (* Check calls to memset and memcpy for out-of-bounds-accesses *) + match desc.special arglist with + | Memset { dest; ch; count; } -> check_count ctx f.vname dest count; + | Memcpy { dest; src; n = count; } -> check_count ctx f.vname dest count; + | _ -> (); ctx.local let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list = From 8bf3705240f1ae479f71f4eaf9346c87768d856b Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sun, 1 Oct 2023 17:16:14 +0200 Subject: [PATCH 16/22] Remove unused function --- src/analyses/memOutOfBounds.ml | 27 --------------------------- 1 file changed, 27 deletions(-) diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index ae0faedb9a..f9a0439333 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -30,33 +30,6 @@ struct let intdom_of_int x = ID.of_int (Cilfacade.ptrdiff_ikind ()) (Z.of_int x) - let to_index ?typ offs = - let idx_of_int x = - ID.of_int (Cilfacade.ptrdiff_ikind ()) (Z.of_int (x / 8)) - in - let rec offset_to_index_offset ?typ offs = match offs with - | `NoOffset -> idx_of_int 0 - | `Field (field, o) -> - let field_as_offset = Field (field, NoOffset) in - let bits_offset, _size = GoblintCil.bitsOffset (TComp (field.fcomp, [])) field_as_offset in - let bits_offset = idx_of_int bits_offset in - let remaining_offset = offset_to_index_offset ~typ:field.ftype o in - ID.add bits_offset remaining_offset - | `Index (x, o) -> - let (item_typ, item_size_in_bits) = - match Option.map unrollType typ with - | Some TArray(item_typ, _, _) -> - let item_size_in_bits = bitsSizeOf item_typ in - (Some item_typ, idx_of_int item_size_in_bits) - | _ -> - (None, ID.top_of @@ Cilfacade.ptrdiff_ikind ()) - in - let bits_offset = ID.mul item_size_in_bits x in - let remaining_offset = offset_to_index_offset ?typ:item_typ o in - ID.add bits_offset remaining_offset - in - offset_to_index_offset ?typ offs - let rec exp_contains_a_ptr (exp:exp) = match exp with | Const _ From 30279106115eed26c94a2b84bc5cf14d153c3400 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sun, 1 Oct 2023 17:42:51 +0200 Subject: [PATCH 17/22] Add further exception handling --- src/analyses/memOutOfBounds.ml | 31 ++++++++++++++++++++++--------- 1 file changed, 22 insertions(+), 9 deletions(-) diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index f9a0439333..f2b2780f58 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -128,11 +128,14 @@ struct let eval_ptr_offset_in_binop ctx exp ptr_contents_typ = let eval_offset = ctx.ask (Queries.EvalInt exp) in - let eval_offset = Option.get @@ VDQ.ID.to_int eval_offset in - let eval_offset = VDQ.ID.of_int (Cilfacade.ptrdiff_ikind ()) eval_offset in let ptr_contents_typ_size_in_bytes = size_of_type_in_bytes ptr_contents_typ in match eval_offset with - | `Lifted i -> `Lifted (ID.mul i ptr_contents_typ_size_in_bytes) + | `Lifted eo -> + let casted_eo = ID.cast_to (Cilfacade.ptrdiff_ikind ()) eo in + begin + try `Lifted (ID.mul casted_eo ptr_contents_typ_size_in_bytes) + with IntDomain.ArithmeticOnIntegerBot _ -> `Bot + end | `Top -> `Top | `Bot -> `Bot @@ -144,12 +147,18 @@ struct let bits_offset, _size = GoblintCil.bitsOffset (TComp (field.fcomp, [])) field_as_offset in let bytes_offset = intdom_of_int (bits_offset / 8) in let remaining_offset = offs_to_idx field.ftype o in - ID.add bytes_offset remaining_offset + begin + try ID.add bytes_offset remaining_offset + with IntDomain.ArithmeticOnIntegerBot _ -> ID.bot_of @@ Cilfacade.ptrdiff_ikind () + end | `Index (x, o) -> - let typ_size_in_bytes = size_of_type_in_bytes typ in - let bytes_offset = ID.mul typ_size_in_bytes x in - let remaining_offset = offs_to_idx typ o in - ID.add bytes_offset remaining_offset + begin try + let typ_size_in_bytes = size_of_type_in_bytes typ in + let bytes_offset = ID.mul typ_size_in_bytes x in + let remaining_offset = offs_to_idx typ o in + ID.add bytes_offset remaining_offset + with IntDomain.ArithmeticOnIntegerBot _ -> ID.bot_of @@ Cilfacade.ptrdiff_ikind () + end let rec get_addr_offs ctx ptr = match ctx.ask (Queries.MayPointTo ptr) with @@ -291,7 +300,10 @@ struct | `Lifted os -> let casted_os = ID.cast_to (Cilfacade.ptrdiff_ikind ()) os in let casted_ao = ID.cast_to (Cilfacade.ptrdiff_ikind ()) addr_offs in - `Lifted (ID.add casted_os casted_ao) + begin + try `Lifted (ID.add casted_os casted_ao) + with IntDomain.ArithmeticOnIntegerBot _ -> `Bot + end | `Top -> `Top | `Bot -> `Bot in @@ -331,6 +343,7 @@ struct end | _ -> () + (* For memset() and memcpy() *) let check_count ctx fun_name dest n = let (behavior:MessageCategory.behavior) = Undefined MemoryOutOfBoundsAccess in let cwe_number = 823 in From 62b20a2839a4df6b24b1e2908893e51daa2e2e7b Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sun, 1 Oct 2023 17:43:49 +0200 Subject: [PATCH 18/22] Add further memset/memcpy test --- .../77-mem-oob/09-memset-memcpy-addr-offs.c | 20 +++++++++++++++++++ 1 file changed, 20 insertions(+) create mode 100644 tests/regression/77-mem-oob/09-memset-memcpy-addr-offs.c diff --git a/tests/regression/77-mem-oob/09-memset-memcpy-addr-offs.c b/tests/regression/77-mem-oob/09-memset-memcpy-addr-offs.c new file mode 100644 index 0000000000..725024946e --- /dev/null +++ b/tests/regression/77-mem-oob/09-memset-memcpy-addr-offs.c @@ -0,0 +1,20 @@ +// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval --disable warn.info +// TODO: The "--disable warn.info" part is a temporary fix and needs to be removed once the MacOS CI job is fixed +#include +#include + +int main(int argc, char const *argv[]) { + int *a = malloc(10 * sizeof(int)); //Size is 40 bytes, assuming a 4-byte int + int *b = malloc(15 * sizeof(int)); //Size is 60 bytes, assuming a 4-byte int + + memset(a, 0, 40); //NOWARN + memcpy(a, b, 40); //NOWARN + + a += 3; + + memset(a, 0, 40); //WARN + memcpy(a, b, 40); //WARN + + memset(a, 0, 37); //NOWARN + memcpy(a, b, 37); //NOWARN +} \ No newline at end of file From 5e683d45c059370eb2fd496073378bcb6232b015 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sun, 1 Oct 2023 17:46:14 +0200 Subject: [PATCH 19/22] Fix comment --- src/analyses/memOutOfBounds.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index f2b2780f58..fe4b854923 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -375,7 +375,7 @@ struct begin match ID.to_bool dest_size_lt_count with | Some true -> AnalysisState.svcomp_may_invalid_deref := true; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of dest in function %s is %a (in bytes) with an address offset of %a (in bytes). Count is %a (in bytes). Memory out-of-bounds access may occur" fun_name ID.pretty casted_ds ID.pretty casted_ao ID.pretty casted_en + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of dest in function %s is %a (in bytes) with an address offset of %a (in bytes). Count is %a (in bytes). Memory out-of-bounds access must occur" fun_name ID.pretty casted_ds ID.pretty casted_ao ID.pretty casted_en | Some false -> () | None -> AnalysisState.svcomp_may_invalid_deref := true; From f03f81ff2ba28715e677c49507b2edea168f3b37 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sun, 1 Oct 2023 18:16:00 +0200 Subject: [PATCH 20/22] Remove some bot checks for ID arithmetic --- src/analyses/memOutOfBounds.ml | 21 +++------------------ 1 file changed, 3 insertions(+), 18 deletions(-) diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index fe4b854923..45048acc93 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -238,12 +238,7 @@ struct | `Lifted ps, ao -> let casted_ps = ID.cast_to (Cilfacade.ptrdiff_ikind ()) ps in let casted_ao = ID.cast_to (Cilfacade.ptrdiff_ikind ()) ao in - let ptr_size_lt_offs = - begin - try ID.lt casted_ps casted_ao - with IntDomain.ArithmeticOnIntegerBot _ -> ID.bot_of @@ Cilfacade.ptrdiff_ikind () - end - in + let ptr_size_lt_offs = ID.lt casted_ps casted_ao in begin match ID.to_bool ptr_size_lt_offs with | Some true -> AnalysisState.svcomp_may_invalid_deref := true; @@ -323,12 +318,7 @@ struct | `Lifted ps, `Lifted o -> let casted_ps = ID.cast_to (Cilfacade.ptrdiff_ikind ()) ps in let casted_o = ID.cast_to (Cilfacade.ptrdiff_ikind ()) o in - let ptr_size_lt_offs = - begin - try ID.lt casted_ps casted_o - with IntDomain.ArithmeticOnIntegerBot _ -> ID.bot_of @@ Cilfacade.ptrdiff_ikind () - end - in + let ptr_size_lt_offs = ID.lt casted_ps casted_o in begin match ID.to_bool ptr_size_lt_offs with | Some true -> AS.svcomp_may_invalid_deref := true; @@ -366,12 +356,7 @@ struct let casted_ds = ID.cast_to (Cilfacade.ptrdiff_ikind ()) ds in let casted_en = ID.cast_to (Cilfacade.ptrdiff_ikind ()) en in let casted_ao = ID.cast_to (Cilfacade.ptrdiff_ikind ()) addr_offs in - let dest_size_lt_count = - begin - try ID.lt casted_ds (ID.add casted_en casted_ao) - with IntDomain.ArithmeticOnIntegerBot _ -> ID.bot_of @@ Cilfacade.ptrdiff_ikind () - end - in + let dest_size_lt_count = ID.lt casted_ds (ID.add casted_en casted_ao) in begin match ID.to_bool dest_size_lt_count with | Some true -> AnalysisState.svcomp_may_invalid_deref := true; From 3da92055ae48f55f827aed5e4f8eae0b2102e009 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sun, 1 Oct 2023 18:33:38 +0200 Subject: [PATCH 21/22] Use size_of_type_in_bytes where possible --- src/analyses/memOutOfBounds.ml | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index 45048acc93..7015e6f143 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -30,6 +30,10 @@ struct let intdom_of_int x = ID.of_int (Cilfacade.ptrdiff_ikind ()) (Z.of_int x) + let size_of_type_in_bytes typ = + let typ_size_in_bytes = (bitsSizeOf typ) / 8 in + intdom_of_int typ_size_in_bytes + let rec exp_contains_a_ptr (exp:exp) = match exp with | Const _ @@ -86,8 +90,7 @@ struct | Addr (v, _) -> begin match v.vtype with | TArray (item_typ, _, _) -> - let item_typ_size_in_bytes = (bitsSizeOf item_typ) / 8 in - let item_typ_size_in_bytes = intdom_of_int item_typ_size_in_bytes in + let item_typ_size_in_bytes = size_of_type_in_bytes item_typ in begin match ctx.ask (Queries.EvalLength ptr) with | `Lifted arr_len -> let arr_len_casted = ID.cast_to (Cilfacade.ptrdiff_ikind ()) arr_len in @@ -99,8 +102,8 @@ struct | `Top -> `Top end | _ -> - let type_size_in_bytes = (bitsSizeOf v.vtype) / 8 in - `Lifted (intdom_of_int type_size_in_bytes) + let type_size_in_bytes = size_of_type_in_bytes v.vtype in + `Lifted type_size_in_bytes end | _ -> `Top end @@ -122,10 +125,6 @@ struct | TPtr (t, _) -> Some t | _ -> None - let size_of_type_in_bytes typ = - let typ_size_in_bytes = (bitsSizeOf typ) / 8 in - intdom_of_int typ_size_in_bytes - let eval_ptr_offset_in_binop ctx exp ptr_contents_typ = let eval_offset = ctx.ask (Queries.EvalInt exp) in let ptr_contents_typ_size_in_bytes = size_of_type_in_bytes ptr_contents_typ in From 89abb1a9ade5352f19fc2c042c4ef2b387c5fa38 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sun, 1 Oct 2023 20:56:16 +0200 Subject: [PATCH 22/22] Keep TODO about count of memset in base.ml --- src/analyses/base.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 57c32fa3bc..232ee36d68 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2094,6 +2094,7 @@ struct in let st = match desc.special args, f.vname with | Memset { dest; ch; count; }, _ -> + (* TODO: check count *) let eval_ch = eval_rv (Analyses.ask_of_ctx ctx) gs st ch in let dest_a, dest_typ = addr_type_of_exp dest in let value =