Use-After-Free (UAF) Analysis First Iteration

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

src/analyses/libraryDesc.ml

@@ -46,6 +46,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

src/analyses/libraryFunctions.ml

@@ -34,6 +34,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("strncmp", special [__ "s1" [r]; __ "s2" [r]; __ "n" []] @@ fun s1 s2 n -> Strcmp { s1; s2; n = Some n; });
     ("malloc", special [__ "size" []] @@ fun size -> Malloc size);
     ("realloc", special [__ "ptr" [r; f]; __ "size" []] @@ fun ptr size -> Realloc { ptr; size });
+    ("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]]);
@@ -309,7 +310,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.

src/analyses/useAfterFree.ml

@@ -0,0 +1,156 @@
+(** An analysis for the detection of use-after-free vulnerabilities. *)
+
+open GoblintCil
+open Analyses
+open MessageCategory
+
+module ToppedVarInfoSet = SetDomain.ToppedSet(CilType.Varinfo)(struct let topname = "All Heap Variables" end)
+
+module Spec : Analyses.MCPSpec =
+struct
+  include Analyses.DefaultSpec
+
+  let name () = "useAfterFree"
+
+  module D = ToppedVarInfoSet
+  module C = Lattice.Unit
+
+  (** TODO: Try out later in benchmarks to see how we perform with and without context-sensititivty *)
+  let context _ _ = ()
+
+
+  (* 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 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 -> ()
+      | 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
+          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) =
+    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 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
+    | 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
+    (* 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
+
+
+  (* TRANSFER FUNCTIONS *)
+
+  let assign ctx (lval:lval) (rval:exp) : D.t =
+    warn_lval_might_contain_freed "assign" ctx lval;
+    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" 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" 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
+    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 (
+      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 = 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]
+    )
+
+  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 caller_state = ctx.local in
+    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 =
+    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
+    match desc.special arglist with
+    | 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 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
+
+  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)

src/util/messageCategory.ml

@@ -11,6 +11,7 @@ type undefined_behavior =
   | ArrayOutOfBounds of array_oob
   | NullPointerDereference
   | UseAfterFree
+  | DoubleFree
   | Uninitialized
   | DoubleLocking
   | Other
@@ -63,6 +64,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 double_locking: category = create @@ DoubleLocking
     let other: category = create @@ Other
@@ -99,6 +101,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
         | "double_locking" -> double_locking
         | "other" -> other
@@ -109,6 +112,7 @@ struct
       | ArrayOutOfBounds e -> "ArrayOutOfBounds" :: ArrayOutOfBounds.path_show e
       | NullPointerDereference -> ["NullPointerDereference"]
       | UseAfterFree -> ["UseAfterFree"]
+      | DoubleFree -> ["DoubleFree"]
       | Uninitialized -> ["Uninitialized"]
       | DoubleLocking -> ["DoubleLocking"]
       | Other -> ["Other"]
@@ -218,6 +222,7 @@ let behaviorName = function
   |Undefined u -> match u with
     |NullPointerDereference -> "NullPointerDereference"
     |UseAfterFree -> "UseAfterFree"
+    |DoubleFree -> "DoubleFree"
     |Uninitialized -> "Uninitialized"
     |DoubleLocking -> "DoubleLocking"
     |Other -> "Other"

src/util/sarifRules.ml

@@ -186,6 +186,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=""
   }
 ]
 

tests/regression/74-use_after_free/01-simple-uaf.c

@@ -0,0 +1,15 @@
+//PARAM: --set ana.activated[+] useAfterFree
+#include <stdlib.h>
+#include <stdio.h>
+
+int main() {
+    int *ptr = malloc(sizeof(int));
+    *ptr = 42;
+
+    free(ptr);
+
+    *ptr = 43; //WARN
+    free(ptr); //WARN
+
+    return 0;
+}

tests/regression/74-use_after_free/02-conditional-uaf.c

@@ -0,0 +1,19 @@
+//PARAM: --set ana.activated[+] useAfterFree
+#include <stdlib.h>
+#include <stdio.h>
+
+int main() {
+    int *ptr = malloc(sizeof(int));
+    *ptr = 42;
+
+    int input1;
+
+    if (input1) {
+        free(ptr);   
+    }
+
+    *ptr = 43; //WARN
+    free(ptr); //WARN
+
+    return 0;
+}

tests/regression/74-use_after_free/03-nested-ptr-uaf.c

@@ -0,0 +1,19 @@
+//PARAM: --set ana.activated[+] useAfterFree
+#include <stdlib.h>
+#include <stdio.h>
+
+int main() {
+    int *ptr = malloc(sizeof(int));
+    *ptr = 1;
+
+    free(ptr);
+
+    int a[2] = {0, 1};
+    a[*ptr] = 5; //WARN
+
+    if (a[*ptr] != 5) { //WARN
+        free(ptr); //WARN
+    }
+
+    return 0;
+}

tests/regression/74-use_after_free/04-function-call-uaf.c

@@ -0,0 +1,32 @@
+//PARAM: --set ana.activated[+] useAfterFree
+#include <stdlib.h>
+#include <stdio.h>
+
+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); //WARN
+
+    free(ptr3); //WARN
+
+    return 0;
+}
+
+void f(int *p1, int *p2, int *p3) {
+    *p1 = 5000; //WARN
+    free(p1); //WARN
+    free(p2); //WARN
+    free(p3);
+}

tests/regression/74-use_after_free/05-uaf-free-in-wrapper-fun.c

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