Memory Out-Of-Bounds Access Analysis

src/analyses/memOutOfBounds.ml

@@ -0,0 +1,187 @@
+open GoblintCil
+open Analyses
+open MessageCategory
+
+module AS = AnalysisState
+module VDQ = ValueDomainQueries
+
+module Spec =
+struct
+  include Analyses.IdentitySpec
+
+  module D = Lattice.Unit
+  module C = D
+
+  (* TODO: Check out later for benchmarking *)
+  let context _ _ = ()
+
+  let name () = "memOutOfBounds"
+
+  (* HELPER FUNCTIONS *)
+
+  let rec exp_contains_a_ptr (exp:exp) =
+    match exp with
+    | Const _
+    | SizeOf _
+    | SizeOfStr _
+    | AlignOf _
+    | AddrOfLabel _ -> false
+    | Real e
+    | Imag e
+    | SizeOfE e
+    | AlignOfE e
+    | UnOp (_, e, _)
+    | CastE (_, e) -> exp_contains_a_ptr e
+    | BinOp (_, e1, e2, _) ->
+      exp_contains_a_ptr e1 || exp_contains_a_ptr e2
+    | Question (e1, e2, e3, _) ->
+      exp_contains_a_ptr e1 || exp_contains_a_ptr e2 || exp_contains_a_ptr e3
+    | Lval lval
+    | AddrOf lval
+    | StartOf lval -> lval_contains_a_ptr lval
+
+  and lval_contains_a_ptr (lval:lval) =
+    let (host, offset) = lval in
+    let host_contains_a_ptr = function
+      | Var v -> isPointerType v.vtype
+      | Mem e -> exp_contains_a_ptr e
+    in
+    let rec offset_contains_a_ptr = function
+      | NoOffset -> false
+      | Index (e, o) -> exp_contains_a_ptr e || offset_contains_a_ptr o
+      | Field (f, o) -> isPointerType f.ftype || offset_contains_a_ptr o
+    in
+    host_contains_a_ptr host || offset_contains_a_ptr offset
+
+  let points_to_heap_only ctx ptr =
+    match ctx.ask (Queries.MayPointTo ptr) with
+    | a when not (Queries.LS.is_top a) && not (Queries.LS.mem (dummyFunDec.svar, `NoOffset) a) ->
+      Queries.LS.for_all (fun (v, _) -> ctx.ask (Queries.IsHeapVar v)) a
+    | _ -> false
+
+  let get_size_of_ptr_target ctx ptr =
+    (* Call Queries.BlobSize only if ptr points solely to the heap. Otherwise we get bot *)
+    if points_to_heap_only ctx ptr then
+      ctx.ask (Queries.BlobSize ptr)
+    else
+      match ctx.ask (Queries.MayPointTo ptr) with
+      | a when not (Queries.LS.is_top a) ->
+        let pts_list = Queries.LS.elements a in
+        let pts_elems_to_sizes (v, _) =
+          if isArrayType v.vtype then
+            ctx.ask (Queries.EvalLength ptr)
+          else
+            let var_type_size = match Cil.getInteger (sizeOf v.vtype) with
+              | Some z ->
+                let ikindOfTypeSize = intKindForValue z true in
+                VDQ.ID.of_int ikindOfTypeSize z
+              | None -> VDQ.ID.bot ()
+            in
+            var_type_size
+        in
+        (* Map each points-to-set element to its size *)
+        let pts_sizes = List.map pts_elems_to_sizes pts_list in
+        (* Take the smallest of all sizes that ptr's contents may have *)
+        begin match pts_sizes with
+          | [] -> VDQ.ID.bot ()
+          | [x] -> x
+          | x::xs -> List.fold_left (fun acc elem ->
+              if VDQ.ID.compare acc elem >= 0 then elem else acc
+            ) x xs
+        end
+      | _ ->
+        M.warn "Pointer %a has a points-to-set of top. An invalid memory access might occur" d_exp ptr;
+        VDQ.ID.top ()
+
+  let eval_ptr_offset_in_binop ctx exp =
+    ctx.ask (Queries.EvalInt exp)
+
+  let rec check_lval_for_oob_access ctx lval =
+    if not @@ lval_contains_a_ptr lval then ()
+    else
+      match lval with
+      | Var _, _ -> ()
+      | Mem e, _ -> check_exp_for_oob_access ctx e
+
+  and check_exp_for_oob_access ctx exp =
+    match exp with
+    | Const _
+    | SizeOf _
+    | SizeOfStr _
+    | AlignOf _
+    | AddrOfLabel _ -> ()
+    | Real e
+    | Imag e
+    | SizeOfE e
+    | AlignOfE e
+    | UnOp (_, e, _)
+    | CastE (_, e) -> check_exp_for_oob_access ctx e
+    | BinOp (bop, e1, e2, t) ->
+      check_binop_exp ctx bop e1 e2 t;
+      check_exp_for_oob_access ctx e1;
+      check_exp_for_oob_access ctx e2
+    | Question (e1, e2, e3, _) ->
+      check_exp_for_oob_access ctx e1;
+      check_exp_for_oob_access ctx e2;
+      check_exp_for_oob_access ctx e3
+    | Lval lval
+    | StartOf lval
+    | AddrOf lval -> check_lval_for_oob_access ctx lval
+
+  and check_binop_exp ctx binop e1 e2 t =
+    let binopexp = BinOp (binop, e1, e2, t) in
+    let behavior = Undefined MemoryOutOfBoundsAccess in
+    let cwe_number = 823 in
+    match binop with
+    | PlusPI
+    | IndexPI
+    | MinusPI ->
+      let ptr_size = get_size_of_ptr_target ctx e1 in
+      let offset_size = eval_ptr_offset_in_binop ctx e2 in
+      begin match VDQ.ID.is_top ptr_size, VDQ.ID.is_top offset_size with
+        | true, _ ->
+          AS.svcomp_may_invalid_deref := true;
+          M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Pointer (%a) size in expression %a not known. Memory out-of-bounds access might occur" d_exp e1 d_exp binopexp
+        | _, true ->
+          AS.svcomp_may_invalid_deref := true;
+          M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Operand value for pointer arithmetic in expression %a not known. Memory out-of-bounds access might occur" d_exp binopexp
+        | false, false ->
+          if ptr_size < offset_size then begin
+            AS.svcomp_may_invalid_deref := true;
+            M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Pointer size (%a) in expression %a is smaller than offset (%a) for pointer arithmetic. Memory out-of-bounds access must occur" VDQ.ID.pretty ptr_size d_exp binopexp VDQ.ID.pretty offset_size
+          end
+      end
+    | _ -> ()
+
+
+  (* TRANSFER FUNCTIONS *)
+
+  let assign ctx (lval:lval) (rval:exp) : D.t =
+    check_lval_for_oob_access ctx lval;
+    check_exp_for_oob_access ctx rval;
+    ctx.local
+
+  let branch ctx (exp:exp) (tv:bool) : D.t =
+    check_exp_for_oob_access ctx exp;
+    ctx.local
+
+  let return ctx (exp:exp option) (f:fundec) : D.t =
+    Option.iter (fun x -> check_exp_for_oob_access ctx x) exp;
+    ctx.local
+
+  let special ctx (lval:lval option) (f:varinfo) (arglist:exp list) : D.t =
+    Option.iter (fun x -> check_lval_for_oob_access ctx x) lval;
+    List.iter (fun arg -> check_exp_for_oob_access ctx arg) arglist;
+    ctx.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 -> check_lval_for_oob_access ctx x) lval;
+    List.iter (fun arg -> check_exp_for_oob_access ctx arg) args;
+    ctx.local
+
+  let startstate v = ()
+  let exitstate v = ()
+end
+
+let _ =
+  MCP.register_analysis (module Spec : MCPSpec)

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 an invalid pointer dereference happened *)
+let svcomp_may_invalid_deref = ref false
+
 (** A hack to see if we are currently doing global inits *)
 let global_initialization = ref false
 

src/util/messageCategory.ml

@@ -11,6 +11,7 @@ type undefined_behavior =
   | ArrayOutOfBounds of array_oob
   | NullPointerDereference
   | UseAfterFree
+  | MemoryOutOfBoundsAccess
   | DoubleFree
   | InvalidMemoryDeallocation
   | MemoryLeak
@@ -66,6 +67,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 memory_out_of_bounds_access: category = create @@ MemoryOutOfBoundsAccess
     let double_free: category = create @@ DoubleFree
     let invalid_memory_deallocation: category = create @@ InvalidMemoryDeallocation
     let memory_leak: category = create @@ MemoryLeak
@@ -105,6 +107,7 @@ struct
         | "array_out_of_bounds" -> ArrayOutOfBounds.from_string_list t
         | "nullpointer_dereference" -> nullpointer_dereference
         | "use_after_free" -> use_after_free
+        | "memory_out_of_bounds_access" -> memory_out_of_bounds_access
         | "double_free" -> double_free
         | "invalid_memory_deallocation" -> invalid_memory_deallocation
         | "uninitialized" -> uninitialized
@@ -117,6 +120,7 @@ struct
       | ArrayOutOfBounds e -> "ArrayOutOfBounds" :: ArrayOutOfBounds.path_show e
       | NullPointerDereference -> ["NullPointerDereference"]
       | UseAfterFree -> ["UseAfterFree"]
+      | MemoryOutOfBoundsAccess -> ["MemoryOutOfBoundsAccess"]
       | DoubleFree -> ["DoubleFree"]
       | InvalidMemoryDeallocation -> ["InvalidMemoryDeallocation"]
       | MemoryLeak -> ["MemoryLeak"]
@@ -229,6 +233,7 @@ let behaviorName = function
   |Undefined u -> match u with
     |NullPointerDereference -> "NullPointerDereference"
     |UseAfterFree -> "UseAfterFree"
+    |MemoryOutOfBoundsAccess -> "MemoryOutOfBoundsAccess"
     |DoubleFree -> "DoubleFree"
     |InvalidMemoryDeallocation -> "InvalidMemoryDeallocation"
     |MemoryLeak -> "MemoryLeak"

tests/regression/77-mem-oob/01-oob-heap-simple.c

@@ -0,0 +1,14 @@
+// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval
+#include <stdlib.h>
+
+int main(int argc, char const *argv[]) {
+    char *ptr = malloc(5 * sizeof(char));
+
+    *ptr = 'a';//NOWARN
+    *(ptr + 1) = 'b';//NOWARN
+    *(ptr + 10) = 'c';//WARN
+
+    free(ptr);
+
+    return 0;
+}

tests/regression/77-mem-oob/02-oob-stack-simple.c

@@ -0,0 +1,12 @@
+// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval
+#include <stdlib.h>
+
+int main(int argc, char const *argv[]) {
+    int i = 42;
+    int *ptr = &i;
+
+    *ptr = 5;//NOWARN
+    *(ptr + 10) = 55;//WARN
+
+    return 0;
+}

tests/regression/77-mem-oob/03-oob-loop.c

@@ -0,0 +1,18 @@
+// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval
+#include <stdlib.h>
+#include <stdio.h>
+
+int main(int argc, char const *argv[]) {
+    char *ptr = malloc(5 * sizeof(char));
+
+    for (int i = 0; i < 10; i++) {
+        ptr++;
+    }
+
+    //TODO: We cannot currently detect OOB memory accesses happening due to loops like the one above
+    // => Both lines below can't have WARNs for now
+    printf("%s", *ptr); //NOWARN
+    free(ptr); //NOWARN
+
+    return 0;
+}