From ace3a0b4c9cce3bfb1590f7d9b89342ff953bbe9 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Thu, 11 May 2023 11:10:47 +0200 Subject: [PATCH 01/53] Initial skeleton for a UAF analysis --- src/analyses/useAfterFree.ml | 47 ++++++++++++++++++++++++++++++++++++ 1 file changed, 47 insertions(+) create mode 100644 src/analyses/useAfterFree.ml diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml new file mode 100644 index 0000000000..b69212660d --- /dev/null +++ b/src/analyses/useAfterFree.ml @@ -0,0 +1,47 @@ +(** An analysis for the detection of use-after-free vulnerabilities. *) + +open GoblintCil +open Analyses + +module Spec : Analyses.MCPSpec = +struct + include Analyses.DefaultSpec + + let name () = "useafterfree" + module D = Lattice.Unit + module C = Lattice.Unit + + let assign ctx (lval:lval) (rval:exp) : D.t = + ctx.local + + let branch ctx (exp:exp) (tv:bool) : D.t = + ctx.local + + let body ctx (f:fundec) : D.t = + ctx.local + + let return ctx (exp:exp option) (f:fundec) : D.t = + ctx.local + + let enter ctx (lval:lval option) (f:fundec) (args:exp list) : (D.t * D.t) list = + [ctx.local, ctx.local] + + let combine_env ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (callee_local:D.t) (f_ask:Queries.ask) : D.t = + callee_local + + let combine_assign ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (callee_local:D.t) (f_ask: Queries.ask): D.t = + ctx.local + + let special ctx (lval:lval option) (f:varinfo) (arglist:exp list) : D.t = + ctx.local + + let threadenter ctx lval f args = [ctx.local] + let threadspawn ctx lval f args fctx = ctx.local + + let startstate v = D.bot () + let exitstate v = D.top () + +end + +let _ = + MCP.register_analysis (module Spec : MCPSpec) \ No newline at end of file From c34181de738afd3ee404a519d23ddf0a07e38b59 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Wed, 17 May 2023 09:24:50 +0200 Subject: [PATCH 02/53] Add "free" as a special function --- src/analyses/libraryDesc.ml | 2 ++ src/analyses/libraryFunctions.ml | 9 ++++++++- 2 files changed, 10 insertions(+), 1 deletion(-) diff --git a/src/analyses/libraryDesc.ml b/src/analyses/libraryDesc.ml index a477fc1809..4f83a06763 100644 --- a/src/analyses/libraryDesc.ml +++ b/src/analyses/libraryDesc.ml @@ -45,6 +45,7 @@ type special = | Malloc of Cil.exp | Calloc of { count: Cil.exp; size: Cil.exp; } | Realloc of { ptr: Cil.exp; size: Cil.exp; } + | Free of Cil.exp | Assert of { exp: Cil.exp; check: bool; refine: bool; } | Lock of { lock: Cil.exp; try_: bool; write: bool; return_on_success: bool; } | Unlock of Cil.exp @@ -122,6 +123,7 @@ let special_of_old classify_name = fun args -> | `Malloc e -> Malloc e | `Calloc (count, size) -> Calloc { count; size; } | `Realloc (ptr, size) -> Realloc { ptr; size; } + | `Free ptr -> Free ptr | `Lock (try_, write, return_on_success) -> begin match args with | [lock] -> Lock { lock ; try_; write; return_on_success; } diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 814de845b2..c23b098176 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -19,6 +19,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("strcpy", special [__ "dest" [w]; __ "src" [r]] @@ fun dest src -> Strcpy { dest; src }); ("malloc", special [__ "size" []] @@ fun size -> Malloc size); ("realloc", special [__ "ptr" [r; f]; __ "size" []] @@ fun ptr size -> Realloc { ptr; size }); + ("free", special [__ "ptr" [r; f]] @@ fun ptr -> Free ptr); ("abort", special [] Abort); ("exit", special [drop "exit_code" []] Abort); ("ungetc", unknown [drop "c" []; drop "stream" [r; w]]); @@ -292,7 +293,7 @@ let goblint_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ let zstd_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("ZSTD_customMalloc", special [__ "size" []; drop "customMem" [r]] @@ fun size -> Malloc size); ("ZSTD_customCalloc", special [__ "size" []; drop "customMem" [r]] @@ fun size -> Calloc { size; count = Cil.one }); - ("ZSTD_customFree", unknown [drop "ptr" [f]; drop "customMem" [r]]); + ("ZSTD_customFree", special [__ "ptr" [f]; drop "customMem" [r]] @@ fun ptr -> Free ptr); ] (** math functions. @@ -454,6 +455,7 @@ type categories = [ | `Malloc of exp | `Calloc of exp * exp | `Realloc of exp * exp + | `Free of exp | `Lock of bool * bool * bool (* try? * write? * return on success *) | `Unlock | `ThreadCreate of exp * exp * exp (* id * f * x *) @@ -487,6 +489,11 @@ let classify fn exps: categories = | n::size::_ -> `Calloc (n, size) | _ -> strange_arguments () end + | "kfree" | "usb_free_urb" -> + begin match exps with + | ptr::_ -> `Free ptr + | _ -> strange_arguments () + end | "_spin_trylock" | "spin_trylock" | "mutex_trylock" | "_spin_trylock_irqsave" | "down_trylock" -> `Lock(true, true, true) From 392b77cba67797659b3e749aa03cd42c565396ce Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Wed, 17 May 2023 09:44:27 +0200 Subject: [PATCH 03/53] Add TODO comment in classify for free-related functions --- src/analyses/libraryFunctions.ml | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index c23b098176..bea7f3d3f7 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -489,6 +489,11 @@ let classify fn exps: categories = | n::size::_ -> `Calloc (n, size) | _ -> strange_arguments () end + (* + * TODO: Docs (https://goblint.readthedocs.io/en/latest/developer-guide/extending-library/#library-function-specifications) + * say we shouldn't add new specifications in classify + * Should I remove the guard for "free"-related functions here in this case? + *) | "kfree" | "usb_free_urb" -> begin match exps with | ptr::_ -> `Free ptr From f9f65b7da26c4b496ca0ba44bdceb1402310ce55 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Wed, 17 May 2023 09:58:35 +0200 Subject: [PATCH 04/53] Add another TODO comment for free special function --- src/analyses/libraryFunctions.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index bea7f3d3f7..c46ee81746 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -19,6 +19,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("strcpy", special [__ "dest" [w]; __ "src" [r]] @@ fun dest src -> Strcpy { dest; src }); ("malloc", special [__ "size" []] @@ fun size -> Malloc size); ("realloc", special [__ "ptr" [r; f]; __ "size" []] @@ fun ptr size -> Realloc { ptr; size }); + (* TODO: Do we need accessKind of "r" for "free" or is "f" alone already sufficient? *) ("free", special [__ "ptr" [r; f]] @@ fun ptr -> Free ptr); ("abort", special [] Abort); ("exit", special [drop "exit_code" []] Abort); From 199d2d253cfd4af565cd7523a490826133cbbff2 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Wed, 17 May 2023 14:06:52 +0200 Subject: [PATCH 05/53] First iteration of UAF analysis implementation --- src/analyses/useAfterFree.ml | 155 +++++++++++++++++++++++++++++++++-- 1 file changed, 148 insertions(+), 7 deletions(-) diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index b69212660d..21730e6193 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -8,32 +8,173 @@ struct include Analyses.DefaultSpec let name () = "useafterfree" - module D = Lattice.Unit + (* module D = Lattice.Unit *) + module D = SetDomain.Make(ValueDomain.Blobs) module C = Lattice.Unit + (** TODO: What about context-sensitivity? *) + let context _ _ = () + + + (* HELPER FUNCTIONS *) + + let check_exp (exp:exp) ctx = + let state = ctx.local in + match ctx.ask (Queries.EvalValue exp) with + | a when not (Queries.VD.is_top a) -> + begin match a with + | `Blob (v, s, t) -> if D.mem (v, s, t) state then true else false + | _ -> false + end + | _ -> false + + let check_lval (lval:lval) ctx = + let state = ctx.local in + match lval with + | (Mem e, _) -> + begin match ctx.ask (Queries.EvalValue e) with + | a when not (Queries.VD.is_top a) -> + begin match a with + | `Blob (v, s, t) -> if D.mem (v, s, t) state then true else false + | _ -> false + end + | _ -> false + end + | _ -> false + + + (* TRANSFER FUNCTIONS *) + let assign ctx (lval:lval) (rval:exp) : D.t = - ctx.local + let state = ctx.local in + (* Intuition: + * Check if lval and/or lval has an expression that points to a "maybe freed" blob + * If yes -> send out a WARNING; otherwise -> don't WARN + * In either case above -> don't change the CFG node's state + *) + match check_lval lval ctx, check_exp rval ctx with + | true, true -> M.warn "WARN: lval and rval contain maybe freed blob"; state + | false, true -> M.warn "WARN: rval contains maybe freed blob"; state + | true, false -> M.warn "WARN: lval contains maybe freed blob"; state + | false, false -> state let branch ctx (exp:exp) (tv:bool) : D.t = - ctx.local + let state = ctx.local in + if check_exp exp ctx then + M.warn "WARN: branch exp contains maybe freed blob"; + state let body ctx (f:fundec) : D.t = ctx.local let return ctx (exp:exp option) (f:fundec) : D.t = - ctx.local + let state = ctx.local in + match exp with + | Some e -> + if check_exp e ctx then + M.warn "WARN: return expression contains maybe freed blob"; + state + | None -> state let enter ctx (lval:lval option) (f:fundec) (args:exp list) : (D.t * D.t) list = - [ctx.local, ctx.local] + let caller_state = ctx.local in + let filtered_args = List.filter (fun x -> check_exp x ctx) args in + let args_to_add_to_callee_state = List.map (fun x -> + match ctx.ask (Queries.EvalValue x) with + | a when not (Queries.VD.is_top a) -> + begin match a with + | `Blob (v, s, t) -> (v, s, t) + | _ -> ValueDomain.Blobs.top () (* TODO: Is this correct? *) + end + | _ -> ValueDomain.Blobs.top () (* TODO: Is this correct? *) + ) filtered_args in + let callee_state = D.of_list args_to_add_to_callee_state in + match lval with + | Some lval -> + if check_lval lval ctx then + M.warn "WARN: lval in enter contains maybe freed blob"; + [caller_state, callee_state] + | None -> [caller_state, callee_state] + (* TODO: Unsure about this transfer function. Should we leave it as an identity function? *) let combine_env ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (callee_local:D.t) (f_ask:Queries.ask) : D.t = callee_local let combine_assign ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (callee_local:D.t) (f_ask: Queries.ask): D.t = - ctx.local + let state = ctx.local in + let () = List.iter (fun x -> + if check_exp x ctx then + M.warn "argument in combine_assign contains maybe freed blob" + ) args in + match lval with + | Some lval -> + if check_lval lval ctx then + M.warn "lval in combine_assign contains maybe freed blob"; + state + | None -> state let special ctx (lval:lval option) (f:varinfo) (arglist:exp list) : D.t = - ctx.local + let state = ctx.local in + let desc = LibraryFunctions.find f in + match desc.special arglist with + | Free ptr -> + if not (check_exp ptr ctx) then + begin match ctx.ask (Queries.EvalValue ptr) with + | a when not (Queries.VD.is_top a) -> + begin match a with + | `Blob (v, s, t) -> D.add (v, s, t) state + | _ -> state + end + | _ -> state + end + else + (* TODO: Is this way of printing in the else block okayish? *) + let () = M.warn "WARN: trying to free an already freed ptr" in + state + (* + * Check if we're allocating a maybe freed ptr -> in this case remove + * it from the maybe freed set + * TODO: Does this make sense? + *) + | Malloc _ + | Calloc _ + | Realloc _ -> + begin match lval with + | Some lval -> + begin match lval with + | (Mem e, _) -> + begin match ctx.ask (Queries.EvalValue e) with + | a when not (Queries.VD.is_top a) -> + begin match a with + | `Blob (v, s, t) -> + (* + * If we're trying to allocate a blob that is maybe freed, + * then we can remove it from the maybe freed set + * TODO: Makes sense? + *) + if D.mem (v, s, t) state then + D.remove (v, s, t) state + else state + | _ -> state + end + | _ -> state + end + | _ -> state + end + | None -> state + end + (* + * If we're not dealing with free or *alloc, + * then check if the lval we're assigning to is a ptr to a maybe freed blob. + * If yes, then WARN + *) + | _ -> + match lval with + | Some lval -> + if check_lval lval ctx then + M.warn "WARN: lval in special contains maybe freed blob"; + state + | None -> state let threadenter ctx lval f args = [ctx.local] let threadspawn ctx lval f args fctx = ctx.local From def0234842f5cce579cdb7c82d2a7ee52690a69f Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Wed, 17 May 2023 14:15:32 +0200 Subject: [PATCH 06/53] Add simple UAF regression test case --- tests/regression/71-use_after_free/01-simple-uaf.c | 12 ++++++++++++ 1 file changed, 12 insertions(+) create mode 100644 tests/regression/71-use_after_free/01-simple-uaf.c diff --git a/tests/regression/71-use_after_free/01-simple-uaf.c b/tests/regression/71-use_after_free/01-simple-uaf.c new file mode 100644 index 0000000000..1d89a602ce --- /dev/null +++ b/tests/regression/71-use_after_free/01-simple-uaf.c @@ -0,0 +1,12 @@ +#include +#include + +int main() { + int *ptr = malloc(sizeof(int)); + *ptr = 42; + + free(ptr); + + *ptr = 43; // UAF + free(ptr); // Double free +} \ No newline at end of file From cfdf32298b643602e092ef76f1e11c527a25962b Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Mon, 22 May 2023 06:59:52 +0200 Subject: [PATCH 07/53] Keep only free accessKind for free function Remove free function from old style definitions --- src/analyses/libraryFunctions.ml | 13 +------------ 1 file changed, 1 insertion(+), 12 deletions(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index c46ee81746..43475a4394 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -19,8 +19,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("strcpy", special [__ "dest" [w]; __ "src" [r]] @@ fun dest src -> Strcpy { dest; src }); ("malloc", special [__ "size" []] @@ fun size -> Malloc size); ("realloc", special [__ "ptr" [r; f]; __ "size" []] @@ fun ptr size -> Realloc { ptr; size }); - (* TODO: Do we need accessKind of "r" for "free" or is "f" alone already sufficient? *) - ("free", special [__ "ptr" [r; f]] @@ fun ptr -> Free ptr); + ("free", special [__ "ptr" [f]] @@ fun ptr -> Free ptr); ("abort", special [] Abort); ("exit", special [drop "exit_code" []] Abort); ("ungetc", unknown [drop "c" []; drop "stream" [r; w]]); @@ -490,16 +489,6 @@ let classify fn exps: categories = | n::size::_ -> `Calloc (n, size) | _ -> strange_arguments () end - (* - * TODO: Docs (https://goblint.readthedocs.io/en/latest/developer-guide/extending-library/#library-function-specifications) - * say we shouldn't add new specifications in classify - * Should I remove the guard for "free"-related functions here in this case? - *) - | "kfree" | "usb_free_urb" -> - begin match exps with - | ptr::_ -> `Free ptr - | _ -> strange_arguments () - end | "_spin_trylock" | "spin_trylock" | "mutex_trylock" | "_spin_trylock_irqsave" | "down_trylock" -> `Lock(true, true, true) From b1059012b361d57bcb99513010e5a278e00267c5 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Fri, 26 May 2023 15:28:56 +0200 Subject: [PATCH 08/53] Make the first UAF version now work --- src/analyses/useAfterFree.ml | 234 +++++++++++++++++------------------ 1 file changed, 111 insertions(+), 123 deletions(-) diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index 21730e6193..f60e166cf7 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -2,66 +2,121 @@ open GoblintCil open Analyses +open MessageCategory + +(* TODO: Maybe come up with a better name for top at some point? *) +module ToppedVarInfoSet = SetDomain.ToppedSet(CilType.Varinfo)(struct let topname = "Unknown" end) module Spec : Analyses.MCPSpec = struct include Analyses.DefaultSpec let name () = "useafterfree" - (* module D = Lattice.Unit *) - module D = SetDomain.Make(ValueDomain.Blobs) + + module D = ToppedVarInfoSet module C = Lattice.Unit - (** TODO: What about context-sensitivity? *) + (** TODO: Try out later in benchmarks to see how we perform with and without context-sensititivty *) let context _ _ = () (* HELPER FUNCTIONS *) - let check_exp (exp:exp) ctx = - let state = ctx.local in - match ctx.ask (Queries.EvalValue exp) with - | a when not (Queries.VD.is_top a) -> - begin match a with - | `Blob (v, s, t) -> if D.mem (v, s, t) state then true else false - | _ -> false - end - | _ -> false - - let check_lval (lval:lval) ctx = + (* Took inspiration from malloc_null *) + let may (f:'a -> 'b) (x:'a option) : unit = + match x with + | Some x -> f x + | None -> () + + (* Also took inspiration from malloc_null *) + let get_concrete_lval (ask:Queries.ask) (lval:lval) = + match ask.f (Queries.MayPointTo (mkAddrOf lval)) with + | a when Queries.LS.cardinal a = 1 && not (Queries.LS.mem (dummyFunDec.svar, `NoOffset) a) -> + let v, o = Queries.LS.choose a in + Some v + | _ -> None + + (* And also took inspiration from malloc_null *) + let get_concrete_exp (exp:exp) = + match constFold true exp with + | CastE (_, Lval (Var v, _)) + | Lval (Var v, _) -> Some v + | _ -> None + + let warn_lval_might_contain_freed ?(is_double_free = false) (transfer_fn_name:string) (lval:lval) ctx = let state = ctx.local in + let cwe_number = if is_double_free then 415 else 416 in match lval with + (* Case: lval is a variable *) + | (Var v, _) -> + if D.mem v state then + M.warn ~category:(Behavior (Undefined UseAfterFree)) ~tags:[CWE cwe_number] "lval in \"%s\" is a maybe freed pointer" transfer_fn_name + else () + (* Case: lval is an object whose address is in a pointer *) | (Mem e, _) -> - begin match ctx.ask (Queries.EvalValue e) with - | a when not (Queries.VD.is_top a) -> - begin match a with - | `Blob (v, s, t) -> if D.mem (v, s, t) state then true else false - | _ -> false - end - | _ -> false + begin match get_concrete_exp e with + | Some v -> + if D.mem v state then + M.warn ~category:(Behavior (Undefined UseAfterFree)) ~tags:[CWE cwe_number] "lval in \"%s\" points to a maybe freed pointer" transfer_fn_name + else () + | None -> () end - | _ -> false + (* TODO: Wasn't sure about the snippet below. Clean it up at some point *) + (* begin match ctx.ask (Queries.MayPointTo e) with + (* TODO: Do we need the second conjunct? *) + | a when not (Queries.LS.is_top a) && not (Queries.LS.mem (dummyFunDec.svar, `NoOffset) a) -> + (* TODO: Took inspiration from malloc_null. Double check if it makes sense. *) + let v, o = Queries.LS.choose a in + if D.mem v state then + M.warn ~category:(Behavior (Undefined UseAfterFree)) "lval in \"%s\" points to a maybe freed pointer" transfer_fn_name + else () + | _ -> () + end *) + + let rec warn_exp_might_contain_freed ?(is_double_free = false) (transfer_fn_name:string) (exp:exp) ctx = + match exp with + (* Base recursion cases *) + | Const _ + | SizeOf _ + | SizeOfStr _ + | AlignOf _ + | AddrOfLabel _ -> () + (* Non-base cases *) + | Real e + | Imag e + | SizeOfE e + | AlignOfE e + | UnOp (_, e, _) + | CastE (_, e) -> warn_exp_might_contain_freed ~is_double_free transfer_fn_name e ctx + | BinOp (_, e1, e2, _) -> + warn_exp_might_contain_freed ~is_double_free transfer_fn_name e1 ctx; + warn_exp_might_contain_freed ~is_double_free transfer_fn_name e2 ctx + | Question (e1, e2, e3, _) -> + warn_exp_might_contain_freed ~is_double_free transfer_fn_name e1 ctx; + warn_exp_might_contain_freed ~is_double_free transfer_fn_name e2 ctx; + warn_exp_might_contain_freed ~is_double_free transfer_fn_name e3 ctx + (* Lval cases (need [warn_lval_might_contain_freed] for them) *) + | Lval lval + | StartOf lval + | AddrOf lval -> warn_lval_might_contain_freed ~is_double_free transfer_fn_name lval ctx (* TRANSFER FUNCTIONS *) let assign ctx (lval:lval) (rval:exp) : D.t = let state = ctx.local in - (* Intuition: - * Check if lval and/or lval has an expression that points to a "maybe freed" blob - * If yes -> send out a WARNING; otherwise -> don't WARN - * In either case above -> don't change the CFG node's state - *) - match check_lval lval ctx, check_exp rval ctx with - | true, true -> M.warn "WARN: lval and rval contain maybe freed blob"; state - | false, true -> M.warn "WARN: rval contains maybe freed blob"; state - | true, false -> M.warn "WARN: lval contains maybe freed blob"; state - | false, false -> state + warn_lval_might_contain_freed "assign" lval ctx; + warn_exp_might_contain_freed "assign" rval ctx; + match get_concrete_exp rval, get_concrete_lval (Analyses.ask_of_ctx ctx) lval with + | Some v_exp, Some v_lval -> + if D.mem v_exp state then + D.add v_lval state + else state + | _ -> state let branch ctx (exp:exp) (tv:bool) : D.t = let state = ctx.local in - if check_exp exp ctx then - M.warn "WARN: branch exp contains maybe freed blob"; + warn_exp_might_contain_freed "branch" exp ctx; state let body ctx (f:fundec) : D.t = @@ -69,112 +124,45 @@ struct let return ctx (exp:exp option) (f:fundec) : D.t = let state = ctx.local in - match exp with - | Some e -> - if check_exp e ctx then - M.warn "WARN: return expression contains maybe freed blob"; - state - | None -> state + may (fun x -> warn_exp_might_contain_freed "return" x ctx) exp; + state + (* TODO: FINISH *) let enter ctx (lval:lval option) (f:fundec) (args:exp list) : (D.t * D.t) list = let caller_state = ctx.local in - let filtered_args = List.filter (fun x -> check_exp x ctx) args in - let args_to_add_to_callee_state = List.map (fun x -> - match ctx.ask (Queries.EvalValue x) with - | a when not (Queries.VD.is_top a) -> - begin match a with - | `Blob (v, s, t) -> (v, s, t) - | _ -> ValueDomain.Blobs.top () (* TODO: Is this correct? *) - end - | _ -> ValueDomain.Blobs.top () (* TODO: Is this correct? *) - ) filtered_args in - let callee_state = D.of_list args_to_add_to_callee_state in - match lval with - | Some lval -> - if check_lval lval ctx then - M.warn "WARN: lval in enter contains maybe freed blob"; - [caller_state, callee_state] - | None -> [caller_state, callee_state] + (* TODO: Decided to keep callee_state the same as caller_state for now. Discuss this. *) + let callee_state = caller_state in + may (fun x -> warn_lval_might_contain_freed "enter" x ctx) lval; + List.iter (fun arg -> warn_exp_might_contain_freed "enter" arg ctx) args; + [caller_state, callee_state] - (* TODO: Unsure about this transfer function. Should we leave it as an identity function? *) + (* TODO: FINISH *) let combine_env ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (callee_local:D.t) (f_ask:Queries.ask) : D.t = callee_local + (* TODO: FINISH *) let combine_assign ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (callee_local:D.t) (f_ask: Queries.ask): D.t = let state = ctx.local in - let () = List.iter (fun x -> - if check_exp x ctx then - M.warn "argument in combine_assign contains maybe freed blob" - ) args in - match lval with - | Some lval -> - if check_lval lval ctx then - M.warn "lval in combine_assign contains maybe freed blob"; - state - | None -> state + may (fun x -> warn_lval_might_contain_freed "combine_assign" x ctx) lval; + List.iter (fun arg -> warn_exp_might_contain_freed "combine_assign" arg ctx) args; + state let special ctx (lval:lval option) (f:varinfo) (arglist:exp list) : D.t = let state = ctx.local in + may (fun x -> warn_lval_might_contain_freed ~is_double_free:(f.vname = "free") ("special: " ^ f.vname) x ctx) lval; + List.iter (fun arg -> warn_exp_might_contain_freed ~is_double_free:(f.vname = "free") ("special: " ^ f.vname) arg ctx) arglist; let desc = LibraryFunctions.find f in match desc.special arglist with | Free ptr -> - if not (check_exp ptr ctx) then - begin match ctx.ask (Queries.EvalValue ptr) with - | a when not (Queries.VD.is_top a) -> - begin match a with - | `Blob (v, s, t) -> D.add (v, s, t) state - | _ -> state - end - | _ -> state - end - else - (* TODO: Is this way of printing in the else block okayish? *) - let () = M.warn "WARN: trying to free an already freed ptr" in - state - (* - * Check if we're allocating a maybe freed ptr -> in this case remove - * it from the maybe freed set - * TODO: Does this make sense? - *) - | Malloc _ - | Calloc _ - | Realloc _ -> - begin match lval with - | Some lval -> - begin match lval with - | (Mem e, _) -> - begin match ctx.ask (Queries.EvalValue e) with - | a when not (Queries.VD.is_top a) -> - begin match a with - | `Blob (v, s, t) -> - (* - * If we're trying to allocate a blob that is maybe freed, - * then we can remove it from the maybe freed set - * TODO: Makes sense? - *) - if D.mem (v, s, t) state then - D.remove (v, s, t) state - else state - | _ -> state - end - | _ -> state - end - | _ -> state - end + begin match get_concrete_exp ptr with + | Some v -> + if D.mem v state then + state + else + D.add v state | None -> state end - (* - * If we're not dealing with free or *alloc, - * then check if the lval we're assigning to is a ptr to a maybe freed blob. - * If yes, then WARN - *) - | _ -> - match lval with - | Some lval -> - if check_lval lval ctx then - M.warn "WARN: lval in special contains maybe freed blob"; - state - | None -> state + | _ -> state let threadenter ctx lval f args = [ctx.local] let threadspawn ctx lval f args fctx = ctx.local From d9027c194f2ab38cb096507e8b361927cd7d6e68 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Fri, 26 May 2023 15:29:45 +0200 Subject: [PATCH 09/53] Update regression test comments --- tests/regression/71-use_after_free/01-simple-uaf.c | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/regression/71-use_after_free/01-simple-uaf.c b/tests/regression/71-use_after_free/01-simple-uaf.c index 1d89a602ce..c08f74a524 100644 --- a/tests/regression/71-use_after_free/01-simple-uaf.c +++ b/tests/regression/71-use_after_free/01-simple-uaf.c @@ -7,6 +7,6 @@ int main() { free(ptr); - *ptr = 43; // UAF - free(ptr); // Double free + *ptr = 43; // Should report "Use After Free (CWE-416)" + free(ptr); // Should report "Double Free (CWE-415)" } \ No newline at end of file From 748d77d37ae50fc4aa1fd8cb4fb7c4829adad1db Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Fri, 26 May 2023 15:58:19 +0200 Subject: [PATCH 10/53] Add conditional UAF regression test case --- .../71-use_after_free/02-conditional-uaf.c | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100644 tests/regression/71-use_after_free/02-conditional-uaf.c diff --git a/tests/regression/71-use_after_free/02-conditional-uaf.c b/tests/regression/71-use_after_free/02-conditional-uaf.c new file mode 100644 index 0000000000..6f84347946 --- /dev/null +++ b/tests/regression/71-use_after_free/02-conditional-uaf.c @@ -0,0 +1,16 @@ +#include +#include + +int main() { + int *ptr = malloc(sizeof(int)); + *ptr = 42; + + int input1; + + if (input1) { + free(ptr); + } + + *ptr = 43; // Should report "Use After Free (CWE-416)" + free(ptr); // Should report "Double Free (CWE-415)" +} \ No newline at end of file From 87ac7f167e9d5b6f84f67355511883130063a0fc Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sat, 27 May 2023 16:32:01 +0200 Subject: [PATCH 11/53] Recurse down into offsets as well --- src/analyses/useAfterFree.ml | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index f60e166cf7..d2150d6afe 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -43,17 +43,25 @@ struct | Lval (Var v, _) -> Some v | _ -> None - let warn_lval_might_contain_freed ?(is_double_free = false) (transfer_fn_name:string) (lval:lval) ctx = + let rec warn_lval_might_contain_freed ?(is_double_free = false) (transfer_fn_name:string) (lval:lval) ctx = let state = ctx.local in let cwe_number = if is_double_free then 415 else 416 in + let rec offset_might_contain_freed offset = + match offset with + | NoOffset -> () + | Field (f, o) -> offset_might_contain_freed o + | Index (e, o) -> warn_exp_might_contain_freed transfer_fn_name e ctx; offset_might_contain_freed o + in match lval with (* Case: lval is a variable *) - | (Var v, _) -> + | (Var v, o) -> + offset_might_contain_freed o; if D.mem v state then M.warn ~category:(Behavior (Undefined UseAfterFree)) ~tags:[CWE cwe_number] "lval in \"%s\" is a maybe freed pointer" transfer_fn_name else () (* Case: lval is an object whose address is in a pointer *) - | (Mem e, _) -> + | (Mem e, o) -> + offset_might_contain_freed o; begin match get_concrete_exp e with | Some v -> if D.mem v state then @@ -73,7 +81,7 @@ struct | _ -> () end *) - let rec warn_exp_might_contain_freed ?(is_double_free = false) (transfer_fn_name:string) (exp:exp) ctx = + and warn_exp_might_contain_freed ?(is_double_free = false) (transfer_fn_name:string) (exp:exp) ctx = match exp with (* Base recursion cases *) | Const _ From 6befcf887a6397674a4e19215116eb9acfab6ae1 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sat, 27 May 2023 16:33:03 +0200 Subject: [PATCH 12/53] Add another regression test case to check offset UAF --- .../71-use_after_free/03-nested-ptr-uaf.c | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100644 tests/regression/71-use_after_free/03-nested-ptr-uaf.c diff --git a/tests/regression/71-use_after_free/03-nested-ptr-uaf.c b/tests/regression/71-use_after_free/03-nested-ptr-uaf.c new file mode 100644 index 0000000000..51c99355e4 --- /dev/null +++ b/tests/regression/71-use_after_free/03-nested-ptr-uaf.c @@ -0,0 +1,16 @@ +#include +#include + +int main() { + int *ptr = malloc(sizeof(int)); + *ptr = 1; + + free(ptr); + + int a[2] = {0, 1}; + a[*ptr] = 5; // Should report "Use After Free (CWE-416)" + + if (a[*ptr] != 5) { // Should report "Use After Free (CWE-416)" + free(ptr); // Should report "Double Free (CWE-415)" + } +} \ No newline at end of file From 71a9cac1ab44d9deb48ffa4abd1754c592fd63eb Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sun, 28 May 2023 11:48:24 +0200 Subject: [PATCH 13/53] Finish some transfer functions TODOs from earlier --- src/analyses/useAfterFree.ml | 60 +++++++++++++++++++++++++++--------- 1 file changed, 46 insertions(+), 14 deletions(-) diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index d2150d6afe..36dc036a34 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -130,44 +130,76 @@ struct let body ctx (f:fundec) : D.t = ctx.local + (* Took inspiration from malloc_null. Does it make sense? *) + let freed_var_at_return_ = ref dummyFunDec.svar + let freed_var_at_return () = !freed_var_at_return_ + let return ctx (exp:exp option) (f:fundec) : D.t = let state = ctx.local in may (fun x -> warn_exp_might_contain_freed "return" x ctx) exp; - state + (* Intuition: + * Check if the return expression has a maybe freed var + * If yes, then add the dummyFunDec's varinfo to the state + * Else, don't change the state + *) + match exp with + | Some ret -> + begin match get_concrete_exp ret with + | Some v -> + if D.mem v state then + D.add (freed_var_at_return ()) state + else state + | None -> state + end + | None -> state - (* TODO: FINISH *) let enter ctx (lval:lval option) (f:fundec) (args:exp list) : (D.t * D.t) list = let caller_state = ctx.local in - (* TODO: Decided to keep callee_state the same as caller_state for now. Discuss this. *) - let callee_state = caller_state in may (fun x -> warn_lval_might_contain_freed "enter" x ctx) lval; List.iter (fun arg -> warn_exp_might_contain_freed "enter" arg ctx) args; + (* Intuition for computing callee_state: + * 1. Take all global variables which are maybe freed + * 2. Take all actual parameters of the callee and take only the ones (if any) which are maybe freed in the caller_state + * 3. callee_state is the union of the sets from 1. and 2. above + *) + let glob_freed_vars = D.filter (fun x -> x.vglob) caller_state in + let args_to_vars = List.filter_map (fun x -> get_concrete_exp x) args in + let caller_freed_vars_in_args = D.of_list (List.filter (fun x -> D.mem x caller_state) args_to_vars) in + let callee_state = D.union glob_freed_vars caller_freed_vars_in_args in [caller_state, callee_state] - (* TODO: FINISH *) let combine_env ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (callee_local:D.t) (f_ask:Queries.ask) : D.t = - callee_local + (* Intuition for computing the caller_state: + * 1. Remove all local vars of the callee, which are maybe freed, from the callee_local state + * 2. Set the caller_state as the callee_local state without the callee local maybe freed vars (the result of 1.) + *) + let freed_callee_local_vars = D.filter (fun x -> List.mem x f.slocals) callee_local in + let caller_state = D.diff callee_local freed_callee_local_vars in + caller_state - (* TODO: FINISH *) let combine_assign ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (callee_local:D.t) (f_ask: Queries.ask): D.t = - let state = ctx.local in + let caller_state = ctx.local in may (fun x -> warn_lval_might_contain_freed "combine_assign" x ctx) lval; List.iter (fun arg -> warn_exp_might_contain_freed "combine_assign" arg ctx) args; - state + match lval, D.mem (freed_var_at_return ()) callee_local with + | Some lv, true -> + begin match get_concrete_lval (Analyses.ask_of_ctx ctx) lv with + | Some v -> D.add v caller_state + | None -> caller_state + end + | _ -> caller_state let special ctx (lval:lval option) (f:varinfo) (arglist:exp list) : D.t = let state = ctx.local in - may (fun x -> warn_lval_might_contain_freed ~is_double_free:(f.vname = "free") ("special: " ^ f.vname) x ctx) lval; + may (fun x -> warn_lval_might_contain_freed ("special: " ^ f.vname) x ctx) lval; List.iter (fun arg -> warn_exp_might_contain_freed ~is_double_free:(f.vname = "free") ("special: " ^ f.vname) arg ctx) arglist; let desc = LibraryFunctions.find f in match desc.special arglist with | Free ptr -> begin match get_concrete_exp ptr with | Some v -> - if D.mem v state then - state - else - D.add v state + if D.mem v state then state + else D.add v state | None -> state end | _ -> state From e8ed31cc8a6446d209c9ec6d832f15c034ac62f7 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sun, 28 May 2023 14:19:31 +0200 Subject: [PATCH 14/53] Print lval names when WARNING for a UAF --- src/analyses/useAfterFree.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index 36dc036a34..eed9e9ac8f 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -57,7 +57,7 @@ struct | (Var v, o) -> offset_might_contain_freed o; if D.mem v state then - M.warn ~category:(Behavior (Undefined UseAfterFree)) ~tags:[CWE cwe_number] "lval in \"%s\" is a maybe freed pointer" transfer_fn_name + M.warn ~category:(Behavior (Undefined UseAfterFree)) ~tags:[CWE cwe_number] "lval (%s) in \"%s\" is a maybe freed pointer" v.vname transfer_fn_name else () (* Case: lval is an object whose address is in a pointer *) | (Mem e, o) -> @@ -65,7 +65,7 @@ struct begin match get_concrete_exp e with | Some v -> if D.mem v state then - M.warn ~category:(Behavior (Undefined UseAfterFree)) ~tags:[CWE cwe_number] "lval in \"%s\" points to a maybe freed pointer" transfer_fn_name + M.warn ~category:(Behavior (Undefined UseAfterFree)) ~tags:[CWE cwe_number] "lval (%s) in \"%s\" points to a maybe freed pointer" v.vname transfer_fn_name else () | None -> () end From 969d57cca6883f8fe1a41be210a377124cfeaf65 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sun, 28 May 2023 15:15:22 +0200 Subject: [PATCH 15/53] Add DoubleFree message category --- src/util/messageCategory.ml | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/util/messageCategory.ml b/src/util/messageCategory.ml index ef8ee5d6a9..6a30842cd6 100644 --- a/src/util/messageCategory.ml +++ b/src/util/messageCategory.ml @@ -11,6 +11,7 @@ type undefined_behavior = | ArrayOutOfBounds of array_oob | NullPointerDereference | UseAfterFree + | DoubleFree | Uninitialized | Other [@@deriving eq, ord, hash] @@ -62,6 +63,7 @@ struct let array_out_of_bounds e: category = create @@ ArrayOutOfBounds e let nullpointer_dereference: category = create @@ NullPointerDereference let use_after_free: category = create @@ UseAfterFree + let double_free: category = create @@ DoubleFree let uninitialized: category = create @@ Uninitialized let other: category = create @@ Other @@ -97,6 +99,7 @@ struct | "array_out_of_bounds" -> ArrayOutOfBounds.from_string_list t | "nullpointer_dereference" -> nullpointer_dereference | "use_after_free" -> use_after_free + | "double_free" -> double_free | "uninitialized" -> uninitialized | "other" -> other | _ -> Unknown @@ -106,6 +109,7 @@ struct | ArrayOutOfBounds e -> "ArrayOutOfBounds" :: ArrayOutOfBounds.path_show e | NullPointerDereference -> ["NullPointerDereference"] | UseAfterFree -> ["UseAfterFree"] + | DoubleFree -> ["DoubleFree"] | Uninitialized -> ["Uninitialized"] | Other -> ["Other"] end @@ -214,6 +218,7 @@ let behaviorName = function |Undefined u -> match u with |NullPointerDereference -> "NullPointerDereference" |UseAfterFree -> "UseAfterFree" + |DoubleFree -> "DoubleFree" |Uninitialized -> "Uninitialized" |Other -> "Other" | ArrayOutOfBounds aob -> match aob with From 89d657f37d0836f1ac819624ab9190b4f1f2ae7d Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sun, 28 May 2023 15:17:23 +0200 Subject: [PATCH 16/53] Fix indentation and remove comma in behaviorName (messageCategory module) --- src/util/messageCategory.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/util/messageCategory.ml b/src/util/messageCategory.ml index 6a30842cd6..a54530fc76 100644 --- a/src/util/messageCategory.ml +++ b/src/util/messageCategory.ml @@ -213,14 +213,14 @@ let path_show e = let show x = String.concat " > " (path_show x) let behaviorName = function - |Machine -> "Machine"; - |Implementation -> "Implementation" - |Undefined u -> match u with - |NullPointerDereference -> "NullPointerDereference" - |UseAfterFree -> "UseAfterFree" - |DoubleFree -> "DoubleFree" - |Uninitialized -> "Uninitialized" - |Other -> "Other" + | Machine -> "Machine" + | Implementation -> "Implementation" + | Undefined u -> match u with + | NullPointerDereference -> "NullPointerDereference" + | UseAfterFree -> "UseAfterFree" + | DoubleFree -> "DoubleFree" + | Uninitialized -> "Uninitialized" + | Other -> "Other" | ArrayOutOfBounds aob -> match aob with | PastEnd -> "PastEnd" | BeforeStart -> "BeforeStart" From a3c1617422e56eb7888531d5c916ce76ba063b85 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sun, 28 May 2023 15:21:04 +0200 Subject: [PATCH 17/53] Use the DoubleFree category in the UAF analysis --- src/analyses/useAfterFree.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index eed9e9ac8f..75a3b44794 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -45,6 +45,7 @@ struct let rec warn_lval_might_contain_freed ?(is_double_free = false) (transfer_fn_name:string) (lval:lval) ctx = let state = ctx.local in + let undefined_behavior = if is_double_free then Undefined DoubleFree else Undefined UseAfterFree in let cwe_number = if is_double_free then 415 else 416 in let rec offset_might_contain_freed offset = match offset with @@ -57,7 +58,7 @@ struct | (Var v, o) -> offset_might_contain_freed o; if D.mem v state then - M.warn ~category:(Behavior (Undefined UseAfterFree)) ~tags:[CWE cwe_number] "lval (%s) in \"%s\" is a maybe freed pointer" v.vname transfer_fn_name + M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "lval (%s) in \"%s\" is a maybe freed pointer" v.vname transfer_fn_name else () (* Case: lval is an object whose address is in a pointer *) | (Mem e, o) -> @@ -65,7 +66,7 @@ struct begin match get_concrete_exp e with | Some v -> if D.mem v state then - M.warn ~category:(Behavior (Undefined UseAfterFree)) ~tags:[CWE cwe_number] "lval (%s) in \"%s\" points to a maybe freed pointer" v.vname transfer_fn_name + M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "lval (%s) in \"%s\" points to a maybe freed pointer" v.vname transfer_fn_name else () | None -> () end From cd7615c3b8cced1ad4dae112a2e70741c5a56466 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sun, 28 May 2023 15:24:18 +0200 Subject: [PATCH 18/53] Add SARIF rule for double free (CWE 415) --- src/util/sarifRules.ml | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/util/sarifRules.ml b/src/util/sarifRules.ml index 17f4f5f263..c446e1cb6a 100644 --- a/src/util/sarifRules.ml +++ b/src/util/sarifRules.ml @@ -185,6 +185,14 @@ let rules = [ shortDescription="The software reads or writes to a buffer using an index or pointer that references a memory location after the end of the buffer. "; helpUri="https://cwe.mitre.org/data/definitions/788.html"; longDescription=""; + }; + { + name="415"; + ruleId="GO0022"; + helpText="Double Free"; + shortDescription="The product calls free() twice on the same memory address, potentially leading to modification of unexpected memory locations."; + helpUri="https://cwe.mitre.org/data/definitions/415.html"; + longDescription="" } ] From 0909a44d7b1c012e22843cfb8a78dd28019caf04 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sun, 28 May 2023 17:49:42 +0200 Subject: [PATCH 19/53] Account for global vars in enter and combine --- src/analyses/useAfterFree.ml | 34 ++++++++++++++++++---------------- 1 file changed, 18 insertions(+), 16 deletions(-) diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index 75a3b44794..245c8af125 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -81,7 +81,6 @@ struct else () | _ -> () end *) - and warn_exp_might_contain_freed ?(is_double_free = false) (transfer_fn_name:string) (exp:exp) ctx = match exp with (* Base recursion cases *) @@ -158,28 +157,31 @@ struct let caller_state = ctx.local in may (fun x -> warn_lval_might_contain_freed "enter" x ctx) lval; List.iter (fun arg -> warn_exp_might_contain_freed "enter" arg ctx) args; - (* Intuition for computing callee_state: - * 1. Take all global variables which are maybe freed - * 2. Take all actual parameters of the callee and take only the ones (if any) which are maybe freed in the caller_state - * 3. callee_state is the union of the sets from 1. and 2. above - *) - let glob_freed_vars = D.filter (fun x -> x.vglob) caller_state in - let args_to_vars = List.filter_map (fun x -> get_concrete_exp x) args in - let caller_freed_vars_in_args = D.of_list (List.filter (fun x -> D.mem x caller_state) args_to_vars) in - let callee_state = D.union glob_freed_vars caller_freed_vars_in_args in + let glob_maybe_freed_vars = D.filter (fun x -> x.vglob) caller_state in + let zipped = List.combine f.sformals args in + let callee_state = List.fold_left (fun acc (f, a) -> + match get_concrete_exp a with + | Some v -> + if D.mem v caller_state then D.add f acc else acc + | None -> acc + ) glob_maybe_freed_vars zipped in [caller_state, callee_state] let combine_env ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (callee_local:D.t) (f_ask:Queries.ask) : D.t = - (* Intuition for computing the caller_state: - * 1. Remove all local vars of the callee, which are maybe freed, from the callee_local state - * 2. Set the caller_state as the callee_local state without the callee local maybe freed vars (the result of 1.) - *) - let freed_callee_local_vars = D.filter (fun x -> List.mem x f.slocals) callee_local in - let caller_state = D.diff callee_local freed_callee_local_vars in + let glob_maybe_freed_vars = D.filter (fun x -> x.vglob) callee_local in + let zipped = List.combine f.sformals args in + let caller_state = List.fold_left (fun acc (f, a) -> + match get_concrete_exp a with + | Some v -> + if D.mem f callee_local then D.add v acc else acc + | None -> acc + ) glob_maybe_freed_vars zipped in caller_state let combine_assign ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (callee_local:D.t) (f_ask: Queries.ask): D.t = let caller_state = ctx.local in + + (* TODO: Should we actually warn here? It seems to clutter the output a bit. *) may (fun x -> warn_lval_might_contain_freed "combine_assign" x ctx) lval; List.iter (fun arg -> warn_exp_might_contain_freed "combine_assign" arg ctx) args; match lval, D.mem (freed_var_at_return ()) callee_local with From 907739d3ecc76f637b361984f4185f6bcf963a8a Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sun, 28 May 2023 17:50:25 +0200 Subject: [PATCH 20/53] Add regression test with a function call --- .../71-use_after_free/04-function-call-uaf.c | 31 +++++++++++++++++++ 1 file changed, 31 insertions(+) create mode 100644 tests/regression/71-use_after_free/04-function-call-uaf.c diff --git a/tests/regression/71-use_after_free/04-function-call-uaf.c b/tests/regression/71-use_after_free/04-function-call-uaf.c new file mode 100644 index 0000000000..0d14a8cb3c --- /dev/null +++ b/tests/regression/71-use_after_free/04-function-call-uaf.c @@ -0,0 +1,31 @@ +#include +#include + +int *ptr1; + +int main() { + ptr1 = malloc(sizeof(int)); + *ptr1 = 100; + + int *ptr2 = malloc(sizeof(int)); + *ptr2 = 1; + + int *ptr3 = malloc(sizeof(int)); + *ptr3 = 10; + + free(ptr1); + free(ptr2); + + f(ptr1, ptr2, ptr3); // Should report "Use After Free (CWE-416)" for "ptr1" and "ptr2" here + + free(ptr3); // Should report "Double Free (CWE-415)" + + return 0; +} + +void f(int *p1, int *p2, int *p3) { + *p1 = 5000; // Should report "Use After Free (CWE-416)" + free(p1); // Should report "Double Free (CWE-415)" + free(p2); // Should report "Double Free (CWE-415)" + free(p3); +} \ No newline at end of file From cc3356108eb695adeba3f7b5324c2ce54b74e83f Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Thu, 1 Jun 2023 23:14:20 +0200 Subject: [PATCH 21/53] Don't treat free in special_of_old --- src/analyses/libraryDesc.ml | 1 - 1 file changed, 1 deletion(-) diff --git a/src/analyses/libraryDesc.ml b/src/analyses/libraryDesc.ml index 4f83a06763..4eb8e5da76 100644 --- a/src/analyses/libraryDesc.ml +++ b/src/analyses/libraryDesc.ml @@ -123,7 +123,6 @@ let special_of_old classify_name = fun args -> | `Malloc e -> Malloc e | `Calloc (count, size) -> Calloc { count; size; } | `Realloc (ptr, size) -> Realloc { ptr; size; } - | `Free ptr -> Free ptr | `Lock (try_, write, return_on_success) -> begin match args with | [lock] -> Lock { lock ; try_; write; return_on_success; } From cf169d30f950cf23d2fc239767b6623f621e7ce4 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Thu, 1 Jun 2023 23:16:57 +0200 Subject: [PATCH 22/53] Cleanup + replace may with Option.iter --- src/analyses/useAfterFree.ml | 16 ++++------------ 1 file changed, 4 insertions(+), 12 deletions(-) diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index 245c8af125..763735da9c 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -22,13 +22,6 @@ struct (* HELPER FUNCTIONS *) - (* Took inspiration from malloc_null *) - let may (f:'a -> 'b) (x:'a option) : unit = - match x with - | Some x -> f x - | None -> () - - (* Also took inspiration from malloc_null *) let get_concrete_lval (ask:Queries.ask) (lval:lval) = match ask.f (Queries.MayPointTo (mkAddrOf lval)) with | a when Queries.LS.cardinal a = 1 && not (Queries.LS.mem (dummyFunDec.svar, `NoOffset) a) -> @@ -36,7 +29,6 @@ struct Some v | _ -> None - (* And also took inspiration from malloc_null *) let get_concrete_exp (exp:exp) = match constFold true exp with | CastE (_, Lval (Var v, _)) @@ -136,7 +128,7 @@ struct let return ctx (exp:exp option) (f:fundec) : D.t = let state = ctx.local in - may (fun x -> warn_exp_might_contain_freed "return" x ctx) exp; + Option.iter (fun x -> warn_exp_might_contain_freed "return" x ctx) exp; (* Intuition: * Check if the return expression has a maybe freed var * If yes, then add the dummyFunDec's varinfo to the state @@ -155,7 +147,7 @@ struct let enter ctx (lval:lval option) (f:fundec) (args:exp list) : (D.t * D.t) list = let caller_state = ctx.local in - may (fun x -> warn_lval_might_contain_freed "enter" x ctx) lval; + Option.iter (fun x -> warn_lval_might_contain_freed "enter" x ctx) lval; List.iter (fun arg -> warn_exp_might_contain_freed "enter" arg ctx) args; let glob_maybe_freed_vars = D.filter (fun x -> x.vglob) caller_state in let zipped = List.combine f.sformals args in @@ -182,7 +174,7 @@ struct let caller_state = ctx.local in (* TODO: Should we actually warn here? It seems to clutter the output a bit. *) - may (fun x -> warn_lval_might_contain_freed "combine_assign" x ctx) lval; + Option.iter (fun x -> warn_lval_might_contain_freed "combine_assign" x ctx) lval; List.iter (fun arg -> warn_exp_might_contain_freed "combine_assign" arg ctx) args; match lval, D.mem (freed_var_at_return ()) callee_local with | Some lv, true -> @@ -194,7 +186,7 @@ struct let special ctx (lval:lval option) (f:varinfo) (arglist:exp list) : D.t = let state = ctx.local in - may (fun x -> warn_lval_might_contain_freed ("special: " ^ f.vname) x ctx) lval; + Option.iter (fun x -> warn_lval_might_contain_freed ("special: " ^ f.vname) x ctx) lval; List.iter (fun arg -> warn_exp_might_contain_freed ~is_double_free:(f.vname = "free") ("special: " ^ f.vname) arg ctx) arglist; let desc = LibraryFunctions.find f in match desc.special arglist with From 61d674cb5b74a6edbcbf077347389ba59d3ece3a Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Thu, 1 Jun 2023 23:20:33 +0200 Subject: [PATCH 23/53] Remove `Free from the categories type --- src/analyses/libraryFunctions.ml | 1 - 1 file changed, 1 deletion(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 43475a4394..c05bc62e90 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -455,7 +455,6 @@ type categories = [ | `Malloc of exp | `Calloc of exp * exp | `Realloc of exp * exp - | `Free of exp | `Lock of bool * bool * bool (* try? * write? * return on success *) | `Unlock | `ThreadCreate of exp * exp * exp (* id * f * x *) From 006e13213cb71ba0c6a6574284c52a74665be694 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sun, 4 Jun 2023 22:45:41 +0200 Subject: [PATCH 24/53] Remove unnecessary code and reiterate on transfer functions --- src/analyses/useAfterFree.ml | 139 +++++++++-------------------------- 1 file changed, 36 insertions(+), 103 deletions(-) diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index 763735da9c..4449242a97 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -22,19 +22,6 @@ struct (* HELPER FUNCTIONS *) - let get_concrete_lval (ask:Queries.ask) (lval:lval) = - match ask.f (Queries.MayPointTo (mkAddrOf lval)) with - | a when Queries.LS.cardinal a = 1 && not (Queries.LS.mem (dummyFunDec.svar, `NoOffset) a) -> - let v, o = Queries.LS.choose a in - Some v - | _ -> None - - let get_concrete_exp (exp:exp) = - match constFold true exp with - | CastE (_, Lval (Var v, _)) - | Lval (Var v, _) -> Some v - | _ -> None - let rec warn_lval_might_contain_freed ?(is_double_free = false) (transfer_fn_name:string) (lval:lval) ctx = let state = ctx.local in let undefined_behavior = if is_double_free then Undefined DoubleFree else Undefined UseAfterFree in @@ -45,34 +32,15 @@ struct | Field (f, o) -> offset_might_contain_freed o | Index (e, o) -> warn_exp_might_contain_freed transfer_fn_name e ctx; offset_might_contain_freed o in - match lval with - (* Case: lval is a variable *) - | (Var v, o) -> - offset_might_contain_freed o; - if D.mem v state then - M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "lval (%s) in \"%s\" is a maybe freed pointer" v.vname transfer_fn_name - else () - (* Case: lval is an object whose address is in a pointer *) - | (Mem e, o) -> - offset_might_contain_freed o; - begin match get_concrete_exp e with - | Some v -> - if D.mem v state then - M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "lval (%s) in \"%s\" points to a maybe freed pointer" v.vname transfer_fn_name - else () - | None -> () - end - (* TODO: Wasn't sure about the snippet below. Clean it up at some point *) - (* begin match ctx.ask (Queries.MayPointTo e) with - (* TODO: Do we need the second conjunct? *) - | a when not (Queries.LS.is_top a) && not (Queries.LS.mem (dummyFunDec.svar, `NoOffset) a) -> - (* TODO: Took inspiration from malloc_null. Double check if it makes sense. *) + let (_, o) = lval in offset_might_contain_freed o; (* Check the lval's offset *) + match ctx.ask (Queries.MayPointTo (mkAddrOf lval)) with + | a when not (Queries.LS.is_top a) && not (Queries.LS.mem (dummyFunDec.svar, `NoOffset) a) -> + ignore (Pretty.printf "WARN_LVAL %a\n" Queries.LS.pretty a); let v, o = Queries.LS.choose a in - if D.mem v state then - M.warn ~category:(Behavior (Undefined UseAfterFree)) "lval in \"%s\" points to a maybe freed pointer" transfer_fn_name - else () - | _ -> () - end *) + if ctx.ask (Queries.IsHeapVar v) && D.mem v state then + M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "lval (%s) in \"%s\" points to a maybe freed memory region" v.vname transfer_fn_name + | _ -> () + and warn_exp_might_contain_freed ?(is_double_free = false) (transfer_fn_name:string) (exp:exp) ctx = match exp with (* Base recursion cases *) @@ -104,85 +72,50 @@ struct (* TRANSFER FUNCTIONS *) let assign ctx (lval:lval) (rval:exp) : D.t = - let state = ctx.local in warn_lval_might_contain_freed "assign" lval ctx; warn_exp_might_contain_freed "assign" rval ctx; - match get_concrete_exp rval, get_concrete_lval (Analyses.ask_of_ctx ctx) lval with - | Some v_exp, Some v_lval -> - if D.mem v_exp state then - D.add v_lval state - else state - | _ -> state + ctx.local let branch ctx (exp:exp) (tv:bool) : D.t = - let state = ctx.local in warn_exp_might_contain_freed "branch" exp ctx; - state + ctx.local let body ctx (f:fundec) : D.t = ctx.local - (* Took inspiration from malloc_null. Does it make sense? *) - let freed_var_at_return_ = ref dummyFunDec.svar - let freed_var_at_return () = !freed_var_at_return_ - let return ctx (exp:exp option) (f:fundec) : D.t = - let state = ctx.local in Option.iter (fun x -> warn_exp_might_contain_freed "return" x ctx) exp; - (* Intuition: - * Check if the return expression has a maybe freed var - * If yes, then add the dummyFunDec's varinfo to the state - * Else, don't change the state - *) - match exp with - | Some ret -> - begin match get_concrete_exp ret with - | Some v -> - if D.mem v state then - D.add (freed_var_at_return ()) state - else state - | None -> state - end - | None -> state + ctx.local let enter ctx (lval:lval option) (f:fundec) (args:exp list) : (D.t * D.t) list = let caller_state = ctx.local in Option.iter (fun x -> warn_lval_might_contain_freed "enter" x ctx) lval; List.iter (fun arg -> warn_exp_might_contain_freed "enter" arg ctx) args; - let glob_maybe_freed_vars = D.filter (fun x -> x.vglob) caller_state in - let zipped = List.combine f.sformals args in - let callee_state = List.fold_left (fun acc (f, a) -> - match get_concrete_exp a with - | Some v -> - if D.mem v caller_state then D.add f acc else acc - | None -> acc - ) glob_maybe_freed_vars zipped in - [caller_state, callee_state] + if D.is_empty caller_state then + [caller_state, caller_state] + else ( + let reachable_from_args = List.fold_left (fun acc arg -> Queries.LS.join acc (ctx.ask (ReachableFrom arg))) (Queries.LS.empty ()) args in + if Queries.LS.is_top reachable_from_args || D.is_top caller_state then + [caller_state, caller_state] + else + let reachable_vars = + Queries.LS.elements reachable_from_args + |> List.map fst + |> List.filter (fun var -> ctx.ask (Queries.IsHeapVar var)) + |> D.of_list + in + let callee_state = D.inter caller_state reachable_vars in + [caller_state, callee_state] + ) let combine_env ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (callee_local:D.t) (f_ask:Queries.ask) : D.t = - let glob_maybe_freed_vars = D.filter (fun x -> x.vglob) callee_local in - let zipped = List.combine f.sformals args in - let caller_state = List.fold_left (fun acc (f, a) -> - match get_concrete_exp a with - | Some v -> - if D.mem f callee_local then D.add v acc else acc - | None -> acc - ) glob_maybe_freed_vars zipped in - caller_state - - let combine_assign ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (callee_local:D.t) (f_ask: Queries.ask): D.t = let caller_state = ctx.local in + D.join caller_state callee_local - (* TODO: Should we actually warn here? It seems to clutter the output a bit. *) + let combine_assign ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (callee_local:D.t) (f_ask: Queries.ask): D.t = Option.iter (fun x -> warn_lval_might_contain_freed "combine_assign" x ctx) lval; List.iter (fun arg -> warn_exp_might_contain_freed "combine_assign" arg ctx) args; - match lval, D.mem (freed_var_at_return ()) callee_local with - | Some lv, true -> - begin match get_concrete_lval (Analyses.ask_of_ctx ctx) lv with - | Some v -> D.add v caller_state - | None -> caller_state - end - | _ -> caller_state + ctx.local let special ctx (lval:lval option) (f:varinfo) (arglist:exp list) : D.t = let state = ctx.local in @@ -191,11 +124,11 @@ struct let desc = LibraryFunctions.find f in match desc.special arglist with | Free ptr -> - begin match get_concrete_exp ptr with - | Some v -> - if D.mem v state then state - else D.add v state - | None -> state + begin match ctx.ask HeapVar with + | `Lifted var -> + ignore (Pretty.printf "FREE: %a\n" CilType.Varinfo.pretty var); + D.add var state + | _ -> state end | _ -> state @@ -208,4 +141,4 @@ struct end let _ = - MCP.register_analysis (module Spec : MCPSpec) \ No newline at end of file + MCP.register_analysis ~dep:["mallocFresh"] (module Spec : MCPSpec) \ No newline at end of file From fb68a36f1ed5d25e9cea01953e01c36b6cbc48c7 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sun, 4 Jun 2023 22:50:40 +0200 Subject: [PATCH 25/53] Remove printf's --- src/analyses/useAfterFree.ml | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index 4449242a97..f9fdb3da5c 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -35,7 +35,6 @@ struct let (_, o) = lval in offset_might_contain_freed o; (* Check the lval's offset *) match ctx.ask (Queries.MayPointTo (mkAddrOf lval)) with | a when not (Queries.LS.is_top a) && not (Queries.LS.mem (dummyFunDec.svar, `NoOffset) a) -> - ignore (Pretty.printf "WARN_LVAL %a\n" Queries.LS.pretty a); let v, o = Queries.LS.choose a in if ctx.ask (Queries.IsHeapVar v) && D.mem v state then M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "lval (%s) in \"%s\" points to a maybe freed memory region" v.vname transfer_fn_name @@ -126,7 +125,6 @@ struct | Free ptr -> begin match ctx.ask HeapVar with | `Lifted var -> - ignore (Pretty.printf "FREE: %a\n" CilType.Varinfo.pretty var); D.add var state | _ -> state end From 779e342ae1719110e02aad1a3d6092f046f5ad60 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sun, 4 Jun 2023 23:33:24 +0200 Subject: [PATCH 26/53] Fix handling of free() --- src/analyses/useAfterFree.ml | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index f9fdb3da5c..05d14b2cae 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -123,9 +123,12 @@ struct let desc = LibraryFunctions.find f in match desc.special arglist with | Free ptr -> - begin match ctx.ask HeapVar with - | `Lifted var -> - D.add var state + begin match ctx.ask (Queries.MayPointTo ptr) with + | a when not (Queries.LS.is_top a) && not (Queries.LS.mem (dummyFunDec.svar, `NoOffset) a) -> + let (v, _) = Queries.LS.choose a in + if ctx.ask (Queries.IsHeapVar v) then + D.add v state + else state | _ -> state end | _ -> state From 7ed8ef187e04fed92d4ccdce0272430d1de14947 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Thu, 8 Jun 2023 11:30:11 +0200 Subject: [PATCH 27/53] Add return 0 to each main in regression tests --- tests/regression/71-use_after_free/01-simple-uaf.c | 2 ++ tests/regression/71-use_after_free/02-conditional-uaf.c | 2 ++ tests/regression/71-use_after_free/03-nested-ptr-uaf.c | 2 ++ 3 files changed, 6 insertions(+) diff --git a/tests/regression/71-use_after_free/01-simple-uaf.c b/tests/regression/71-use_after_free/01-simple-uaf.c index c08f74a524..26f5ffe0f2 100644 --- a/tests/regression/71-use_after_free/01-simple-uaf.c +++ b/tests/regression/71-use_after_free/01-simple-uaf.c @@ -9,4 +9,6 @@ int main() { *ptr = 43; // Should report "Use After Free (CWE-416)" free(ptr); // Should report "Double Free (CWE-415)" + + return 0; } \ No newline at end of file diff --git a/tests/regression/71-use_after_free/02-conditional-uaf.c b/tests/regression/71-use_after_free/02-conditional-uaf.c index 6f84347946..54b695a3d6 100644 --- a/tests/regression/71-use_after_free/02-conditional-uaf.c +++ b/tests/regression/71-use_after_free/02-conditional-uaf.c @@ -13,4 +13,6 @@ int main() { *ptr = 43; // Should report "Use After Free (CWE-416)" free(ptr); // Should report "Double Free (CWE-415)" + + return 0; } \ No newline at end of file diff --git a/tests/regression/71-use_after_free/03-nested-ptr-uaf.c b/tests/regression/71-use_after_free/03-nested-ptr-uaf.c index 51c99355e4..aeca6efa28 100644 --- a/tests/regression/71-use_after_free/03-nested-ptr-uaf.c +++ b/tests/regression/71-use_after_free/03-nested-ptr-uaf.c @@ -13,4 +13,6 @@ int main() { if (a[*ptr] != 5) { // Should report "Use After Free (CWE-416)" free(ptr); // Should report "Double Free (CWE-415)" } + + return 0; } \ No newline at end of file From f9f47bef5ab89ddbaea57ade49a312eda7ec05f8 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Thu, 8 Jun 2023 11:32:20 +0200 Subject: [PATCH 28/53] Make sure to consider derefed ptrs accordingly when warning Also handle Not_Found exn from Set.choose --- src/analyses/useAfterFree.ml | 18 +++++++++++++----- 1 file changed, 13 insertions(+), 5 deletions(-) diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index 05d14b2cae..e6c7bf1fac 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -32,12 +32,20 @@ struct | Field (f, o) -> offset_might_contain_freed o | Index (e, o) -> warn_exp_might_contain_freed transfer_fn_name e ctx; offset_might_contain_freed o in - let (_, o) = lval in offset_might_contain_freed o; (* Check the lval's offset *) - match ctx.ask (Queries.MayPointTo (mkAddrOf lval)) with + let (lval_host, o) = lval in offset_might_contain_freed o; (* Check the lval's offset *) + let lval_to_query = + match lval_host with + | Var _ -> Lval lval + | Mem _ -> mkAddrOf lval (* Take the lval's address if its lhost is of the form *p, where p is a ptr *) + in + match ctx.ask (Queries.MayPointTo lval_to_query) with | a when not (Queries.LS.is_top a) && not (Queries.LS.mem (dummyFunDec.svar, `NoOffset) a) -> - let v, o = Queries.LS.choose a in - if ctx.ask (Queries.IsHeapVar v) && D.mem v state then - M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "lval (%s) in \"%s\" points to a maybe freed memory region" v.vname transfer_fn_name + begin try + let v, o = Queries.LS.choose a in + if ctx.ask (Queries.IsHeapVar v) && D.mem v state then + M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "lval (%s) in \"%s\" points to a maybe freed memory region" v.vname transfer_fn_name + with Not_found -> () + end | _ -> () and warn_exp_might_contain_freed ?(is_double_free = false) (transfer_fn_name:string) (exp:exp) ctx = From b6cf0527ae9089299e27e97d7dd3e3bd98af2ebf Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Thu, 8 Jun 2023 11:33:23 +0200 Subject: [PATCH 29/53] No need to depend on mallocFresh --- src/analyses/useAfterFree.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index e6c7bf1fac..8c949caf88 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -150,4 +150,4 @@ struct end let _ = - MCP.register_analysis ~dep:["mallocFresh"] (module Spec : MCPSpec) \ No newline at end of file + MCP.register_analysis (module Spec : MCPSpec) \ No newline at end of file From 26507ab40e8529cd72022e55046e9f37ca70708b Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Thu, 8 Jun 2023 11:36:17 +0200 Subject: [PATCH 30/53] Remove warn calls in combine_assign --- src/analyses/useAfterFree.ml | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index 8c949caf88..d519ef0994 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -120,8 +120,6 @@ struct D.join caller_state callee_local let combine_assign ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (callee_local:D.t) (f_ask: Queries.ask): D.t = - Option.iter (fun x -> warn_lval_might_contain_freed "combine_assign" x ctx) lval; - List.iter (fun arg -> warn_exp_might_contain_freed "combine_assign" arg ctx) args; ctx.local let special ctx (lval:lval option) (f:varinfo) (arglist:exp list) : D.t = From 517c90b19b11e64d6cdd81bd47ca5384efc6ad5b Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Thu, 8 Jun 2023 12:12:24 +0200 Subject: [PATCH 31/53] Put the UAF analysis' name in camel case --- src/analyses/useAfterFree.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index d519ef0994..551a149f3f 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -11,7 +11,7 @@ module Spec : Analyses.MCPSpec = struct include Analyses.DefaultSpec - let name () = "useafterfree" + let name () = "useAfterFree" module D = ToppedVarInfoSet module C = Lattice.Unit From 19b4bcd8ac678ad00d96ee4032462fd484ec1416 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Thu, 8 Jun 2023 15:20:21 +0200 Subject: [PATCH 32/53] Change top name to something more meaningful --- src/analyses/useAfterFree.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index 551a149f3f..5fe77d3091 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -4,8 +4,7 @@ open GoblintCil open Analyses open MessageCategory -(* TODO: Maybe come up with a better name for top at some point? *) -module ToppedVarInfoSet = SetDomain.ToppedSet(CilType.Varinfo)(struct let topname = "Unknown" end) +module ToppedVarInfoSet = SetDomain.ToppedSet(CilType.Varinfo)(struct let topname = "All Heap Variables" end) module Spec : Analyses.MCPSpec = struct From 7ce115ff3dc5b82a46f6fd8517de1dc79b883af5 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Thu, 8 Jun 2023 16:16:52 +0200 Subject: [PATCH 33/53] Annotate regression tests --- tests/regression/71-use_after_free/01-simple-uaf.c | 5 +++-- .../regression/71-use_after_free/02-conditional-uaf.c | 5 +++-- .../regression/71-use_after_free/03-nested-ptr-uaf.c | 7 ++++--- .../71-use_after_free/04-function-call-uaf.c | 11 ++++++----- 4 files changed, 16 insertions(+), 12 deletions(-) diff --git a/tests/regression/71-use_after_free/01-simple-uaf.c b/tests/regression/71-use_after_free/01-simple-uaf.c index 26f5ffe0f2..5a12179a24 100644 --- a/tests/regression/71-use_after_free/01-simple-uaf.c +++ b/tests/regression/71-use_after_free/01-simple-uaf.c @@ -1,3 +1,4 @@ +//PARAM: --set ana.activated[+] useAfterFree #include #include @@ -7,8 +8,8 @@ int main() { free(ptr); - *ptr = 43; // Should report "Use After Free (CWE-416)" - free(ptr); // Should report "Double Free (CWE-415)" + *ptr = 43; //WARN + free(ptr); //WARN return 0; } \ No newline at end of file diff --git a/tests/regression/71-use_after_free/02-conditional-uaf.c b/tests/regression/71-use_after_free/02-conditional-uaf.c index 54b695a3d6..f9873815fb 100644 --- a/tests/regression/71-use_after_free/02-conditional-uaf.c +++ b/tests/regression/71-use_after_free/02-conditional-uaf.c @@ -1,3 +1,4 @@ +//PARAM: --set ana.activated[+] useAfterFree #include #include @@ -11,8 +12,8 @@ int main() { free(ptr); } - *ptr = 43; // Should report "Use After Free (CWE-416)" - free(ptr); // Should report "Double Free (CWE-415)" + *ptr = 43; //WARN + free(ptr); //WARN return 0; } \ No newline at end of file diff --git a/tests/regression/71-use_after_free/03-nested-ptr-uaf.c b/tests/regression/71-use_after_free/03-nested-ptr-uaf.c index aeca6efa28..244a643706 100644 --- a/tests/regression/71-use_after_free/03-nested-ptr-uaf.c +++ b/tests/regression/71-use_after_free/03-nested-ptr-uaf.c @@ -1,3 +1,4 @@ +//PARAM: --set ana.activated[+] useAfterFree #include #include @@ -8,10 +9,10 @@ int main() { free(ptr); int a[2] = {0, 1}; - a[*ptr] = 5; // Should report "Use After Free (CWE-416)" + a[*ptr] = 5; //WARN - if (a[*ptr] != 5) { // Should report "Use After Free (CWE-416)" - free(ptr); // Should report "Double Free (CWE-415)" + if (a[*ptr] != 5) { //WARN + free(ptr); //WARN } return 0; diff --git a/tests/regression/71-use_after_free/04-function-call-uaf.c b/tests/regression/71-use_after_free/04-function-call-uaf.c index 0d14a8cb3c..f83f9966b4 100644 --- a/tests/regression/71-use_after_free/04-function-call-uaf.c +++ b/tests/regression/71-use_after_free/04-function-call-uaf.c @@ -1,3 +1,4 @@ +//PARAM: --set ana.activated[+] useAfterFree #include #include @@ -16,16 +17,16 @@ int main() { free(ptr1); free(ptr2); - f(ptr1, ptr2, ptr3); // Should report "Use After Free (CWE-416)" for "ptr1" and "ptr2" here + f(ptr1, ptr2, ptr3); //WARN - free(ptr3); // Should report "Double Free (CWE-415)" + free(ptr3); //WARN return 0; } void f(int *p1, int *p2, int *p3) { - *p1 = 5000; // Should report "Use After Free (CWE-416)" - free(p1); // Should report "Double Free (CWE-415)" - free(p2); // Should report "Double Free (CWE-415)" + *p1 = 5000; //WARN + free(p1); //WARN + free(p2); //WARN free(p3); } \ No newline at end of file From ee9f2ce8bbd6a6d236c7f0a7a2ed62cb8bee1b9b Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Thu, 8 Jun 2023 16:20:09 +0200 Subject: [PATCH 34/53] Add 2 more UAF regression tests --- .../05-uaf-free-in-wrapper-fun.c | 29 ++++++++++++ .../71-use_after_free/06-uaf-struct.c | 45 +++++++++++++++++++ 2 files changed, 74 insertions(+) create mode 100644 tests/regression/71-use_after_free/05-uaf-free-in-wrapper-fun.c create mode 100644 tests/regression/71-use_after_free/06-uaf-struct.c diff --git a/tests/regression/71-use_after_free/05-uaf-free-in-wrapper-fun.c b/tests/regression/71-use_after_free/05-uaf-free-in-wrapper-fun.c new file mode 100644 index 0000000000..e0eed9e800 --- /dev/null +++ b/tests/regression/71-use_after_free/05-uaf-free-in-wrapper-fun.c @@ -0,0 +1,29 @@ +//PARAM: --set ana.activated[+] useAfterFree +# include +# include +# include +# include +# include + +int *p, *p_alias; +char buf[10]; + +void bad_func() { + free(p); // exit() is missing +} + +int main (int argc, char *argv[]) { + int f = open(argv[1], O_RDONLY); + read(f, buf, 10); + p = malloc(sizeof(int)); + + if (buf[0] == 'A') { + p_alias = malloc(sizeof(int)); + p = p_alias; + } + if (buf[1] == 'F') + bad_func(); + if (buf[2] == 'U') + *p = 1; //WARN + return 0; +} \ No newline at end of file diff --git a/tests/regression/71-use_after_free/06-uaf-struct.c b/tests/regression/71-use_after_free/06-uaf-struct.c new file mode 100644 index 0000000000..02c4f3e77a --- /dev/null +++ b/tests/regression/71-use_after_free/06-uaf-struct.c @@ -0,0 +1,45 @@ +//PARAM: --set ana.activated[+] useAfterFree +#include +#include +#include +#include +#include + +struct auth { + char name[32]; + int auth; +}; + +struct auth *auth; +char *service; + +int main(int argc, char **argv) { + char line[128]; + + while (1) { + printf("[ auth = %p, service = %p ]\n", auth, service); //WARN + + if (fgets(line, sizeof(line), stdin) == NULL) break; + + if (strncmp(line, "auth ", 5) == 0) { + auth = malloc(sizeof(auth)); //WARN + memset(auth, 0, sizeof(auth)); //WARN + if (strlen(line + 5) < 31) { + strcpy(auth->name, line + 5); //WARN + } + } + if (strncmp(line, "reset", 5) == 0) { + free(auth); //WARN + } + if (strncmp(line, "service", 6) == 0) { + service = strdup(line + 7); + } + if (strncmp(line, "login", 5) == 0) { + if (auth->auth) { //WARN + printf("you have logged in already!\n"); + } else { + printf("please enter your password\n"); + } + } + } +} \ No newline at end of file From 621238719ac3a2e5574b9ed5fa78815a9dc8f60b Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Fri, 9 Jun 2023 13:50:55 +0200 Subject: [PATCH 35/53] Add regression test for double free detection (from ITC repo) --- .../71-use_after_free/07-itc-double-free.c | 222 ++++++++++++++++++ 1 file changed, 222 insertions(+) create mode 100644 tests/regression/71-use_after_free/07-itc-double-free.c diff --git a/tests/regression/71-use_after_free/07-itc-double-free.c b/tests/regression/71-use_after_free/07-itc-double-free.c new file mode 100644 index 0000000000..d0d35eccee --- /dev/null +++ b/tests/regression/71-use_after_free/07-itc-double-free.c @@ -0,0 +1,222 @@ +//PARAM: --set ana.activated[+] useAfterFree +#include + +void double_free_001() +{ + char* ptr= (char*) malloc(sizeof(char)); + free(ptr); + + free(ptr); //WARN (Double Free (CWE-415)) +} + +void double_free_002() +{ + char* ptr= (char*) malloc(10*sizeof(char)); + int i; + + for(i=0;i<10;i++) + { + ptr[i]='a'; + if(i==9) + { + free(ptr); + } + } + free(ptr); //WARN (Double Free (CWE-415)) +} + +void double_free_003() +{ + char* ptr= (char*) malloc(10*sizeof(char)); + int i; + + for(i=0;i<10;i++) + { + *(ptr+i)='a'; + if(i==9) + { + free(ptr); + } + } + free(ptr); //WARN (Double Free (CWE-415)) +} + +void double_free_004() +{ + char* ptr= (char*) malloc(10*sizeof(char)); + int i; + for(i=0;i<10;i++) + { + *(ptr+i)='a'; + } + + if (rand() % 2==0) + { + free(ptr); + } + + if(rand() % 3==0) + free(ptr); //WARN (Double Free (CWE-415)) +} + +void double_free_005() +{ + char* ptr= (char*) malloc(sizeof(char)); + free(ptr); + + if(ptr) + free(ptr); //WARN (Double Free (CWE-415)) +} + +void double_free_006() +{ + char* ptr= (char*) malloc(sizeof(char)); + if(1) + free(ptr); + + free(ptr); //WARN (Double Free (CWE-415)) +} + +void double_free_007() +{ + char* ptr= (char*) malloc(sizeof(char)); + int flag=0; + + if(flag>=0) + free(ptr); + + free(ptr); //WARN (Double Free (CWE-415)) +} + +char *double_free_function_008_gbl_ptr; + +void double_free_function_008() +{ + free (double_free_function_008_gbl_ptr); +} + +void double_free_008() +{ + double_free_function_008_gbl_ptr= (char*) malloc(sizeof(char)); + + double_free_function_008(); + free(double_free_function_008_gbl_ptr); //WARN (Double Free (CWE-415)) +} + +void double_free_009() +{ + char* ptr= (char*) malloc(sizeof(char)); + int flag=0; + + while(flag==0) + { + free(ptr); + flag++; + } + free(ptr); //WARN (Double Free (CWE-415)) +} + +void double_free_010() +{ + char* ptr= (char*) malloc(sizeof(char)); + int flag=1; + + while(flag) + { + free(ptr); + flag--; + } + free(ptr); //WARN (Double Free (CWE-415)) +} + +void double_free_011() +{ + char* ptr= (char*) malloc(sizeof(char)); + int flag=1,a=0,b=2; + + while(a Date: Fri, 9 Jun 2023 14:12:35 +0200 Subject: [PATCH 36/53] Add regression test for FP detection for double free (from ITC repo) --- .../71-use_after_free/08-itc-no-double-free.c | 206 ++++++++++++++++++ 1 file changed, 206 insertions(+) create mode 100644 tests/regression/71-use_after_free/08-itc-no-double-free.c diff --git a/tests/regression/71-use_after_free/08-itc-no-double-free.c b/tests/regression/71-use_after_free/08-itc-no-double-free.c new file mode 100644 index 0000000000..8071858703 --- /dev/null +++ b/tests/regression/71-use_after_free/08-itc-no-double-free.c @@ -0,0 +1,206 @@ +//PARAM: --set ana.activated[+] useAfterFree +#include + +void double_free_001() +{ + char* ptr= (char*) malloc(sizeof(char)); + + free(ptr); //NOWARN (Double Free (CWE-415)) +} + +void double_free_002() +{ + char* ptr= (char*) malloc(10*sizeof(char)); + int i; + + for(i=0;i<10;i++) + { + ptr[i]='a'; + if(i==10) + free(ptr); + } + free(ptr); //NOWARN (Double Free (CWE-415)) +} + +void double_free_003() +{ + char* ptr= (char*) malloc(10*sizeof(char)); + int i; + + for(i=0;i<10;i++) + { + *(ptr+i)='a'; + + } + + free(ptr); //NOWARN (Double Free (CWE-415)) +} + +void double_free_004() +{ + char* ptr= (char*) malloc(10*sizeof(char)); + int i; + for(i=0;i<10;i++) + { + *(ptr+i)='a'; + + } + free(ptr); //NOWARN (Double Free (CWE-415)) +} + +void double_free_005() +{ + char* ptr= (char*) malloc(sizeof(char)); + + if(ptr) + free(ptr); //NOWARN (Double Free (CWE-415)) +} + +void double_free_006() +{ + char* ptr= (char*) malloc(sizeof(char)); + if(0) + free(ptr); + + free(ptr); //NOWARN (Double Free (CWE-415)) +} + +void double_free_007() +{ + char* ptr= (char*) malloc(sizeof(char)); + int flag=0; + + if(flag<0) + free(ptr); + + free(ptr); //NOWARN (Double Free (CWE-415)) +} + +char *double_free_function_008_gbl_ptr; + +void double_free_function_008() +{ + free (double_free_function_008_gbl_ptr); //NOWARN (Double Free (CWE-415)) +} + +void double_free_008() +{ + double_free_function_008_gbl_ptr= (char*) malloc(sizeof(char)); + + double_free_function_008(); +} + +void double_free_009() +{ + char* ptr= (char*) malloc(sizeof(char)); + int flag=0; + + while(flag==1) + { + free(ptr); + flag++; + } + free(ptr); //NOWARN (Double Free (CWE-415)) +} + +void double_free_010() +{ + char* ptr= (char*) malloc(sizeof(char)); + int flag=1; + + while(flag) + { + free(ptr); //NOWARN (Double Free (CWE-415)) + flag--; + } +} + +void double_free_011() +{ + char* ptr= (char*) malloc(sizeof(char)); + int flag=1,a=0,b=1; + + while(a Date: Fri, 9 Jun 2023 14:55:00 +0200 Subject: [PATCH 37/53] Add UAF and Double Free regression tests (from Juliet Test Suite) --- .../71-use_after_free/09-juliet-uaf.c | 116 ++++++++++++++++++ .../71-use_after_free/10-juliet-double-free.c | 105 ++++++++++++++++ 2 files changed, 221 insertions(+) create mode 100644 tests/regression/71-use_after_free/09-juliet-uaf.c create mode 100644 tests/regression/71-use_after_free/10-juliet-double-free.c diff --git a/tests/regression/71-use_after_free/09-juliet-uaf.c b/tests/regression/71-use_after_free/09-juliet-uaf.c new file mode 100644 index 0000000000..5a5bf3ee32 --- /dev/null +++ b/tests/regression/71-use_after_free/09-juliet-uaf.c @@ -0,0 +1,116 @@ +//PARAM: --set ana.activated[+] useAfterFree +#include +#include +#include +#include + +static char * helperBad(char * aString) +{ + size_t i = 0; + size_t j; + char * reversedString = NULL; + if (aString != NULL) + { + i = strlen(aString); + reversedString = (char *) malloc(i+1); + if (reversedString == NULL) {exit(-1);} + for (j = 0; j < i; j++) + { + reversedString[j] = aString[i-j-1]; + } + reversedString[i] = '\0'; + + free(reversedString); + return reversedString; // WARN (Use After Free (CWE-416)) + } + else + { + return NULL; + } +} + +static char * helperGood(char * aString) +{ + size_t i = 0; + size_t j; + char * reversedString = NULL; + if (aString != NULL) + { + i = strlen(aString); + reversedString = (char *) malloc(i+1); + if (reversedString == NULL) {exit(-1);} + for (j = 0; j < i; j++) + { + reversedString[j] = aString[i-j-1]; + } + reversedString[i] = '\0'; + return reversedString; //NOWARN + } + else + { + return NULL; + } +} + +static int staticReturnsTrue() +{ + return 1; +} + +static int staticReturnsFalse() +{ + return 0; +} + +void CWE416_Use_After_Free__return_freed_ptr_08_bad() +{ + if(staticReturnsTrue()) + { + { + char * reversedString = helperBad("BadSink"); // WARN (Use After Free (CWE-416)) + printf("%s\n", reversedString); // WARN (Use After Free (CWE-416)) + } + } +} + +static void good1() +{ + if(staticReturnsFalse()) + { + /* INCIDENTAL: CWE 561 Dead Code, the code below will never run */ + printf("%s\n", "Benign, fixed string"); + } + else + { + { + char * reversedString = helperGood("GoodSink"); + printf("%s\n", reversedString); + } + } +} + +static void good2() +{ + if(staticReturnsTrue()) + { + { + char * reversedString = helperGood("GoodSink"); + printf("%s\n", reversedString); + } + } +} + +void CWE416_Use_After_Free__return_freed_ptr_08_good() +{ + good1(); + good2(); +} + + +int main(int argc, char * argv[]) +{ + CWE416_Use_After_Free__return_freed_ptr_08_good(); + CWE416_Use_After_Free__return_freed_ptr_08_bad(); + + return 0; +} \ No newline at end of file diff --git a/tests/regression/71-use_after_free/10-juliet-double-free.c b/tests/regression/71-use_after_free/10-juliet-double-free.c new file mode 100644 index 0000000000..c1ab5310c9 --- /dev/null +++ b/tests/regression/71-use_after_free/10-juliet-double-free.c @@ -0,0 +1,105 @@ +//PARAM: --set ana.activated[+] useAfterFree +#include +#include +#include +#include +#include + +typedef struct _twoIntsStruct { + int intOne; + int intTwo; +} twoIntsStruct; + +static int staticTrue = 1; /* true */ +static int staticFalse = 0; /* false */ + +void CWE415_Double_Free__malloc_free_struct_05_bad() +{ + twoIntsStruct * data; + data = NULL; + if(staticTrue) + { + data = (twoIntsStruct *)malloc(100*sizeof(twoIntsStruct)); + if (data == NULL) {exit(-1);} + free(data); + } + if(staticTrue) + { + free(data); //WARN (Double Free (CWE-415)) + } +} + +static void goodB2G1() +{ + twoIntsStruct * data; + data = NULL; + if(staticTrue) + { + data = (twoIntsStruct *)malloc(100*sizeof(twoIntsStruct)); + if (data == NULL) {exit(-1);} + free(data); + } +} + +static void goodB2G2() +{ + twoIntsStruct * data; + data = NULL; + if(staticTrue) + { + data = (twoIntsStruct *)malloc(100*sizeof(twoIntsStruct)); + if (data == NULL) {exit(-1);} + free(data); + } +} + +static void goodG2B1() +{ + twoIntsStruct * data; + data = NULL; + if(staticFalse) + { + /* INCIDENTAL: CWE 561 Dead Code, the code below will never run */ + printf("%s\n", "Benign, fixed string"); + } + else + { + data = (twoIntsStruct *)malloc(100*sizeof(twoIntsStruct)); + if (data == NULL) {exit(-1);} + } + if(staticTrue) + { + free(data); + } +} + +static void goodG2B2() +{ + twoIntsStruct * data; + data = NULL; + if(staticTrue) + { + data = (twoIntsStruct *)malloc(100*sizeof(twoIntsStruct)); + if (data == NULL) {exit(-1);} + } + if(staticTrue) + { + free(data); + } +} + +void CWE415_Double_Free__malloc_free_struct_05_good() +{ + goodB2G1(); + goodB2G2(); + goodG2B1(); + goodG2B2(); +} + +int main(int argc, char * argv[]) +{ + CWE415_Double_Free__malloc_free_struct_05_good(); + CWE415_Double_Free__malloc_free_struct_05_bad(); + + return 0; +} \ No newline at end of file From 1a70e8fe325b1eeb1b15fc4c2925838cd4dfd8cd Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Thu, 15 Jun 2023 11:41:51 +0200 Subject: [PATCH 38/53] Enable intervals for test case 71/08 Also add comments for a few spurious warnings in the same test case --- tests/regression/71-use_after_free/08-itc-no-double-free.c | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/tests/regression/71-use_after_free/08-itc-no-double-free.c b/tests/regression/71-use_after_free/08-itc-no-double-free.c index 8071858703..a5d2e38263 100644 --- a/tests/regression/71-use_after_free/08-itc-no-double-free.c +++ b/tests/regression/71-use_after_free/08-itc-no-double-free.c @@ -1,4 +1,4 @@ -//PARAM: --set ana.activated[+] useAfterFree +//PARAM: --set ana.activated[+] useAfterFree --enable ana.int.interval #include void double_free_001() @@ -110,6 +110,7 @@ void double_free_010() while(flag) { + // There might be a spurious warning here (due to the loop) free(ptr); //NOWARN (Double Free (CWE-415)) flag--; } @@ -123,6 +124,7 @@ void double_free_011() while(a Date: Wed, 21 Jun 2023 21:45:04 +0200 Subject: [PATCH 39/53] Add extra check for Not_found exception in "special" --- src/analyses/useAfterFree.ml | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index 5fe77d3091..eaa7401521 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -130,10 +130,13 @@ struct | Free ptr -> begin match ctx.ask (Queries.MayPointTo ptr) with | a when not (Queries.LS.is_top a) && not (Queries.LS.mem (dummyFunDec.svar, `NoOffset) a) -> - let (v, _) = Queries.LS.choose a in - if ctx.ask (Queries.IsHeapVar v) then - D.add v state - else state + begin try + let (v, _) = Queries.LS.choose a in + if ctx.ask (Queries.IsHeapVar v) then + D.add v state + else state + with Not_found -> state + end | _ -> state end | _ -> state From 80268f90f6600aeadee9956fc5465adf9cb7fd73 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Thu, 22 Jun 2023 11:29:29 +0200 Subject: [PATCH 40/53] Swap ctx and lval arguments of warn_lval_might_contain_freed --- src/analyses/useAfterFree.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index eaa7401521..607546512c 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -21,7 +21,7 @@ struct (* HELPER FUNCTIONS *) - let rec warn_lval_might_contain_freed ?(is_double_free = false) (transfer_fn_name:string) (lval:lval) ctx = + let rec warn_lval_might_contain_freed ?(is_double_free = false) (transfer_fn_name:string) ctx (lval:lval) = let state = ctx.local in let undefined_behavior = if is_double_free then Undefined DoubleFree else Undefined UseAfterFree in let cwe_number = if is_double_free then 415 else 416 in @@ -72,13 +72,13 @@ struct (* Lval cases (need [warn_lval_might_contain_freed] for them) *) | Lval lval | StartOf lval - | AddrOf lval -> warn_lval_might_contain_freed ~is_double_free transfer_fn_name lval ctx + | AddrOf lval -> warn_lval_might_contain_freed ~is_double_free transfer_fn_name ctx lval (* TRANSFER FUNCTIONS *) let assign ctx (lval:lval) (rval:exp) : D.t = - warn_lval_might_contain_freed "assign" lval ctx; + warn_lval_might_contain_freed "assign" ctx lval; warn_exp_might_contain_freed "assign" rval ctx; ctx.local @@ -95,7 +95,7 @@ struct let enter ctx (lval:lval option) (f:fundec) (args:exp list) : (D.t * D.t) list = let caller_state = ctx.local in - Option.iter (fun x -> warn_lval_might_contain_freed "enter" x ctx) lval; + Option.iter (fun x -> warn_lval_might_contain_freed "enter" ctx x) lval; List.iter (fun arg -> warn_exp_might_contain_freed "enter" arg ctx) args; if D.is_empty caller_state then [caller_state, caller_state] @@ -123,7 +123,7 @@ struct let special ctx (lval:lval option) (f:varinfo) (arglist:exp list) : D.t = let state = ctx.local in - Option.iter (fun x -> warn_lval_might_contain_freed ("special: " ^ f.vname) x ctx) lval; + Option.iter (fun x -> warn_lval_might_contain_freed ("special: " ^ f.vname) ctx x) lval; List.iter (fun arg -> warn_exp_might_contain_freed ~is_double_free:(f.vname = "free") ("special: " ^ f.vname) arg ctx) arglist; let desc = LibraryFunctions.find f in match desc.special arglist with From 6bfcf02a0e4bbda27846383265a92d7da3c4a062 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Thu, 22 Jun 2023 11:33:39 +0200 Subject: [PATCH 41/53] Swap exp and ctx arguments of warn_exp_might_contain_freed --- src/analyses/useAfterFree.ml | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index 607546512c..a0dfa605a5 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -29,7 +29,7 @@ struct match offset with | NoOffset -> () | Field (f, o) -> offset_might_contain_freed o - | Index (e, o) -> warn_exp_might_contain_freed transfer_fn_name e ctx; offset_might_contain_freed o + | Index (e, o) -> warn_exp_might_contain_freed transfer_fn_name ctx e; offset_might_contain_freed o in let (lval_host, o) = lval in offset_might_contain_freed o; (* Check the lval's offset *) let lval_to_query = @@ -47,7 +47,7 @@ struct end | _ -> () - and warn_exp_might_contain_freed ?(is_double_free = false) (transfer_fn_name:string) (exp:exp) ctx = + and warn_exp_might_contain_freed ?(is_double_free = false) (transfer_fn_name:string) ctx (exp:exp) = match exp with (* Base recursion cases *) | Const _ @@ -61,14 +61,14 @@ struct | SizeOfE e | AlignOfE e | UnOp (_, e, _) - | CastE (_, e) -> warn_exp_might_contain_freed ~is_double_free transfer_fn_name e ctx + | CastE (_, e) -> warn_exp_might_contain_freed ~is_double_free transfer_fn_name ctx e | BinOp (_, e1, e2, _) -> - warn_exp_might_contain_freed ~is_double_free transfer_fn_name e1 ctx; - warn_exp_might_contain_freed ~is_double_free transfer_fn_name e2 ctx + warn_exp_might_contain_freed ~is_double_free transfer_fn_name ctx e1; + warn_exp_might_contain_freed ~is_double_free transfer_fn_name ctx e2 | Question (e1, e2, e3, _) -> - warn_exp_might_contain_freed ~is_double_free transfer_fn_name e1 ctx; - warn_exp_might_contain_freed ~is_double_free transfer_fn_name e2 ctx; - warn_exp_might_contain_freed ~is_double_free transfer_fn_name e3 ctx + warn_exp_might_contain_freed ~is_double_free transfer_fn_name ctx e1; + warn_exp_might_contain_freed ~is_double_free transfer_fn_name ctx e2; + warn_exp_might_contain_freed ~is_double_free transfer_fn_name ctx e3 (* Lval cases (need [warn_lval_might_contain_freed] for them) *) | Lval lval | StartOf lval @@ -79,24 +79,24 @@ struct let assign ctx (lval:lval) (rval:exp) : D.t = warn_lval_might_contain_freed "assign" ctx lval; - warn_exp_might_contain_freed "assign" rval ctx; + warn_exp_might_contain_freed "assign" ctx rval; ctx.local let branch ctx (exp:exp) (tv:bool) : D.t = - warn_exp_might_contain_freed "branch" exp ctx; + warn_exp_might_contain_freed "branch" ctx exp; ctx.local let body ctx (f:fundec) : D.t = ctx.local let return ctx (exp:exp option) (f:fundec) : D.t = - Option.iter (fun x -> warn_exp_might_contain_freed "return" x ctx) exp; + Option.iter (fun x -> warn_exp_might_contain_freed "return" ctx x) exp; ctx.local let enter ctx (lval:lval option) (f:fundec) (args:exp list) : (D.t * D.t) list = let caller_state = ctx.local in Option.iter (fun x -> warn_lval_might_contain_freed "enter" ctx x) lval; - List.iter (fun arg -> warn_exp_might_contain_freed "enter" arg ctx) args; + List.iter (fun arg -> warn_exp_might_contain_freed "enter" ctx arg) args; if D.is_empty caller_state then [caller_state, caller_state] else ( @@ -124,7 +124,7 @@ struct let special ctx (lval:lval option) (f:varinfo) (arglist:exp list) : D.t = let state = ctx.local in Option.iter (fun x -> warn_lval_might_contain_freed ("special: " ^ f.vname) ctx x) lval; - List.iter (fun arg -> warn_exp_might_contain_freed ~is_double_free:(f.vname = "free") ("special: " ^ f.vname) arg ctx) arglist; + List.iter (fun arg -> warn_exp_might_contain_freed ~is_double_free:(f.vname = "free") ("special: " ^ f.vname) ctx arg) arglist; let desc = LibraryFunctions.find f in match desc.special arglist with | Free ptr -> From 2f729eed5ad5d22fe790934967b3f1c524167634 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Thu, 22 Jun 2023 14:00:32 +0200 Subject: [PATCH 42/53] Change calculation of callee_state in enter transfer function --- src/analyses/useAfterFree.ml | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index a0dfa605a5..d0cf01c3d5 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -104,13 +104,8 @@ struct if Queries.LS.is_top reachable_from_args || D.is_top caller_state then [caller_state, caller_state] else - let reachable_vars = - Queries.LS.elements reachable_from_args - |> List.map fst - |> List.filter (fun var -> ctx.ask (Queries.IsHeapVar var)) - |> D.of_list - in - let callee_state = D.inter caller_state reachable_vars in + let reachable_vars = List.map fst (Queries.LS.elements reachable_from_args) in + let callee_state = D.filter (fun var -> List.mem var reachable_vars) caller_state in [caller_state, callee_state] ) From d518665e4d8c0cba299f4d5a34c8a3bf4c1aaa67 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Thu, 22 Jun 2023 14:05:09 +0200 Subject: [PATCH 43/53] Move lval warn from enter to combine_assign --- src/analyses/useAfterFree.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index d0cf01c3d5..335b331d37 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -95,7 +95,6 @@ struct let enter ctx (lval:lval option) (f:fundec) (args:exp list) : (D.t * D.t) list = let caller_state = ctx.local in - Option.iter (fun x -> warn_lval_might_contain_freed "enter" ctx x) lval; List.iter (fun arg -> warn_exp_might_contain_freed "enter" ctx arg) args; if D.is_empty caller_state then [caller_state, caller_state] @@ -114,6 +113,7 @@ struct D.join caller_state callee_local let combine_assign ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (callee_local:D.t) (f_ask: Queries.ask): D.t = + Option.iter (fun x -> warn_lval_might_contain_freed "enter" ctx x) lval; ctx.local let special ctx (lval:lval option) (f:varinfo) (arglist:exp list) : D.t = From 2bb696c94e62a467bf5b69158b68bd9f9f140294 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Thu, 22 Jun 2023 14:07:34 +0200 Subject: [PATCH 44/53] Use consistent notation for Queries.LS.choose --- src/analyses/useAfterFree.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index 335b331d37..8998e72d4e 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -40,7 +40,7 @@ struct match ctx.ask (Queries.MayPointTo lval_to_query) with | a when not (Queries.LS.is_top a) && not (Queries.LS.mem (dummyFunDec.svar, `NoOffset) a) -> begin try - let v, o = Queries.LS.choose a in + let (v, _) = Queries.LS.choose a in if ctx.ask (Queries.IsHeapVar v) && D.mem v state then M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "lval (%s) in \"%s\" points to a maybe freed memory region" v.vname transfer_fn_name with Not_found -> () From 47eff4483145b24366c8b80089ffd1e8663cb01f Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Thu, 22 Jun 2023 21:37:42 +0200 Subject: [PATCH 45/53] Add all possibly pointed-to heap vars to state + warn for all of them as well --- src/analyses/useAfterFree.ml | 29 ++++++++++++++++------------- 1 file changed, 16 insertions(+), 13 deletions(-) diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index 8998e72d4e..0dabe96232 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -39,12 +39,16 @@ struct in match ctx.ask (Queries.MayPointTo lval_to_query) with | a when not (Queries.LS.is_top a) && not (Queries.LS.mem (dummyFunDec.svar, `NoOffset) a) -> - begin try - let (v, _) = Queries.LS.choose a in - if ctx.ask (Queries.IsHeapVar v) && D.mem v state then - M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "lval (%s) in \"%s\" points to a maybe freed memory region" v.vname transfer_fn_name - with Not_found -> () - end + let warn_for_heap_var var = + if D.mem var state then + M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "lval (%s) in \"%s\" points to a maybe freed memory region" var.vname transfer_fn_name + in + let pointed_to_heap_vars = + Queries.LS.elements a + |> List.map fst + |> List.filter (fun var -> ctx.ask (Queries.IsHeapVar var)) + in + List.iter warn_for_heap_var pointed_to_heap_vars (* Warn for all heap vars that the lval possibly points to *) | _ -> () and warn_exp_might_contain_freed ?(is_double_free = false) (transfer_fn_name:string) ctx (exp:exp) = @@ -125,13 +129,12 @@ struct | Free ptr -> begin match ctx.ask (Queries.MayPointTo ptr) with | a when not (Queries.LS.is_top a) && not (Queries.LS.mem (dummyFunDec.svar, `NoOffset) a) -> - begin try - let (v, _) = Queries.LS.choose a in - if ctx.ask (Queries.IsHeapVar v) then - D.add v state - else state - with Not_found -> state - end + let pointed_to_heap_vars = + Queries.LS.elements a + |> List.map fst + |> List.filter (fun var -> ctx.ask (Queries.IsHeapVar var)) + in + D.join state (D.of_list pointed_to_heap_vars) (* Add all heap vars, which ptr points to, to the state *) | _ -> state end | _ -> state From 9e5cd7a199a5b04c35215cced5d09727fb48bf61 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sat, 1 Jul 2023 14:25:21 +0200 Subject: [PATCH 46/53] Add regression test case with wrapper functions for malloc and free --- .../71-use_after_free/11-wrapper-funs-uaf.c | 35 +++++++++++++++++++ 1 file changed, 35 insertions(+) create mode 100644 tests/regression/71-use_after_free/11-wrapper-funs-uaf.c diff --git a/tests/regression/71-use_after_free/11-wrapper-funs-uaf.c b/tests/regression/71-use_after_free/11-wrapper-funs-uaf.c new file mode 100644 index 0000000000..dc467b5a57 --- /dev/null +++ b/tests/regression/71-use_after_free/11-wrapper-funs-uaf.c @@ -0,0 +1,35 @@ +//PARAM: --set ana.activated[+] useAfterFree +#include +#include + +void *my_malloc(size_t size) { + return malloc(size); +} + +void my_free(void *ptr) { + free(ptr); +} + +void *my_malloc2(size_t size) { + return my_malloc(size); +} + +void my_free2(void *ptr) { + my_free(ptr); +} + +int main(int argc, char const *argv[]) { + char *p = my_malloc2(50 * sizeof(char)); + + *(p + 42) = 'c'; //NOWARN + printf("%s", p); //NOWARN + + my_free2(p); + + *(p + 42) = 'c'; //WARN + printf("%s", p); //WARN + + char *p2 = p; //WARN + + return 0; +} From fd5a5134dc6be1c2e0ed056f35685d2f308e2774 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sat, 1 Jul 2023 14:37:16 +0200 Subject: [PATCH 47/53] Slightly update regression test for wrapper funs for malloc and free --- tests/regression/71-use_after_free/11-wrapper-funs-uaf.c | 3 +++ 1 file changed, 3 insertions(+) diff --git a/tests/regression/71-use_after_free/11-wrapper-funs-uaf.c b/tests/regression/71-use_after_free/11-wrapper-funs-uaf.c index dc467b5a57..3ed540b53d 100644 --- a/tests/regression/71-use_after_free/11-wrapper-funs-uaf.c +++ b/tests/regression/71-use_after_free/11-wrapper-funs-uaf.c @@ -31,5 +31,8 @@ int main(int argc, char const *argv[]) { char *p2 = p; //WARN + my_free2(p); //WARN + my_free2(p2); //WARN + return 0; } From a00814f3cd70d7d04831b36a206497fd5f3db9b7 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sat, 1 Jul 2023 14:52:11 +0200 Subject: [PATCH 48/53] Add test for UAF in multi-threaded context --- .../71-use_after_free/12-multi-threaded-uaf.c | 30 +++++++++++++++++++ 1 file changed, 30 insertions(+) create mode 100644 tests/regression/71-use_after_free/12-multi-threaded-uaf.c diff --git a/tests/regression/71-use_after_free/12-multi-threaded-uaf.c b/tests/regression/71-use_after_free/12-multi-threaded-uaf.c new file mode 100644 index 0000000000..0c647eff76 --- /dev/null +++ b/tests/regression/71-use_after_free/12-multi-threaded-uaf.c @@ -0,0 +1,30 @@ +//PARAM: --set ana.activated[+] useAfterFree +#include +#include +#include + +int* gptr; + +// Mutex to ensure we don't get race warnings, but the UAF warnings we actually care about +pthread_mutex_t mtx = PTHREAD_MUTEX_INITIALIZER; + +void *t_other(void* p) { + pthread_mutex_lock(&mtx); + free(gptr); //WARN + pthread_mutex_unlock(&mtx); +} + +int main() { + gptr = malloc(sizeof(int)); + *gptr = 42; + + pthread_t thread; + pthread_create(&thread, NULL, t_other, NULL); + + pthread_mutex_lock(&mtx); + *gptr = 43; //WARN + free(gptr); //WARN + pthread_mutex_unlock(&mtx); + + return 0; +} \ No newline at end of file From 9545618a3ccba1dc7bbca051f980c4fc1803bc09 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sat, 1 Jul 2023 14:52:37 +0200 Subject: [PATCH 49/53] Add simple WARN solution for multi-threaded programs with potential UAF --- src/analyses/useAfterFree.ml | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index 0dabe96232..6029915651 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -21,10 +21,15 @@ struct (* HELPER FUNCTIONS *) + let warn_for_multi_threaded ctx behavior cwe_number = + if not (ctx.ask (Queries.MustBeSingleThreaded)) then + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Program isn't running in single-threaded mode. Use-After-Free might occur due to multi-threading" + let rec warn_lval_might_contain_freed ?(is_double_free = false) (transfer_fn_name:string) ctx (lval:lval) = let state = ctx.local in let undefined_behavior = if is_double_free then Undefined DoubleFree else Undefined UseAfterFree in let cwe_number = if is_double_free then 415 else 416 in + warn_for_multi_threaded ctx undefined_behavior cwe_number; (* Simple solution to warn when multi-threaded *) let rec offset_might_contain_freed offset = match offset with | NoOffset -> () From b7b5d872b8062b0830196b4f44672c8b0658186d Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Fri, 7 Jul 2023 11:37:51 +0200 Subject: [PATCH 50/53] Use since_start for warn_for_multi_threaded in UAF analysis --- src/analyses/useAfterFree.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index 6029915651..bcfd9979fc 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -22,7 +22,7 @@ struct (* HELPER FUNCTIONS *) let warn_for_multi_threaded ctx behavior cwe_number = - if not (ctx.ask (Queries.MustBeSingleThreaded)) then + if not (ctx.ask (Queries.MustBeSingleThreaded { since_start = true })) then M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Program isn't running in single-threaded mode. Use-After-Free might occur due to multi-threading" let rec warn_lval_might_contain_freed ?(is_double_free = false) (transfer_fn_name:string) ctx (lval:lval) = From d81153b8b47fed85edda60a8f65558f126eb5e22 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Fri, 7 Jul 2023 11:38:29 +0200 Subject: [PATCH 51/53] Fix indentation --- src/analyses/baseInvariant.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml index 67563c0f1e..8878dc49f9 100644 --- a/src/analyses/baseInvariant.ml +++ b/src/analyses/baseInvariant.ml @@ -674,7 +674,7 @@ struct st'' (* Mixed Float and Int cases should never happen, as there are no binary operators with one float and one int parameter ?!*) | Int _, Float _ | Float _, Int _ -> failwith "ill-typed program"; - (* | Address a, Address b -> ... *) + (* | Address a, Address b -> ... *) | a1, a2 -> fallback (GobPretty.sprintf "binop: got abstract values that are not Int: %a and %a" VD.pretty a1 VD.pretty a2) st) (* use closures to avoid unused casts *) in (match c_typed with From 120735f63710277a598c1e9f864444bc71209ae2 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Fri, 7 Jul 2023 11:57:30 +0200 Subject: [PATCH 52/53] Move UAF regression tests into a different directory --- .../{71-use_after_free => 74-use_after_free}/01-simple-uaf.c | 0 .../{71-use_after_free => 74-use_after_free}/02-conditional-uaf.c | 0 .../{71-use_after_free => 74-use_after_free}/03-nested-ptr-uaf.c | 0 .../04-function-call-uaf.c | 0 .../05-uaf-free-in-wrapper-fun.c | 0 .../{71-use_after_free => 74-use_after_free}/06-uaf-struct.c | 0 .../{71-use_after_free => 74-use_after_free}/07-itc-double-free.c | 0 .../08-itc-no-double-free.c | 0 .../{71-use_after_free => 74-use_after_free}/09-juliet-uaf.c | 0 .../10-juliet-double-free.c | 0 .../11-wrapper-funs-uaf.c | 0 .../12-multi-threaded-uaf.c | 0 12 files changed, 0 insertions(+), 0 deletions(-) rename tests/regression/{71-use_after_free => 74-use_after_free}/01-simple-uaf.c (100%) rename tests/regression/{71-use_after_free => 74-use_after_free}/02-conditional-uaf.c (100%) rename tests/regression/{71-use_after_free => 74-use_after_free}/03-nested-ptr-uaf.c (100%) rename tests/regression/{71-use_after_free => 74-use_after_free}/04-function-call-uaf.c (100%) rename tests/regression/{71-use_after_free => 74-use_after_free}/05-uaf-free-in-wrapper-fun.c (100%) rename tests/regression/{71-use_after_free => 74-use_after_free}/06-uaf-struct.c (100%) rename tests/regression/{71-use_after_free => 74-use_after_free}/07-itc-double-free.c (100%) rename tests/regression/{71-use_after_free => 74-use_after_free}/08-itc-no-double-free.c (100%) rename tests/regression/{71-use_after_free => 74-use_after_free}/09-juliet-uaf.c (100%) rename tests/regression/{71-use_after_free => 74-use_after_free}/10-juliet-double-free.c (100%) rename tests/regression/{71-use_after_free => 74-use_after_free}/11-wrapper-funs-uaf.c (100%) rename tests/regression/{71-use_after_free => 74-use_after_free}/12-multi-threaded-uaf.c (100%) diff --git a/tests/regression/71-use_after_free/01-simple-uaf.c b/tests/regression/74-use_after_free/01-simple-uaf.c similarity index 100% rename from tests/regression/71-use_after_free/01-simple-uaf.c rename to tests/regression/74-use_after_free/01-simple-uaf.c diff --git a/tests/regression/71-use_after_free/02-conditional-uaf.c b/tests/regression/74-use_after_free/02-conditional-uaf.c similarity index 100% rename from tests/regression/71-use_after_free/02-conditional-uaf.c rename to tests/regression/74-use_after_free/02-conditional-uaf.c diff --git a/tests/regression/71-use_after_free/03-nested-ptr-uaf.c b/tests/regression/74-use_after_free/03-nested-ptr-uaf.c similarity index 100% rename from tests/regression/71-use_after_free/03-nested-ptr-uaf.c rename to tests/regression/74-use_after_free/03-nested-ptr-uaf.c diff --git a/tests/regression/71-use_after_free/04-function-call-uaf.c b/tests/regression/74-use_after_free/04-function-call-uaf.c similarity index 100% rename from tests/regression/71-use_after_free/04-function-call-uaf.c rename to tests/regression/74-use_after_free/04-function-call-uaf.c diff --git a/tests/regression/71-use_after_free/05-uaf-free-in-wrapper-fun.c b/tests/regression/74-use_after_free/05-uaf-free-in-wrapper-fun.c similarity index 100% rename from tests/regression/71-use_after_free/05-uaf-free-in-wrapper-fun.c rename to tests/regression/74-use_after_free/05-uaf-free-in-wrapper-fun.c diff --git a/tests/regression/71-use_after_free/06-uaf-struct.c b/tests/regression/74-use_after_free/06-uaf-struct.c similarity index 100% rename from tests/regression/71-use_after_free/06-uaf-struct.c rename to tests/regression/74-use_after_free/06-uaf-struct.c diff --git a/tests/regression/71-use_after_free/07-itc-double-free.c b/tests/regression/74-use_after_free/07-itc-double-free.c similarity index 100% rename from tests/regression/71-use_after_free/07-itc-double-free.c rename to tests/regression/74-use_after_free/07-itc-double-free.c diff --git a/tests/regression/71-use_after_free/08-itc-no-double-free.c b/tests/regression/74-use_after_free/08-itc-no-double-free.c similarity index 100% rename from tests/regression/71-use_after_free/08-itc-no-double-free.c rename to tests/regression/74-use_after_free/08-itc-no-double-free.c diff --git a/tests/regression/71-use_after_free/09-juliet-uaf.c b/tests/regression/74-use_after_free/09-juliet-uaf.c similarity index 100% rename from tests/regression/71-use_after_free/09-juliet-uaf.c rename to tests/regression/74-use_after_free/09-juliet-uaf.c diff --git a/tests/regression/71-use_after_free/10-juliet-double-free.c b/tests/regression/74-use_after_free/10-juliet-double-free.c similarity index 100% rename from tests/regression/71-use_after_free/10-juliet-double-free.c rename to tests/regression/74-use_after_free/10-juliet-double-free.c diff --git a/tests/regression/71-use_after_free/11-wrapper-funs-uaf.c b/tests/regression/74-use_after_free/11-wrapper-funs-uaf.c similarity index 100% rename from tests/regression/71-use_after_free/11-wrapper-funs-uaf.c rename to tests/regression/74-use_after_free/11-wrapper-funs-uaf.c diff --git a/tests/regression/71-use_after_free/12-multi-threaded-uaf.c b/tests/regression/74-use_after_free/12-multi-threaded-uaf.c similarity index 100% rename from tests/regression/71-use_after_free/12-multi-threaded-uaf.c rename to tests/regression/74-use_after_free/12-multi-threaded-uaf.c From 020d1ffae7d886a8a60ad08ed60d024e2f92f281 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Fri, 7 Jul 2023 12:37:57 +0200 Subject: [PATCH 53/53] Remove a few NOWARNs in 74/08 test due to imprecision --- .../74-use_after_free/08-itc-no-double-free.c | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/tests/regression/74-use_after_free/08-itc-no-double-free.c b/tests/regression/74-use_after_free/08-itc-no-double-free.c index a5d2e38263..f2f501f1bc 100644 --- a/tests/regression/74-use_after_free/08-itc-no-double-free.c +++ b/tests/regression/74-use_after_free/08-itc-no-double-free.c @@ -110,8 +110,8 @@ void double_free_010() while(flag) { - // There might be a spurious warning here (due to the loop) - free(ptr); //NOWARN (Double Free (CWE-415)) + // We're currently too unprecise to properly detect this below (due to the loop) + free(ptr); // (Double Free (CWE-415)) flag--; } } @@ -124,8 +124,8 @@ void double_free_011() while(a