From a57112b0316c9000c35ee639198a299e5059fb7c Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Wed, 26 Jul 2023 16:54:03 +0200 Subject: [PATCH 01/22] Add regression test case with a joined thread --- ...13-multi-threaded-uaf-with-joined-thread.c | 33 +++++++++++++++++++ 1 file changed, 33 insertions(+) create mode 100644 tests/regression/74-use_after_free/13-multi-threaded-uaf-with-joined-thread.c diff --git a/tests/regression/74-use_after_free/13-multi-threaded-uaf-with-joined-thread.c b/tests/regression/74-use_after_free/13-multi-threaded-uaf-with-joined-thread.c new file mode 100644 index 0000000000..140e66eff8 --- /dev/null +++ b/tests/regression/74-use_after_free/13-multi-threaded-uaf-with-joined-thread.c @@ -0,0 +1,33 @@ +//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_use(void* p) { + pthread_mutex_lock(&mtx); + *gptr = 0; //NOWARN + pthread_mutex_unlock(&mtx); +} + +int main() { + gptr = malloc(sizeof(int)); + *gptr = 42; + + pthread_t using_thread; + pthread_create(&using_thread, NULL, t_use, NULL); + + // Join using_thread before freeing gptr in the main thread + pthread_join(using_thread, NULL); + + pthread_mutex_lock(&mtx); + *gptr = 43; //NOWARN + free(gptr); //WARN + pthread_mutex_unlock(&mtx); + + return 0; +} \ No newline at end of file From 0b3bfc99d1c261be0806de1f2e45e6fe7b5eea78 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Wed, 26 Jul 2023 17:31:25 +0200 Subject: [PATCH 02/22] Add global variable for detection of UAF occurrences --- src/analyses/useAfterFree.ml | 14 +++++++++++--- src/framework/analysisState.ml | 3 +++ 2 files changed, 14 insertions(+), 3 deletions(-) diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index c3aebc985e..591cbba448 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -50,17 +50,24 @@ struct match get_current_threadid ctx with | `Lifted current -> let possibly_started = ThreadIdSet.exists (possibly_started current) freeing_threads in - if possibly_started then + if possibly_started then begin + AnalysisState.svcomp_may_use_after_free := true; 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 + end 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 + if not current_is_unique && any_equal_current freeing_threads then begin + AnalysisState.svcomp_may_use_after_free := true; 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 + end + else if D.mem heap_var ctx.local then begin + AnalysisState.svcomp_may_use_after_free := true; 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 end | `Top -> + AnalysisState.svcomp_may_use_after_free := true; 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" @@ -86,6 +93,7 @@ struct | a when not (Queries.LS.is_top a) && not (Queries.LS.mem (dummyFunDec.svar, `NoOffset) a) -> let warn_for_heap_var var = if D.mem var state then + AnalysisState.svcomp_may_use_after_free := true; 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 = diff --git a/src/framework/analysisState.ml b/src/framework/analysisState.ml index 0f3a9f55bc..385fa26aef 100644 --- a/src/framework/analysisState.ml +++ b/src/framework/analysisState.ml @@ -7,6 +7,9 @@ let should_warn = ref false (** Whether signed overflow or underflow happened *) let svcomp_may_overflow = ref false +(** Whether a Use-After-Free (UAF) happened *) +let svcomp_may_use_after_free = ref false + (** A hack to see if we are currently doing global inits *) let global_initialization = ref false From 77f7e89a6cd42ab2052cb5afab7b816918b8f1e3 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Wed, 26 Jul 2023 17:31:49 +0200 Subject: [PATCH 03/22] Add SVComp result generation for memory safety Currently only considering UAF --- src/autoTune.ml | 4 ++++ src/witness/svcomp.ml | 1 + src/witness/svcompSpec.ml | 4 ++++ src/witness/witness.ml | 30 ++++++++++++++++++++++++++++++ 4 files changed, 39 insertions(+) diff --git a/src/autoTune.ml b/src/autoTune.ml index a267c3bf9b..bce12302cd 100644 --- a/src/autoTune.ml +++ b/src/autoTune.ml @@ -185,6 +185,7 @@ let enableAnalyses anas = (*does not consider dynamic calls!*) let notNeccessaryThreadAnalyses = ["race"; "deadlock"; "maylocks"; "symb_locks"; "thread"; "threadid"; "threadJoins"; "threadreturn"] +let memorySafetyAnalyses = ["useAfterFree"] let reduceThreadAnalyses () = let isThreadCreate = function | LibraryDesc.ThreadCreate _ -> true @@ -219,6 +220,9 @@ let focusOnSpecification () = | NoOverflow -> (*We focus on integer analysis*) set_bool "ana.int.def_exc" true; set_bool "ana.int.interval" true + | MemorySafety -> (* Enable the memory safety analyses *) + print_endline @@ "Specification: MemorySafety -> enabling memory safety analyses \"" ^ (String.concat ", " memorySafetyAnalyses) ^ "\""; + enableAnalyses memorySafetyAnalyses (*Detect enumerations and enable the "ana.int.enums" option*) exception EnumFound diff --git a/src/witness/svcomp.ml b/src/witness/svcomp.ml index a5a572d1c2..b762d2eb5d 100644 --- a/src/witness/svcomp.ml +++ b/src/witness/svcomp.ml @@ -52,6 +52,7 @@ struct | UnreachCall _ -> "unreach-call" | NoOverflow -> "no-overflow" | NoDataRace -> "no-data-race" (* not yet in SV-COMP/Benchexec *) + | MemorySafety -> "memory-safety" in "false(" ^ result_spec ^ ")" | Unknown -> "unknown" diff --git a/src/witness/svcompSpec.ml b/src/witness/svcompSpec.ml index 464c170251..784155ab9b 100644 --- a/src/witness/svcompSpec.ml +++ b/src/witness/svcompSpec.ml @@ -6,6 +6,7 @@ type t = | UnreachCall of string | NoDataRace | NoOverflow + | MemorySafety let of_string s = let s = String.strip s in @@ -16,6 +17,8 @@ let of_string s = NoDataRace else if global_not = "overflow" then NoOverflow + else if global_not = "memory-safety" then + MemorySafety else let call_regex = Str.regexp "call(\\(.*\\)())" in if Str.string_match call_regex global_not 0 then @@ -42,5 +45,6 @@ let to_string spec = | UnreachCall f -> "call(" ^ f ^ "())" | NoDataRace -> "data-race" | NoOverflow -> "overflow" + | MemorySafety -> "memory-safety" in "CHECK( init(main()), LTL(G ! " ^ global_not ^ ") )" diff --git a/src/witness/witness.ml b/src/witness/witness.ml index aff9a01383..6dc0d04034 100644 --- a/src/witness/witness.ml +++ b/src/witness/witness.ml @@ -472,6 +472,36 @@ struct in (module TaskResult:WitnessTaskResult) ) + | MemorySafety -> + let module TrivialArg = + struct + include Arg + let next _ = [] + end + in + if not !AnalysisState.svcomp_may_use_after_free then + let module TaskResult = + struct + module Arg = Arg + let result = Result.True + let invariant _ = Invariant.none + let is_violation _ = false + let is_sink _ = false + end + in + (module TaskResult:WitnessTaskResult) + else ( + let module TaskResult = + struct + module Arg = TrivialArg + let result = Result.Unknown + let invariant _ = Invariant.none + let is_violation _ = false + let is_sink _ = false + end + in + (module TaskResult:WitnessTaskResult) + ) let write entrystates = From cfef9bd7d3f08fb578bc44608bd6af549785d48e Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sun, 30 Jul 2023 14:13:32 +0200 Subject: [PATCH 04/22] Fix multi-line if expression --- src/analyses/useAfterFree.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index 591cbba448..3b189a6dea 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -92,9 +92,10 @@ 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) -> let warn_for_heap_var var = - if D.mem var state then + if D.mem var state then begin AnalysisState.svcomp_may_use_after_free := true; 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 + end in let pointed_to_heap_vars = Queries.LS.elements a From cbaffbb8de505036a1058d42376ded1630116965 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sun, 30 Jul 2023 15:00:07 +0200 Subject: [PATCH 05/22] Side-effect a tuple of tids and sets of joined threads This aims to improve precision --- src/analyses/useAfterFree.ml | 56 +++++++++++++++++++++++++----------- 1 file changed, 39 insertions(+), 17 deletions(-) diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index 3b189a6dea..31203e505d 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -5,7 +5,7 @@ open Analyses open MessageCategory module ToppedVarInfoSet = SetDomain.ToppedSet(CilType.Varinfo)(struct let topname = "All Heap Variables" end) -module ThreadIdSet = SetDomain.Make(ThreadIdDomain.ThreadLifted) +module ThreadIdWithJoinedThreads = SetDomain.Make(Lattice.Prod(ThreadIdDomain.ThreadLifted)(ConcDomain.MustThreadSet)) module Spec : Analyses.MCPSpec = struct @@ -15,7 +15,7 @@ struct module D = ToppedVarInfoSet module C = Lattice.Unit - module G = ThreadIdSet + module G = ThreadIdWithJoinedThreads module V = VarinfoV (** TODO: Try out later in benchmarks to see how we perform with and without context-sensititivty *) @@ -27,36 +27,41 @@ struct let get_current_threadid ctx = ctx.ask Queries.CurrentThreadId + let get_joined_threads ctx = + ctx.ask Queries.MustJoinedThreads + 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 () + if ctx.ask (Queries.MustBeSingleThreaded { since_start = true }) || ThreadIdWithJoinedThreads.is_empty freeing_threads then () else begin let possibly_started current = function - | `Lifted tid -> - let threads = ctx.ask Queries.CreatedThreads in + | `Lifted tid, joined_threads -> + let created_threads = ctx.ask Queries.CreatedThreads in + (* Discard joined threads, as they're supposed to be joined before the point of freeing the memory *) + let threads = ConcDomain.MustThreadSet.diff created_threads joined_threads 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 + | `Top, _ -> true + | `Bot, _ -> false in let equal_current current = function - | `Lifted tid -> + | `Lifted tid, _ -> ThreadId.Thread.equal current tid - | `Top -> true - | `Bot -> false + | `Top, _ -> true + | `Bot, _ -> false in match get_current_threadid ctx with | `Lifted current -> - let possibly_started = ThreadIdSet.exists (possibly_started current) freeing_threads in + let possibly_started = ThreadIdWithJoinedThreads.exists (possibly_started current) freeing_threads in if possibly_started then begin AnalysisState.svcomp_may_use_after_free := true; 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 end else begin let current_is_unique = ThreadId.Thread.is_unique current in - let any_equal_current threads = ThreadIdSet.exists (equal_current current) threads in + let any_equal_current threads = ThreadIdWithJoinedThreads.exists (equal_current current) threads in if not current_is_unique && any_equal_current freeing_threads then begin AnalysisState.svcomp_may_use_after_free := true; 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 @@ -134,9 +139,25 @@ 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 + let side_effect_mem_free ctx freed_heap_vars threadid joined_threads = + let side_effect_globals_to_heap_var heap_var globals_to_add = + let (tid_to_add, joined_threads_to_add) = globals_to_add in + let current_globals = ctx.global heap_var in + (* + * Check if there are tuples with the same first component (i.e., tid) + * If no, side-effect the globals that we receive here and be done + * If yes, join all second components together and side-effect a single global with + the tid as first component and the joined second components as a single second component + *) + let globals_with_same_tid = G.filter (fun (tid, _) -> ThreadIdDomain.ThreadLifted.equal tid tid_to_add) current_globals in + if G.is_empty globals_with_same_tid then + ctx.sideg heap_var (G.singleton globals_to_add) + else + let globals_to_add = G.fold (fun (t, j) (t_acc, j_acc) -> (t_acc, ConcDomain.MustThreadSet.join j j_acc)) globals_with_same_tid (tid_to_add, joined_threads_to_add) in + ctx.sideg heap_var (G.singleton globals_to_add) + in + let globals_to_side_effect = (threadid, joined_threads) in + D.iter (fun var -> side_effect_globals_to_heap_var var globals_to_side_effect) freed_heap_vars (* TRANSFER FUNCTIONS *) @@ -196,8 +217,9 @@ struct |> D.of_list in (* 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 *) + side_effect_mem_free ctx pointed_to_heap_vars (get_current_threadid ctx) (get_joined_threads ctx); + (* Add all heap vars, which ptr points to, to the state *) + D.join state (pointed_to_heap_vars) | _ -> state end | _ -> state From c01585dac6ecc8d2efb42ff21c302ddcb675d705 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Mon, 31 Jul 2023 18:50:25 +0200 Subject: [PATCH 06/22] Warn if threadJoins is deactivated --- src/analyses/useAfterFree.ml | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index 31203e505d..9a6484f624 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -1,5 +1,6 @@ (** An analysis for the detection of use-after-free vulnerabilities ([useAfterFree]). *) +open GobConfig open GoblintCil open Analyses open MessageCategory @@ -30,7 +31,16 @@ struct let get_joined_threads ctx = ctx.ask Queries.MustJoinedThreads + let warn_about_deactivated_thread_joins () = + if not @@ List.mem "threadJoins" @@ get_string_list "ana.activated" then + M.warn "Running without thread joins analysis. Multi-threaded UAF detection might be imprecise!" + let warn_for_multi_threaded_access ctx (heap_var:varinfo) behavior cwe_number = + (* + * We need the [threadJoins] analysis for making the multi-threaded UAF detection more precise + * Warn the user in case [threadJoins] is disabled + *) + warn_about_deactivated_thread_joins (); 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 }) || ThreadIdWithJoinedThreads.is_empty freeing_threads then () From 49a6d5440099df0f3e730a6c7949c680809a5f7e Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Mon, 31 Jul 2023 18:54:20 +0200 Subject: [PATCH 07/22] Update joined thread test case annotations --- .../13-multi-threaded-uaf-with-joined-thread.c | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/regression/74-use_after_free/13-multi-threaded-uaf-with-joined-thread.c b/tests/regression/74-use_after_free/13-multi-threaded-uaf-with-joined-thread.c index 140e66eff8..2ce291f9d1 100644 --- a/tests/regression/74-use_after_free/13-multi-threaded-uaf-with-joined-thread.c +++ b/tests/regression/74-use_after_free/13-multi-threaded-uaf-with-joined-thread.c @@ -1,4 +1,4 @@ -//PARAM: --set ana.activated[+] useAfterFree +//PARAM: --set ana.activated[+] useAfterFree --set ana.activated[+] threadJoins #include #include #include @@ -26,7 +26,7 @@ int main() { pthread_mutex_lock(&mtx); *gptr = 43; //NOWARN - free(gptr); //WARN + free(gptr); //NOWARN pthread_mutex_unlock(&mtx); return 0; From b02d0a743f51fd0afd79a6ba86eb46556bfc1e1f Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Wed, 2 Aug 2023 08:53:23 +0200 Subject: [PATCH 08/22] Remove threadJoins activation warning --- src/analyses/useAfterFree.ml | 9 --------- 1 file changed, 9 deletions(-) diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index 9a6484f624..437f19264b 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -31,16 +31,7 @@ struct let get_joined_threads ctx = ctx.ask Queries.MustJoinedThreads - let warn_about_deactivated_thread_joins () = - if not @@ List.mem "threadJoins" @@ get_string_list "ana.activated" then - M.warn "Running without thread joins analysis. Multi-threaded UAF detection might be imprecise!" - let warn_for_multi_threaded_access ctx (heap_var:varinfo) behavior cwe_number = - (* - * We need the [threadJoins] analysis for making the multi-threaded UAF detection more precise - * Warn the user in case [threadJoins] is disabled - *) - warn_about_deactivated_thread_joins (); 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 }) || ThreadIdWithJoinedThreads.is_empty freeing_threads then () From 50f20b0e1db69285385c28fe54bfc30d758fc163 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Wed, 2 Aug 2023 09:55:10 +0200 Subject: [PATCH 09/22] Use a map domain for the globals --- src/analyses/useAfterFree.ml | 53 ++++++++++++++++-------------------- 1 file changed, 24 insertions(+), 29 deletions(-) diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index 437f19264b..c1f963b466 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -6,7 +6,7 @@ open Analyses open MessageCategory module ToppedVarInfoSet = SetDomain.ToppedSet(CilType.Varinfo)(struct let topname = "All Heap Variables" end) -module ThreadIdWithJoinedThreads = SetDomain.Make(Lattice.Prod(ThreadIdDomain.ThreadLifted)(ConcDomain.MustThreadSet)) +module ThreadIdToJoinedThreadsMap = MapDomain.MapBot(ThreadIdDomain.ThreadLifted)(ConcDomain.MustThreadSet) module Spec : Analyses.MCPSpec = struct @@ -16,7 +16,7 @@ struct module D = ToppedVarInfoSet module C = Lattice.Unit - module G = ThreadIdWithJoinedThreads + module G = ThreadIdToJoinedThreadsMap module V = VarinfoV (** TODO: Try out later in benchmarks to see how we perform with and without context-sensititivty *) @@ -34,35 +34,37 @@ struct 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 }) || ThreadIdWithJoinedThreads.is_empty freeing_threads then () + if ctx.ask (Queries.MustBeSingleThreaded { since_start = true }) || G.is_empty freeing_threads then () else begin - let possibly_started current = function - | `Lifted tid, joined_threads -> + let possibly_started current tid joined_threads = + match tid with + | `Lifted tid -> let created_threads = ctx.ask Queries.CreatedThreads in (* Discard joined threads, as they're supposed to be joined before the point of freeing the memory *) let threads = ConcDomain.MustThreadSet.diff created_threads joined_threads 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 + | `Top -> true + | `Bot -> false in - let equal_current current = function - | `Lifted tid, _ -> + let equal_current current tid joined_threads = + match tid with + | `Lifted tid -> ThreadId.Thread.equal current tid - | `Top, _ -> true - | `Bot, _ -> false + | `Top -> true + | `Bot -> false in match get_current_threadid ctx with | `Lifted current -> - let possibly_started = ThreadIdWithJoinedThreads.exists (possibly_started current) freeing_threads in + let possibly_started = G.exists (possibly_started current) freeing_threads in if possibly_started then begin AnalysisState.svcomp_may_use_after_free := true; 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 end else begin let current_is_unique = ThreadId.Thread.is_unique current in - let any_equal_current threads = ThreadIdWithJoinedThreads.exists (equal_current current) threads 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 AnalysisState.svcomp_may_use_after_free := true; 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 @@ -141,24 +143,17 @@ struct | 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 joined_threads = - let side_effect_globals_to_heap_var heap_var globals_to_add = - let (tid_to_add, joined_threads_to_add) = globals_to_add in + let side_effect_globals_to_heap_var heap_var = let current_globals = ctx.global heap_var in - (* - * Check if there are tuples with the same first component (i.e., tid) - * If no, side-effect the globals that we receive here and be done - * If yes, join all second components together and side-effect a single global with - the tid as first component and the joined second components as a single second component - *) - let globals_with_same_tid = G.filter (fun (tid, _) -> ThreadIdDomain.ThreadLifted.equal tid tid_to_add) current_globals in - if G.is_empty globals_with_same_tid then - ctx.sideg heap_var (G.singleton globals_to_add) - else - let globals_to_add = G.fold (fun (t, j) (t_acc, j_acc) -> (t_acc, ConcDomain.MustThreadSet.join j j_acc)) globals_with_same_tid (tid_to_add, joined_threads_to_add) in - ctx.sideg heap_var (G.singleton globals_to_add) + let joined_threads_to_add = match G.find_opt threadid current_globals with + | Some threads -> ConcDomain.ThreadSet.inter joined_threads threads + | None -> joined_threads + in + let globals_to_side_effect = G.add threadid joined_threads_to_add current_globals in + ctx.sideg heap_var globals_to_side_effect in - let globals_to_side_effect = (threadid, joined_threads) in - D.iter (fun var -> side_effect_globals_to_heap_var var globals_to_side_effect) freed_heap_vars + D.iter side_effect_globals_to_heap_var freed_heap_vars + (* TRANSFER FUNCTIONS *) From c90fb0f11a3070c9c92534232a06008b0c2beb32 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Wed, 2 Aug 2023 14:27:40 +0200 Subject: [PATCH 10/22] Add global vars for all three memory safety SVComp properties --- src/framework/analysisState.ml | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/framework/analysisState.ml b/src/framework/analysisState.ml index 385fa26aef..e987c414f2 100644 --- a/src/framework/analysisState.ml +++ b/src/framework/analysisState.ml @@ -10,6 +10,12 @@ let svcomp_may_overflow = ref false (** Whether a Use-After-Free (UAF) happened *) let svcomp_may_use_after_free = ref false +(** Whether an invalid pointer dereference happened *) +let svcomp_may_invalid_deref = ref false + +(** Whether an invalid memtrack happened *) +let svcomp_may_invalid_memtrack = ref false + (** A hack to see if we are currently doing global inits *) let global_initialization = ref false From e28f72b22f55fa0412d14b5877c8c90577c1c3eb Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Wed, 2 Aug 2023 14:29:13 +0200 Subject: [PATCH 11/22] Improve SVComp result generation and support all 3 memory-safety props --- src/autoTune.ml | 11 ++++--- src/witness/svcomp.ml | 4 ++- src/witness/svcompSpec.ml | 41 +++++++++++++++++++------- src/witness/witness.ml | 62 ++++++++++++++++++++++++++++++++++++++- 4 files changed, 101 insertions(+), 17 deletions(-) diff --git a/src/autoTune.ml b/src/autoTune.ml index bce12302cd..d532081799 100644 --- a/src/autoTune.ml +++ b/src/autoTune.ml @@ -185,7 +185,6 @@ let enableAnalyses anas = (*does not consider dynamic calls!*) let notNeccessaryThreadAnalyses = ["race"; "deadlock"; "maylocks"; "symb_locks"; "thread"; "threadid"; "threadJoins"; "threadreturn"] -let memorySafetyAnalyses = ["useAfterFree"] let reduceThreadAnalyses () = let isThreadCreate = function | LibraryDesc.ThreadCreate _ -> true @@ -220,9 +219,13 @@ let focusOnSpecification () = | NoOverflow -> (*We focus on integer analysis*) set_bool "ana.int.def_exc" true; set_bool "ana.int.interval" true - | MemorySafety -> (* Enable the memory safety analyses *) - print_endline @@ "Specification: MemorySafety -> enabling memory safety analyses \"" ^ (String.concat ", " memorySafetyAnalyses) ^ "\""; - enableAnalyses memorySafetyAnalyses + | ValidFree -> (* Enable the useAfterFree analysis *) + let uafAna = ["useAfterFree"] in + print_endline @@ "Specification: ValidFree -> enabling useAfterFree analysis \"" ^ (String.concat ", " uafAna) ^ "\""; + enableAnalyses uafAna + (* TODO: Finish these two below later *) + | ValidDeref + | ValidMemtrack -> () (*Detect enumerations and enable the "ana.int.enums" option*) exception EnumFound diff --git a/src/witness/svcomp.ml b/src/witness/svcomp.ml index b762d2eb5d..f1ee18ed72 100644 --- a/src/witness/svcomp.ml +++ b/src/witness/svcomp.ml @@ -52,7 +52,9 @@ struct | UnreachCall _ -> "unreach-call" | NoOverflow -> "no-overflow" | NoDataRace -> "no-data-race" (* not yet in SV-COMP/Benchexec *) - | MemorySafety -> "memory-safety" + | ValidFree -> "valid-free" + | ValidDeref -> "valid-deref" + | ValidMemtrack -> "valid-memtrack" in "false(" ^ result_spec ^ ")" | Unknown -> "unknown" diff --git a/src/witness/svcompSpec.ml b/src/witness/svcompSpec.ml index 784155ab9b..8dafb8873c 100644 --- a/src/witness/svcompSpec.ml +++ b/src/witness/svcompSpec.ml @@ -6,19 +6,20 @@ type t = | UnreachCall of string | NoDataRace | NoOverflow - | MemorySafety + | ValidFree + | ValidDeref + | ValidMemtrack let of_string s = let s = String.strip s in - let regexp = Str.regexp "CHECK( init(main()), LTL(G ! \\(.*\\)) )" in - if Str.string_match regexp s 0 then + let regexp = Str.regexp "CHECK( init(main()), LTL(G \\(.*\\)) )" in + let regexp_negated = Str.regexp "CHECK( init(main()), LTL(G ! \\(.*\\)) )" in + if Str.string_match regexp_negated s 0 then let global_not = Str.matched_group 1 s in if global_not = "data-race" then NoDataRace else if global_not = "overflow" then NoOverflow - else if global_not = "memory-safety" then - MemorySafety else let call_regex = Str.regexp "call(\\(.*\\)())" in if Str.string_match call_regex global_not 0 then @@ -26,6 +27,16 @@ let of_string s = UnreachCall f else failwith "Svcomp.Specification.of_string: unknown global not expression" + else if Str.string_match regexp s 0 then + let global = Str.matched_group 1 s in + if global = "valid-free" then + ValidFree + else if global = "valid-deref" then + ValidDeref + else if global = "valid-memtrack" then + ValidMemtrack + else + failwith "Svcomp.Specification.of_string: unknown global expression" else failwith "Svcomp.Specification.of_string: unknown expression" @@ -41,10 +52,18 @@ let of_option () = of_string s let to_string spec = - let global_not = match spec with - | UnreachCall f -> "call(" ^ f ^ "())" - | NoDataRace -> "data-race" - | NoOverflow -> "overflow" - | MemorySafety -> "memory-safety" + let print_output spec_str is_neg = + if is_neg then + Printf.sprintf "CHECK( init(main()), LTL(G ! %s) )" spec_str + else + Printf.sprintf "CHECK( init(main()), LTL(G %s) )" spec_str + in + let spec_str, is_neg = match spec with + | UnreachCall f -> "call(" ^ f ^ "())", true + | NoDataRace -> "data-race", true + | NoOverflow -> "overflow", true + | ValidFree -> "valid-free", false + | ValidDeref -> "valid-deref", false + | ValidMemtrack -> "valid-memtrack", false in - "CHECK( init(main()), LTL(G ! " ^ global_not ^ ") )" + print_output spec_str is_neg diff --git a/src/witness/witness.ml b/src/witness/witness.ml index 6dc0d04034..797541c606 100644 --- a/src/witness/witness.ml +++ b/src/witness/witness.ml @@ -472,7 +472,7 @@ struct in (module TaskResult:WitnessTaskResult) ) - | MemorySafety -> + | ValidFree -> let module TrivialArg = struct include Arg @@ -502,6 +502,66 @@ struct in (module TaskResult:WitnessTaskResult) ) + | ValidDeref -> + let module TrivialArg = + struct + include Arg + let next _ = [] + end + in + if not !AnalysisState.svcomp_may_invalid_deref then + let module TaskResult = + struct + module Arg = Arg + let result = Result.True + let invariant _ = Invariant.none + let is_violation _ = false + let is_sink _ = false + end + in + (module TaskResult:WitnessTaskResult) + else ( + let module TaskResult = + struct + module Arg = TrivialArg + let result = Result.Unknown + let invariant _ = Invariant.none + let is_violation _ = false + let is_sink _ = false + end + in + (module TaskResult:WitnessTaskResult) + ) + | ValidMemtrack -> + let module TrivialArg = + struct + include Arg + let next _ = [] + end + in + if not !AnalysisState.svcomp_may_invalid_memtrack then + let module TaskResult = + struct + module Arg = Arg + let result = Result.True + let invariant _ = Invariant.none + let is_violation _ = false + let is_sink _ = false + end + in + (module TaskResult:WitnessTaskResult) + else ( + let module TaskResult = + struct + module Arg = TrivialArg + let result = Result.Unknown + let invariant _ = Invariant.none + let is_violation _ = false + let is_sink _ = false + end + in + (module TaskResult:WitnessTaskResult) + ) let write entrystates = From a054a4f401772ea3318c640d4c0827dbce37e778 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sat, 26 Aug 2023 12:29:39 +0200 Subject: [PATCH 12/22] Warn for UAF only in case there's a deref happening --- src/analyses/useAfterFree.ml | 65 +++++++++++++++++++----------------- 1 file changed, 35 insertions(+), 30 deletions(-) diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index c1f963b466..e88cfc1e51 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -82,38 +82,43 @@ struct 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 - 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 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 = - 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 warn_for_heap_var var = - if D.mem var state then begin - AnalysisState.svcomp_may_use_after_free := true; - 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 - end + match is_double_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, (Var _, NoOffset) -> () + | _ -> + 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 = function + | NoOffset -> () + | Field (f, o) -> 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 pointed_to_heap_vars = - Queries.LS.elements a - |> List.map fst - |> List.filter (fun var -> ctx.ask (Queries.IsHeapVar var)) + 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 - 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 - | _ -> () + begin 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 warn_for_heap_var var = + if D.mem var state then begin + AnalysisState.svcomp_may_use_after_free := true; + 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 + end + in + let pointed_to_heap_vars = + Queries.LS.elements a + |> List.map fst + |> List.filter (fun var -> ctx.ask (Queries.IsHeapVar var)) + in + (* 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 ctx heap_var undefined_behavior cwe_number) pointed_to_heap_vars + | _ -> () + end and warn_exp_might_contain_freed ?(is_double_free = false) (transfer_fn_name:string) ctx (exp:exp) = match exp with From 32714309d38154f3af572c8186879cc6eb7da176 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sat, 26 Aug 2023 12:30:01 +0200 Subject: [PATCH 13/22] Adapt regression tests to not WARN for UAF if there's no deref --- .../74-use_after_free/04-function-call-uaf.c | 3 ++- tests/regression/74-use_after_free/06-uaf-struct.c | 8 +++++--- tests/regression/74-use_after_free/09-juliet-uaf.c | 8 +++++--- .../74-use_after_free/11-wrapper-funs-uaf.c | 12 +++++++----- 4 files changed, 19 insertions(+), 12 deletions(-) diff --git a/tests/regression/74-use_after_free/04-function-call-uaf.c b/tests/regression/74-use_after_free/04-function-call-uaf.c index f83f9966b4..d110db9edc 100644 --- a/tests/regression/74-use_after_free/04-function-call-uaf.c +++ b/tests/regression/74-use_after_free/04-function-call-uaf.c @@ -17,7 +17,8 @@ int main() { free(ptr1); free(ptr2); - f(ptr1, ptr2, ptr3); //WARN + // No deref happening in the function call, hence nothing to warn about + f(ptr1, ptr2, ptr3); //NOWARN free(ptr3); //WARN diff --git a/tests/regression/74-use_after_free/06-uaf-struct.c b/tests/regression/74-use_after_free/06-uaf-struct.c index 02c4f3e77a..13eed8e3db 100644 --- a/tests/regression/74-use_after_free/06-uaf-struct.c +++ b/tests/regression/74-use_after_free/06-uaf-struct.c @@ -17,13 +17,15 @@ int main(int argc, char **argv) { char line[128]; while (1) { - printf("[ auth = %p, service = %p ]\n", auth, service); //WARN + // No deref happening here => nothing to warn about + printf("[ auth = %p, service = %p ]\n", auth, service); //NOWARN 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 + // No deref happening in either of the 2 lines below => no need to warn + auth = malloc(sizeof(auth)); //NOWARN + memset(auth, 0, sizeof(auth)); //NOWARN if (strlen(line + 5) < 31) { strcpy(auth->name, line + 5); //WARN } diff --git a/tests/regression/74-use_after_free/09-juliet-uaf.c b/tests/regression/74-use_after_free/09-juliet-uaf.c index 5a5bf3ee32..c37ef26aca 100644 --- a/tests/regression/74-use_after_free/09-juliet-uaf.c +++ b/tests/regression/74-use_after_free/09-juliet-uaf.c @@ -21,7 +21,8 @@ static char * helperBad(char * aString) reversedString[i] = '\0'; free(reversedString); - return reversedString; // WARN (Use After Free (CWE-416)) + // No need to warn in the line below, as there's no dereferencing happening + return reversedString; // NOWARN } else { @@ -67,8 +68,9 @@ 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)) + // No need to warn in the two lines below, since there's no dereferencing of the freed memory + char * reversedString = helperBad("BadSink"); // NOWARN + printf("%s\n", reversedString); // NOWARN } } } diff --git a/tests/regression/74-use_after_free/11-wrapper-funs-uaf.c b/tests/regression/74-use_after_free/11-wrapper-funs-uaf.c index 3ed540b53d..6ae79e0062 100644 --- a/tests/regression/74-use_after_free/11-wrapper-funs-uaf.c +++ b/tests/regression/74-use_after_free/11-wrapper-funs-uaf.c @@ -27,12 +27,14 @@ int main(int argc, char const *argv[]) { my_free2(p); *(p + 42) = 'c'; //WARN - printf("%s", p); //WARN - - char *p2 = p; //WARN + // No dereferencing in the line below => no need to warn + printf("%s", p); //NOWARN - my_free2(p); //WARN - my_free2(p2); //WARN + // No dereferencing happening in the lines below => no need to warn for an invalid-deref + // Also no need to warn for an invalid-free, as the call to free is within these functions and they're not the "free" function itself + char *p2 = p; //NOWARN + my_free2(p); //NOWARN + my_free2(p2); //NOWARN return 0; } From d49db71fee1a9ffc125cf373eaa0bf2dab0baa58 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sat, 26 Aug 2023 14:38:23 +0200 Subject: [PATCH 14/22] Clean up and use proper global vars for SV-COMP --- src/analyses/useAfterFree.ml | 21 +++++++++++++-------- src/framework/analysisState.ml | 4 ++-- src/witness/witness.ml | 2 +- 3 files changed, 16 insertions(+), 11 deletions(-) diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index e88cfc1e51..6e2ca3b04f 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -1,6 +1,5 @@ (** An analysis for the detection of use-after-free vulnerabilities ([useAfterFree]). *) -open GobConfig open GoblintCil open Analyses open MessageCategory @@ -25,13 +24,19 @@ struct (* HELPER FUNCTIONS *) + let set_global_svcomp_var is_double_free = + if is_double_free then + AnalysisState.svcomp_may_invalid_free := true + else + AnalysisState.svcomp_may_invalid_deref := true + let get_current_threadid ctx = ctx.ask Queries.CurrentThreadId let get_joined_threads ctx = ctx.ask Queries.MustJoinedThreads - let warn_for_multi_threaded_access ctx (heap_var:varinfo) behavior cwe_number = + let warn_for_multi_threaded_access ctx ?(is_double_free = false) (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 }) || G.is_empty freeing_threads then () @@ -59,23 +64,23 @@ struct | `Lifted current -> let possibly_started = G.exists (possibly_started current) freeing_threads in if possibly_started then begin - AnalysisState.svcomp_may_use_after_free := true; + set_global_svcomp_var is_double_free; 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 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 - AnalysisState.svcomp_may_use_after_free := true; + set_global_svcomp_var is_double_free; 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 end else if D.mem heap_var ctx.local then begin - AnalysisState.svcomp_may_use_after_free := true; + set_global_svcomp_var is_double_free; 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 end | `Top -> - AnalysisState.svcomp_may_use_after_free := true; + set_global_svcomp_var is_double_free; 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" @@ -104,7 +109,7 @@ struct | a when not (Queries.LS.is_top a) && not (Queries.LS.mem (dummyFunDec.svar, `NoOffset) a) -> let warn_for_heap_var var = if D.mem var state then begin - AnalysisState.svcomp_may_use_after_free := true; + set_global_svcomp_var is_double_free; 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 end in @@ -116,7 +121,7 @@ struct (* 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 ctx heap_var undefined_behavior cwe_number) pointed_to_heap_vars + List.iter (fun heap_var -> warn_for_multi_threaded_access ctx ~is_double_free heap_var undefined_behavior cwe_number) pointed_to_heap_vars | _ -> () end diff --git a/src/framework/analysisState.ml b/src/framework/analysisState.ml index e987c414f2..ca619d4dfb 100644 --- a/src/framework/analysisState.ml +++ b/src/framework/analysisState.ml @@ -7,8 +7,8 @@ let should_warn = ref false (** Whether signed overflow or underflow happened *) let svcomp_may_overflow = ref false -(** Whether a Use-After-Free (UAF) happened *) -let svcomp_may_use_after_free = ref false +(** Whether an invalid free happened *) +let svcomp_may_invalid_free = ref false (** Whether an invalid pointer dereference happened *) let svcomp_may_invalid_deref = ref false diff --git a/src/witness/witness.ml b/src/witness/witness.ml index 797541c606..8a77a10bc7 100644 --- a/src/witness/witness.ml +++ b/src/witness/witness.ml @@ -479,7 +479,7 @@ struct let next _ = [] end in - if not !AnalysisState.svcomp_may_use_after_free then + if not !AnalysisState.svcomp_may_invalid_free then let module TaskResult = struct module Arg = Arg From 034b0ab90198a60311485dc290b434386c41fd21 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sun, 27 Aug 2023 13:49:07 +0200 Subject: [PATCH 15/22] Use proper bug names when warning for multi-threaded programs --- src/analyses/useAfterFree.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index 6e2ca3b04f..b680bc5369 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -60,28 +60,29 @@ struct | `Top -> true | `Bot -> false in + let bug_name = if is_double_free then "Double Free" else "Use After Free" in match get_current_threadid ctx with | `Lifted current -> let possibly_started = G.exists (possibly_started current) freeing_threads in if possibly_started then begin set_global_svcomp_var is_double_free; - 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 + 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 set_global_svcomp_var is_double_free; - 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 + 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 D.mem heap_var ctx.local then begin set_global_svcomp_var is_double_free; - 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 + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "%s might occur in current unique thread %a for heap variable %a" bug_name ThreadIdDomain.FlagConfiguredTID.pretty current CilType.Varinfo.pretty heap_var end end | `Top -> set_global_svcomp_var is_double_free; - 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 + 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 From 68e1b7111bbf57a734a3ff9e1abce0e405e5f935 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sun, 27 Aug 2023 14:00:17 +0200 Subject: [PATCH 16/22] Add a valid-memsafety.prp file --- tests/sv-comp/valid-memsafety.prp | 4 ++++ 1 file changed, 4 insertions(+) create mode 100644 tests/sv-comp/valid-memsafety.prp diff --git a/tests/sv-comp/valid-memsafety.prp b/tests/sv-comp/valid-memsafety.prp new file mode 100644 index 0000000000..06a87f5a37 --- /dev/null +++ b/tests/sv-comp/valid-memsafety.prp @@ -0,0 +1,4 @@ +CHECK( init(main()), LTL(G valid-free) ) +CHECK( init(main()), LTL(G valid-deref) ) +CHECK( init(main()), LTL(G valid-memtrack) ) + From cd95e8d45dbcaf68adacd3508cc5938eec4d500c Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Mon, 28 Aug 2023 22:17:59 +0200 Subject: [PATCH 17/22] Try to not warn for threads joined before free() --- src/analyses/useAfterFree.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index b680bc5369..94d996249d 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -45,11 +45,11 @@ struct match tid with | `Lifted tid -> let created_threads = ctx.ask Queries.CreatedThreads in - (* Discard joined threads, as they're supposed to be joined before the point of freeing the memory *) - let threads = ConcDomain.MustThreadSet.diff created_threads joined_threads in - let not_started = MHP.definitely_not_started (current, threads) tid in + let not_started = MHP.definitely_not_started (current, created_threads) tid in let possibly_started = not not_started in - possibly_started + (* If [current] is possibly running together with [tid], but is also joined before the free() in [tid], then no need to WARN *) + let current_joined_before_free = ConcDomain.MustThreadSet.mem current joined_threads in + possibly_started && not current_joined_before_free | `Top -> true | `Bot -> false in From ba4d301aede5ad76f7175f00a4ca82c09adeddc4 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Mon, 28 Aug 2023 22:18:35 +0200 Subject: [PATCH 18/22] Enable threadJoins for all multi-threaded test cases --- tests/regression/74-use_after_free/12-multi-threaded-uaf.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/regression/74-use_after_free/12-multi-threaded-uaf.c b/tests/regression/74-use_after_free/12-multi-threaded-uaf.c index 0c647eff76..f6d11ae098 100644 --- a/tests/regression/74-use_after_free/12-multi-threaded-uaf.c +++ b/tests/regression/74-use_after_free/12-multi-threaded-uaf.c @@ -1,4 +1,4 @@ -//PARAM: --set ana.activated[+] useAfterFree +//PARAM: --set ana.activated[+] useAfterFree --set ana.activated[+] threadJoins #include #include #include From 66f0c9da414be2dc0d989a9dd22db35978bf00ef Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Mon, 28 Aug 2023 23:25:53 +0200 Subject: [PATCH 19/22] Add checks for implicit dereferencing of pointers --- src/analyses/useAfterFree.ml | 33 ++++++++++++++++++++------------- 1 file changed, 20 insertions(+), 13 deletions(-) diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index 94d996249d..e8a0d99925 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -87,10 +87,10 @@ struct 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) = - match is_double_free, lval with + let rec warn_lval_might_contain_freed ?(is_implicitly_derefed = false) ?(is_double_free = false) (transfer_fn_name:string) ctx (lval:lval) = + match is_implicitly_derefed, is_double_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, (Var _, NoOffset) -> () + | false, false, (Var _, NoOffset) -> () | _ -> let state = ctx.local in let undefined_behavior = if is_double_free then Undefined DoubleFree else Undefined UseAfterFree in @@ -126,7 +126,7 @@ struct | _ -> () end - and warn_exp_might_contain_freed ?(is_double_free = false) (transfer_fn_name:string) ctx (exp:exp) = + and warn_exp_might_contain_freed ?(is_implicitly_derefed = false) ?(is_double_free = false) (transfer_fn_name:string) ctx (exp:exp) = match exp with (* Base recursion cases *) | Const _ @@ -140,18 +140,18 @@ struct | SizeOfE e | AlignOfE e | UnOp (_, e, _) - | CastE (_, e) -> warn_exp_might_contain_freed ~is_double_free transfer_fn_name ctx e + | CastE (_, e) -> warn_exp_might_contain_freed ~is_implicitly_derefed ~is_double_free transfer_fn_name ctx e | BinOp (_, e1, e2, _) -> - 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_implicitly_derefed ~is_double_free transfer_fn_name ctx e1; + warn_exp_might_contain_freed ~is_implicitly_derefed ~is_double_free transfer_fn_name ctx e2 | Question (e1, e2, e3, _) -> - 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 + warn_exp_might_contain_freed ~is_implicitly_derefed ~is_double_free transfer_fn_name ctx e1; + warn_exp_might_contain_freed ~is_implicitly_derefed ~is_double_free transfer_fn_name ctx e2; + warn_exp_might_contain_freed ~is_implicitly_derefed ~is_double_free transfer_fn_name ctx e3 (* 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 ctx lval + | AddrOf lval -> warn_lval_might_contain_freed ~is_implicitly_derefed ~is_double_free transfer_fn_name ctx lval let side_effect_mem_free ctx freed_heap_vars threadid joined_threads = let side_effect_globals_to_heap_var heap_var = @@ -210,9 +210,16 @@ 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) ctx arg) arglist; let desc = LibraryFunctions.find f in + let is_arg_implicitly_derefed arg = + let read_shallow_args = LibraryDesc.Accesses.find desc.accs { kind = Read; deep = false } arglist in + let read_deep_args = LibraryDesc.Accesses.find desc.accs { kind = Read; deep = true } arglist in + let write_shallow_args = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = false } arglist in + let write_deep_args = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = true } arglist in + 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) ctx x) lval; + List.iter (fun arg -> warn_exp_might_contain_freed ~is_implicitly_derefed:(is_arg_implicitly_derefed arg) ~is_double_free:(f.vname = "free") ("special: " ^ f.vname) ctx arg) arglist; match desc.special arglist with | Free ptr -> begin match ctx.ask (Queries.MayPointTo ptr) with From 54646364ce12217a8e64c300a20548698c646aac Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Mon, 28 Aug 2023 23:26:14 +0200 Subject: [PATCH 20/22] Accommodate implicit dereferencing in regression tests --- tests/regression/74-use_after_free/06-uaf-struct.c | 9 +++++---- tests/regression/74-use_after_free/09-juliet-uaf.c | 5 +++-- tests/regression/74-use_after_free/11-wrapper-funs-uaf.c | 4 ++-- 3 files changed, 10 insertions(+), 8 deletions(-) diff --git a/tests/regression/74-use_after_free/06-uaf-struct.c b/tests/regression/74-use_after_free/06-uaf-struct.c index 13eed8e3db..fa3ffc7b56 100644 --- a/tests/regression/74-use_after_free/06-uaf-struct.c +++ b/tests/regression/74-use_after_free/06-uaf-struct.c @@ -17,15 +17,16 @@ int main(int argc, char **argv) { char line[128]; while (1) { - // No deref happening here => nothing to warn about - printf("[ auth = %p, service = %p ]\n", auth, service); //NOWARN + // printf() is considered an implicit deref => need to warn here + printf("[ auth = %p, service = %p ]\n", auth, service); //WARN if (fgets(line, sizeof(line), stdin) == NULL) break; if (strncmp(line, "auth ", 5) == 0) { - // No deref happening in either of the 2 lines below => no need to warn + // No deref happening in the line below => no need to warn auth = malloc(sizeof(auth)); //NOWARN - memset(auth, 0, sizeof(auth)); //NOWARN + // memset() is considered an implicit deref => need to warn + memset(auth, 0, sizeof(auth)); //WARN if (strlen(line + 5) < 31) { strcpy(auth->name, line + 5); //WARN } diff --git a/tests/regression/74-use_after_free/09-juliet-uaf.c b/tests/regression/74-use_after_free/09-juliet-uaf.c index c37ef26aca..e1a88508a6 100644 --- a/tests/regression/74-use_after_free/09-juliet-uaf.c +++ b/tests/regression/74-use_after_free/09-juliet-uaf.c @@ -68,9 +68,10 @@ void CWE416_Use_After_Free__return_freed_ptr_08_bad() if(staticReturnsTrue()) { { - // No need to warn in the two lines below, since there's no dereferencing of the freed memory + // No need to warn in the line below, since there's no dereferencing of the freed memory char * reversedString = helperBad("BadSink"); // NOWARN - printf("%s\n", reversedString); // NOWARN + // printf() is considered an implicit deref => need to warn here + printf("%s\n", reversedString); // WARN } } } diff --git a/tests/regression/74-use_after_free/11-wrapper-funs-uaf.c b/tests/regression/74-use_after_free/11-wrapper-funs-uaf.c index 6ae79e0062..cc6539eff2 100644 --- a/tests/regression/74-use_after_free/11-wrapper-funs-uaf.c +++ b/tests/regression/74-use_after_free/11-wrapper-funs-uaf.c @@ -27,8 +27,8 @@ int main(int argc, char const *argv[]) { my_free2(p); *(p + 42) = 'c'; //WARN - // No dereferencing in the line below => no need to warn - printf("%s", p); //NOWARN + // printf() is considered an implicit deref => need to warn + printf("%s", p); //WARN // No dereferencing happening in the lines below => no need to warn for an invalid-deref // Also no need to warn for an invalid-free, as the call to free is within these functions and they're not the "free" function itself From 049dc5853368f7b604aeb1a17aa449788d66ee72 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Mon, 28 Aug 2023 23:32:26 +0200 Subject: [PATCH 21/22] Remove redundant intersection when side-effecting --- src/analyses/useAfterFree.ml | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index e8a0d99925..9af1b8ca7a 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -156,11 +156,7 @@ struct let side_effect_mem_free ctx freed_heap_vars threadid joined_threads = let side_effect_globals_to_heap_var heap_var = let current_globals = ctx.global heap_var in - let joined_threads_to_add = match G.find_opt threadid current_globals with - | Some threads -> ConcDomain.ThreadSet.inter joined_threads threads - | None -> joined_threads - in - let globals_to_side_effect = G.add threadid joined_threads_to_add current_globals in + let globals_to_side_effect = G.add threadid joined_threads current_globals in ctx.sideg heap_var globals_to_side_effect in D.iter side_effect_globals_to_heap_var freed_heap_vars From 75f15808590ae9e595bc3857ac353cd0cf595a57 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Thu, 28 Sep 2023 11:54:22 +0200 Subject: [PATCH 22/22] Improve double free check --- 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 ba2c49f012..1b1e2f008d 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -216,7 +216,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) ctx x) lval; - List.iter (fun arg -> warn_exp_might_contain_freed ~is_implicitly_derefed:(is_arg_implicitly_derefed arg) ~is_double_free:(f.vname = "free") ("special: " ^ f.vname) ctx arg) arglist; + 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) ctx arg) arglist; match desc.special arglist with | Free ptr -> begin match ctx.ask (Queries.MayPointTo ptr) with