diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index fab76f177b..9f080dfb62 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -31,7 +31,7 @@ struct let get_joined_threads man = man.ask Queries.MustJoinedThreads - let warn_for_multi_threaded_access man ?(is_double_free = false) (heap_var:varinfo) behavior cwe_number = + let warn_for_multi_threaded_access man ?(is_free = false) (heap_var:varinfo) behavior cwe_number = let freeing_threads = man.global heap_var in (* If we're single-threaded or there are no threads freeing the memory, we have nothing to WARN about *) if man.ask (Queries.MustBeSingleThreaded { since_start = true }) || G.is_empty freeing_threads then () @@ -58,76 +58,88 @@ struct | `Top -> true | `Bot -> false in - let bug_name = if is_double_free then "Double Free" else "Use After Free" in + let bug_name = if is_free then "Double Free" else "Use After Free" in match get_current_threadid man with | `Lifted current -> let possibly_started = G.exists (other_possibly_started current) freeing_threads in if possibly_started then begin - if is_double_free then set_mem_safety_flag InvalidFree else set_mem_safety_flag InvalidDeref; + if is_free then set_mem_safety_flag InvalidFree else set_mem_safety_flag InvalidDeref; M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "There's a thread that's been started in parallel with the memory-freeing threads for heap variable %a. %s might occur" CilType.Varinfo.pretty heap_var bug_name end else begin let current_is_unique = ThreadId.Thread.is_unique current in let any_equal_current threads = G.exists (equal_current current) threads in if not current_is_unique && any_equal_current freeing_threads then begin - if is_double_free then set_mem_safety_flag InvalidFree else set_mem_safety_flag InvalidDeref; + if is_free then set_mem_safety_flag InvalidFree else set_mem_safety_flag InvalidDeref; M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Current thread is not unique and a %s might occur for heap variable %a" bug_name CilType.Varinfo.pretty heap_var end else if HeapVars.mem heap_var (snd man.local) then begin - if is_double_free then set_mem_safety_flag InvalidFree else set_mem_safety_flag InvalidDeref; + if is_free then set_mem_safety_flag InvalidFree else set_mem_safety_flag InvalidDeref; M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "%s might occur in current unique thread %a for heap variable %a" bug_name ThreadIdDomain.Thread.pretty current CilType.Varinfo.pretty heap_var end end | `Top -> - if is_double_free then set_mem_safety_flag InvalidFree else set_mem_safety_flag InvalidDeref; + if is_free then set_mem_safety_flag InvalidFree else set_mem_safety_flag InvalidDeref; M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "CurrentThreadId is top. %s might occur for heap variable %a" bug_name CilType.Varinfo.pretty heap_var | `Bot -> M.warn ~category:MessageCategory.Analyzer "CurrentThreadId is bottom" end - let rec warn_lval_might_contain_freed ?(is_implicitly_derefed = false) ?(is_double_free = false) (transfer_fn_name:string) man (lval:lval) = - match is_implicitly_derefed, is_double_free, lval with + (** + [is_free] indicates that the lval is passed to free, i.e., whether we consider a call [free(lval)]. + *) + let rec warn_lval_might_contain_freed ?(is_implicitly_derefed = false) ?(is_free = false) (transfer_fn_name:string) man (lval:lval) = + match is_implicitly_derefed, is_free, lval with (* If we're not checking for a double-free and there's no deref happening, then there's no need to check for an invalid deref or an invalid free *) | false, false, (Var _, NoOffset) -> () | _ -> - let state = man.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 | NoOffset -> () - | Field (f, o) -> offset_might_contain_freed o - | Index (e, o) -> warn_exp_might_contain_freed transfer_fn_name man e; offset_might_contain_freed o + | Field (f, o) -> + offset_might_contain_freed o + | Index (e, o) -> + warn_exp_might_contain_freed transfer_fn_name man 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 = - 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 - begin match man.ask (Queries.MayPointTo lval_to_query) with - | ad when not (Queries.AD.is_top ad) -> - let warn_for_heap_var v = - if HeapVars.mem v (snd state) then begin - if is_double_free then set_mem_safety_flag InvalidFree else set_mem_safety_flag InvalidDeref; - 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 - end - in - let pointed_to_heap_vars = - Queries.AD.fold (fun addr vars -> - match addr with - | Queries.AD.Addr.Addr (v,_) when man.ask (Queries.IsAllocVar v) -> v :: vars - | _ -> vars - ) ad [] - in + let (lval_host, o) = lval in + offset_might_contain_freed o; (* Check the lval's offset *) + + let freed_heap_vars = snd man.local in + let undefined_behavior = if is_free then Undefined DoubleFree else Undefined UseAfterFree in + let cwe_number = if is_free then 415 else 416 in + + let check_adress adresses = + let warn_for_heap_var v = + if HeapVars.mem v freed_heap_vars then begin + if is_free then set_mem_safety_flag InvalidFree else set_mem_safety_flag InvalidDeref; + 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 + end + in + let pointed_to_heap_vars = + Queries.AD.fold (fun addr vars -> + match addr with + | Queries.AD.Addr.Addr (v,_) when man.ask (Queries.IsAllocVar v) -> v :: vars + | _ -> vars + ) adresses [] + in + if not (Queries.AD.is_top adresses) then begin (* Warn for all heap vars that the lval possibly points to *) List.iter warn_for_heap_var pointed_to_heap_vars; (* Warn for a potential multi-threaded UAF for all heap vars that the lval possibly points to *) - List.iter (fun heap_var -> warn_for_multi_threaded_access man ~is_double_free heap_var undefined_behavior cwe_number) pointed_to_heap_vars - | _ -> () - end + List.iter (fun heap_var -> warn_for_multi_threaded_access man ~is_free heap_var undefined_behavior cwe_number) pointed_to_heap_vars + end + in + let addresses = man.ask (Queries.MayPointTo (Lval lval)) in + check_adress addresses; + match lval_host with + | Var _ -> () + | Mem exp -> + (* We have (\*x).o', so we check recursively whether x has been freed. *) + warn_exp_might_contain_freed ~is_implicitly_derefed:true ~is_free:false transfer_fn_name man exp - and warn_exp_might_contain_freed ?(is_implicitly_derefed = false) ?(is_double_free = false) (transfer_fn_name:string) man (exp:exp) = + (** [is_free] indicates that the exp is passed to free, i.e., we consider a call [free(exp)]*) + and warn_exp_might_contain_freed ?(is_implicitly_derefed = false) ?(is_free = false) (transfer_fn_name:string) man (exp:exp) = match exp with (* Base recursion cases *) | Const _ @@ -141,18 +153,18 @@ struct | SizeOfE e | AlignOfE e | UnOp (_, e, _) - | CastE (_, e) -> warn_exp_might_contain_freed ~is_implicitly_derefed ~is_double_free transfer_fn_name man e + | CastE (_, e) -> warn_exp_might_contain_freed ~is_implicitly_derefed ~is_free transfer_fn_name man e | BinOp (_, e1, e2, _) -> - warn_exp_might_contain_freed ~is_implicitly_derefed ~is_double_free transfer_fn_name man e1; - warn_exp_might_contain_freed ~is_implicitly_derefed ~is_double_free transfer_fn_name man e2 + warn_exp_might_contain_freed ~is_implicitly_derefed ~is_free transfer_fn_name man e1; + warn_exp_might_contain_freed ~is_implicitly_derefed ~is_free transfer_fn_name man e2 | Question (e1, e2, e3, _) -> - warn_exp_might_contain_freed ~is_implicitly_derefed ~is_double_free transfer_fn_name man e1; - warn_exp_might_contain_freed ~is_implicitly_derefed ~is_double_free transfer_fn_name man e2; - warn_exp_might_contain_freed ~is_implicitly_derefed ~is_double_free transfer_fn_name man e3 + warn_exp_might_contain_freed ~is_implicitly_derefed ~is_free transfer_fn_name man e1; + warn_exp_might_contain_freed ~is_implicitly_derefed ~is_free transfer_fn_name man e2; + warn_exp_might_contain_freed ~is_implicitly_derefed ~is_free transfer_fn_name man e3 (* Lval cases (need [warn_lval_might_contain_freed] for them) *) | Lval lval | StartOf lval - | AddrOf lval -> warn_lval_might_contain_freed ~is_implicitly_derefed ~is_double_free transfer_fn_name man lval + | AddrOf lval -> warn_lval_might_contain_freed ~is_implicitly_derefed ~is_free transfer_fn_name man lval let side_effect_mem_free man freed_heap_vars threadid joined_threads = let side_effect_globals_to_heap_var heap_var = @@ -210,7 +222,7 @@ struct List.mem arg read_shallow_args || List.mem arg read_deep_args || List.mem arg write_shallow_args || List.mem arg write_deep_args in Option.iter (fun x -> warn_lval_might_contain_freed ("special: " ^ f.vname) man x) lval; - List.iter (fun arg -> warn_exp_might_contain_freed ~is_implicitly_derefed:(is_arg_implicitly_derefed arg) ~is_double_free:(match desc.special arglist with Free _ -> true | _ -> false) ("special: " ^ f.vname) man arg) arglist; + List.iter (fun arg -> warn_exp_might_contain_freed ~is_implicitly_derefed:(is_arg_implicitly_derefed arg) ~is_free:(match desc.special arglist with Free _ -> true | _ -> false) ("special: " ^ f.vname) man arg) arglist; match desc.special arglist with | Free ptr -> begin match man.ask (Queries.MayPointTo ptr) with diff --git a/tests/regression/75-invalid_free/14-double-free-deref.c b/tests/regression/75-invalid_free/14-double-free-deref.c new file mode 100644 index 0000000000..3bf22f34c9 --- /dev/null +++ b/tests/regression/75-invalid_free/14-double-free-deref.c @@ -0,0 +1,21 @@ +//PARAM: --set ana.activated[+] useAfterFree +#include + +struct A19 { + int *p; +}; + +void init_and_free(struct A19 *a) { + a->p = (int *)malloc(sizeof(int)); + + free(a->p); + free(a->p); //WARN +} + + +int main(void) { + struct A19 a19; + a19.p = NULL; + init_and_free(&a19); + return 0; +} diff --git a/tests/regression/75-invalid_free/15-use-after-free-indirect.c b/tests/regression/75-invalid_free/15-use-after-free-indirect.c new file mode 100644 index 0000000000..e550b0a293 --- /dev/null +++ b/tests/regression/75-invalid_free/15-use-after-free-indirect.c @@ -0,0 +1,24 @@ +//PARAM: --set ana.activated[+] useAfterFree +#include + +struct A19 { + int *p; +}; + + +void init_and_free(struct A19 *a) { + (*a).p = (int *)malloc(sizeof(int)); + + free(a); + // a is freed; use-after-free + *((*a).p) = 3; //WARN + + // a already freed; Thus, this not a double free, but a use-after-free. + free((*a).p); //WARN +} + +int main(void) { + struct A19 *a19p = (struct A19 *)malloc(sizeof(struct A19)); + init_and_free(a19p); + return 0; +} diff --git a/tests/regression/75-invalid_free/16-use-after-free-double-indirect.c b/tests/regression/75-invalid_free/16-use-after-free-double-indirect.c new file mode 100644 index 0000000000..d145234e43 --- /dev/null +++ b/tests/regression/75-invalid_free/16-use-after-free-double-indirect.c @@ -0,0 +1,28 @@ +//PARAM: --set ana.activated[+] useAfterFree +#include + +struct A19 { + int *p; +}; + +void init_and_free(struct A19 **a) { + (**a).p = (int *)malloc(sizeof(int)); + + free(a); + // a already freed; Thus, this not a double free, but a use-after-free. + *((**a).p) = 3; //WARN + + // a already freed; Thus, this not a double free, but a use-after-free. + free((**a).p); //WARN +} + + + +int main(void) { + struct A19 **a19pp = (struct A19 **)malloc(sizeof(struct A19*)); + struct A19 *a19p2 = (struct A19 *)malloc(sizeof(struct A19)); + + *a19pp = a19p2; + init_and_free(a19pp); + return 0; +}