diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index bcfd9979fc..c3aebc985e 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -1,10 +1,11 @@ -(** An analysis for the detection of use-after-free vulnerabilities. *) +(** An analysis for the detection of use-after-free vulnerabilities ([useAfterFree]). *) open GoblintCil open Analyses open MessageCategory module ToppedVarInfoSet = SetDomain.ToppedSet(CilType.Varinfo)(struct let topname = "All Heap Variables" end) +module ThreadIdSet = SetDomain.Make(ThreadIdDomain.ThreadLifted) module Spec : Analyses.MCPSpec = struct @@ -14,6 +15,8 @@ struct module D = ToppedVarInfoSet module C = Lattice.Unit + module G = ThreadIdSet + module V = VarinfoV (** TODO: Try out later in benchmarks to see how we perform with and without context-sensititivty *) let context _ _ = () @@ -21,15 +24,52 @@ struct (* HELPER FUNCTIONS *) - let warn_for_multi_threaded ctx behavior cwe_number = - 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 get_current_threadid ctx = + ctx.ask Queries.CurrentThreadId + + let warn_for_multi_threaded_access ctx (heap_var:varinfo) behavior cwe_number = + let freeing_threads = ctx.global heap_var in + (* If we're single-threaded or there are no threads freeing the memory, we have nothing to WARN about *) + if ctx.ask (Queries.MustBeSingleThreaded { since_start = true }) || ThreadIdSet.is_empty freeing_threads then () + else begin + let possibly_started current = function + | `Lifted tid -> + let threads = ctx.ask Queries.CreatedThreads in + let not_started = MHP.definitely_not_started (current, threads) tid in + let possibly_started = not not_started in + possibly_started + | `Top -> true + | `Bot -> false + in + let equal_current current = function + | `Lifted tid -> + ThreadId.Thread.equal current tid + | `Top -> true + | `Bot -> false + in + match get_current_threadid ctx with + | `Lifted current -> + let possibly_started = ThreadIdSet.exists (possibly_started current) freeing_threads in + if possibly_started then + 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. Use-After-Free might occur" CilType.Varinfo.pretty heap_var + else begin + let current_is_unique = ThreadId.Thread.is_unique current in + let any_equal_current threads = ThreadIdSet.exists (equal_current current) threads in + if not current_is_unique && any_equal_current freeing_threads then + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Current thread is not unique and a Use-After-Free might occur for heap variable %a" CilType.Varinfo.pretty heap_var + else if D.mem heap_var ctx.local then + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Use-After-Free might occur in current unique thread %a for heap variable %a" ThreadIdDomain.FlagConfiguredTID.pretty current CilType.Varinfo.pretty heap_var + end + | `Top -> + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "CurrentThreadId is top. A Use-After-Free might occur for heap variable %a" CilType.Varinfo.pretty heap_var + | `Bot -> + M.warn ~category:MessageCategory.Analyzer "CurrentThreadId is bottom" + end 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 -> () @@ -53,7 +93,9 @@ struct |> 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 *) + List.iter warn_for_heap_var pointed_to_heap_vars; (* Warn for all heap vars that the lval possibly points to *) + (* 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 ctx heap_var undefined_behavior cwe_number) pointed_to_heap_vars | _ -> () and warn_exp_might_contain_freed ?(is_double_free = false) (transfer_fn_name:string) ctx (exp:exp) = @@ -83,6 +125,10 @@ struct | StartOf lval | AddrOf lval -> warn_lval_might_contain_freed ~is_double_free transfer_fn_name ctx lval + let side_effect_mem_free ctx freed_heap_vars threadid = + let threadid = G.singleton threadid in + D.iter (fun var -> ctx.sideg var threadid) freed_heap_vars + (* TRANSFER FUNCTIONS *) @@ -138,8 +184,11 @@ struct Queries.LS.elements a |> List.map fst |> List.filter (fun var -> ctx.ask (Queries.IsHeapVar var)) + |> D.of_list in - D.join state (D.of_list pointed_to_heap_vars) (* Add all heap vars, which ptr points to, to the state *) + (* Side-effect the tid that's freeing all the heap vars collected here *) + side_effect_mem_free ctx pointed_to_heap_vars (get_current_threadid ctx); + D.join state (pointed_to_heap_vars) (* Add all heap vars, which ptr points to, to the state *) | _ -> state end | _ -> state