Merge pull request #1864 from goblint/uaf-event

Use access events in useAfterFree analysis

Author: sim642

src/analyses/accessAnalysis.ml

@@ -29,7 +29,7 @@ struct
   let init _ =
     collect_local := get_bool "witness.yaml.enabled" && get_bool "witness.invariant.accessed";
     let activated = get_string_list "ana.activated" in
-    emit_single_threaded := List.mem (ModifiedSinceSetjmp.Spec.name ()) activated || List.mem (PoisonVariables.Spec.name ()) activated
+    emit_single_threaded := List.mem (ModifiedSinceSetjmp.Spec.name ()) activated || List.mem (PoisonVariables.Spec.name ()) activated || List.mem (UseAfterFree.Spec.name ()) activated (* TODO: some of these don't have access as dependency *)
 
   let do_access (man: (D.t, G.t, C.t, V.t) man) (kind:AccessKind.t) (reach:bool) (e:exp) =
     if M.tracing then M.trace "access" "do_access %a %a %B" d_exp e AccessKind.pretty kind reach;

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,102 +58,33 @@ 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
-    (* 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
-      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
-          (* 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
-
-  and warn_exp_might_contain_freed ?(is_implicitly_derefed = false) ?(is_double_free = false) (transfer_fn_name:string) man (exp:exp) =
-    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_implicitly_derefed ~is_double_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
-    | 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
-    (* 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
-
   let side_effect_mem_free man freed_heap_vars threadid joined_threads =
     let side_effect_globals_to_heap_var heap_var =
       let current_globals = man.global heap_var in
@@ -165,22 +96,8 @@ struct
 
   (* TRANSFER FUNCTIONS *)
 
-  let assign man (lval:lval) (rval:exp) : D.t =
-    warn_lval_might_contain_freed "assign" man lval;
-    warn_exp_might_contain_freed "assign" man rval;
-    man.local
-
-  let branch man (exp:exp) (tv:bool) : D.t =
-    warn_exp_might_contain_freed "branch" man exp;
-    man.local
-
-  let return man (exp:exp option) (f:fundec) : D.t =
-    Option.iter (fun x -> warn_exp_might_contain_freed "return" man x) exp;
-    man.local
-
   let enter man (lval:lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
     let caller_state = man.local in
-    List.iter (fun arg -> warn_exp_might_contain_freed "enter" man arg) args;
     (* TODO: The 2nd component of the callee state needs to contain only the heap vars from the caller state which are reachable from: *)
     (* * Global program variables *)
     (* * The callee arguments *)
@@ -195,24 +112,12 @@ struct
     let callee_combined_state = HeapVars.join callee_stack_state callee_heap_state in
     (caller_stack_state, HeapVars.join caller_heap_state callee_combined_state)
 
-  let combine_assign man (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" man x) lval;
-    man.local
-
   let special man (lval:lval option) (f:varinfo) (arglist:exp list) : D.t =
     let state = man.local in
     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) 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;
     match desc.special arglist with
     | Free ptr ->
+      (* TODO: do this using Free Access events? *)
       begin match man.ask (Queries.MayPointTo ptr) with
         | ad when not (Queries.AD.is_top ad) ->
           let pointed_to_heap_vars =
@@ -239,7 +144,37 @@ struct
   let startstate v = D.bot ()
   let exitstate v = D.top ()
 
+  let event man e oman =
+    match e with
+    | Events.Access {exp; ad; kind; reach} ->
+      (* must use original (pre-assign, etc) man queries *)
+      let is_free = kind = Free in
+      let freed_heap_vars = snd oman.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 warn_for_heap_var v =
+        if HeapVars.mem v freed_heap_vars then begin
+          set_mem_safety_flag InvalidDeref;
+          M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "lval (%s) points to a maybe freed memory region" v.vname
+        end
+      in
+      if not (Queries.AD.is_top ad) then begin
+        let pointed_to_heap_vars =
+          Queries.AD.fold (fun addr vars ->
+              match addr with
+              | Queries.AD.Addr.Addr (v,_) when oman.ask (Queries.IsAllocVar v) -> v :: vars
+              | _ -> vars
+            ) ad []
+        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 oman ~is_free heap_var undefined_behavior cwe_number) pointed_to_heap_vars
+      end;
+      man.local
+    | _ ->
+      man.local
 end
 
 let _ =
-  MCP.register_analysis (module Spec : MCPSpec)
+  MCP.register_analysis ~dep:["access"] (module Spec : MCPSpec)

tests/regression/74-invalid_deref/18-simple-uaf.t

@@ -0,0 +1,7 @@
+  $ goblint --set ana.activated[+] useAfterFree 18-simple-uaf.c 2>&1 | sed -r 's/sid:[0-9]+/sid:$SID/'
+  [Warning][Behavior > Undefined > UseAfterFree][CWE-416] lval ((alloc@sid:$SID@tid:[main])) points to a maybe freed memory region (18-simple-uaf.c:11:5-11:14)
+  [Warning][Behavior > Undefined > DoubleFree][CWE-415] lval ((alloc@sid:$SID@tid:[main])) points to a maybe freed memory region (18-simple-uaf.c:12:5-12:14)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 7
+    dead: 0
+    total lines: 7

tests/regression/75-invalid_free/14-double-free-deref.c

@@ -0,0 +1,21 @@
+//PARAM: --set ana.activated[+] useAfterFree
+#include <stdlib.h>
+
+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;
+}

tests/regression/75-invalid_free/15-use-after-free-indirect.c

@@ -0,0 +1,24 @@
+//PARAM: --set ana.activated[+] useAfterFree
+#include <stdlib.h>
+
+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;
+}

tests/regression/75-invalid_free/16-use-after-free-double-indirect.c

@@ -0,0 +1,28 @@
+//PARAM: --set ana.activated[+] useAfterFree
+#include <stdlib.h>
+
+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;
+}