Type inference

.gitignore

@@ -204,16 +204,20 @@ dmypy.json
 pyvenv.cfg
 pip-selfcheck.json
 
+# End of https://www.gitignore.io/api/c,ocaml,python
+
 # dont upload our real life zoo
 test/real_world_samples
 test/run_real_world_samples.sh
 
-# End of https://www.gitignore.io/api/c,ocaml,python
-
 .project
 .pydevproject
 
-src/cwe_checker.plugin
+# Plugin files (generated by bapbuild)
+*.plugin
+
+# install files for opam packages (generated by dune)
+*.install
 
 test/artificial_samples/dockcross*
 

CHANGES.md

@@ -9,6 +9,8 @@
 -   Added BAP recipe for standard cwe_checker run (PR #9)
 -   Improved check for CWE-476 (NULL Pointer Dereference) using data flow analysis (PR #11)
 -   Switched C build system from make to scons (PR #16)
+-   Added type inference pass (PR #14)
+-   Added unit tests to test suite (PR #14)
 
 0.1 (2018-10-08)
 =====

Makefile

@@ -1,12 +1,25 @@
 .PHONY: all clean test uninstall
 all:
-	cd src; bapbuild -r -Is checkers,utils -pkgs yojson,unix cwe_checker.plugin; bapbundle install cwe_checker.plugin; cd ..
+	dune build --profile release
+	dune install
+	cd plugins/cwe_checker; make all; cd ../..
+	cd plugins/cwe_checker_type_inference; make all; cd ../..
+	cd plugins/cwe_checker_type_inference_print; make all; cd ../..
 
 test:
+	dune runtest --profile release # TODO: correct all dune linter warnings so that we can remove --profile release
 	pytest -v
 
 clean:
+	dune clean
 	bapbuild -clean
+	cd test/unit; make clean; cd ../..
+	cd plugins/cwe_checker; make clean; cd ../..
+	cd plugins/cwe_checker_type_inference; make clean; cd ../..
+	cd plugins/cwe_checker_type_inference_print; make clean; cd ../..
 
 uninstall:
-	bapbundle remove cwe_checker.plugin
+	dune uninstall
+	cd plugins/cwe_checker; make uninstall; cd ../..
+	cd plugins/cwe_checker_type_inference; make uninstall; cd ../..
+	cd plugins/cwe_checker_type_inference_print; make uninstall; cd ../..

dune-project

@@ -0,0 +1,2 @@
+(lang dune 1.6)
+(name cwe_checker)

plugins/cwe_checker/Makefile

@@ -0,0 +1,9 @@
+all:
+	bapbuild -pkgs yojson,unix,ppx_jane,cwe_checker_core cwe_checker.plugin
+	bapbundle install cwe_checker.plugin
+
+clean:
+	bapbuild -clean
+
+uninstall:
+	bapbundle remove cwe_checker.plugin

src/cwe_checker.ml → plugins/cwe_checker/cwe_checker.ml

@@ -1,8 +1,9 @@
-open Core_kernel.Std
+open Core_kernel
 open Bap.Std
 open Graphlib.Std
 open Format
 open Yojson.Basic.Util
+open Cwe_checker_core
 
 include Self()
 

plugins/cwe_checker_type_inference/Makefile

@@ -0,0 +1,9 @@
+all:
+	bapbuild -pkgs yojson,unix,ppx_jane,cwe_checker_core cwe_checker_type_inference.plugin
+	bapbundle install cwe_checker_type_inference.plugin
+
+clean:
+	bapbuild -clean
+
+uninstall:
+	bapbundle remove cwe_checker_type_inference.plugin

plugins/cwe_checker_type_inference/cwe_checker_type_inference.ml

@@ -0,0 +1,5 @@
+open Bap.Std
+open Core_kernel
+open Cwe_checker_core
+
+let () = Project.register_pass Type_inference.compute_pointer_register

plugins/cwe_checker_type_inference_print/Makefile

@@ -0,0 +1,9 @@
+all:
+	bapbuild -pkgs yojson,unix,ppx_jane,cwe_checker_core cwe_checker_type_inference_print.plugin
+	bapbundle install cwe_checker_type_inference_print.plugin
+
+clean:
+	bapbuild -clean
+
+uninstall:
+	bapbundle remove cwe_checker_type_inference_print.plugin

plugins/cwe_checker_type_inference_print/cwe_checker_type_inference_print.ml

@@ -0,0 +1,14 @@
+open Bap.Std
+open Core_kernel
+open Cwe_checker_core
+
+let main project =
+  Log_utils.set_log_level Log_utils.DEBUG;
+  Log_utils.set_output stdout;
+  Log_utils.color_on ();
+
+  let program = Project.program project in
+  let tid_map = Address_translation.generate_tid_map program in
+  Type_inference.print_type_info_tags project tid_map
+
+let () = Project.register_pass' main ~deps:["cwe-checker-type-inference"]

recipes/type_inference/descr

@@ -0,0 +1 @@
+Prints the results of the type inference pass of each block.

recipes/type_inference/recipe.scm

@@ -0,0 +1 @@
+(option pass cwe-type-inference-print)

src/analysis/mem_region.ml

@@ -0,0 +1,164 @@
+open Bap.Std
+open Core_kernel
+
+
+let (+), (-) = Bitvector.(+), Bitvector.(-)
+
+let (>) x y = Bitvector.(>) (Bitvector.signed x) (Bitvector.signed y)
+let (<) x y = Bitvector.(<) (Bitvector.signed x) (Bitvector.signed y)
+let (>=) x y = Bitvector.(>=) (Bitvector.signed x) (Bitvector.signed y)
+let (<=) x y = Bitvector.(<=) (Bitvector.signed x) (Bitvector.signed y)
+let (=) x y = Bitvector.(=) x y
+
+type 'a mem_node = {
+  pos: Bitvector.t; (* address of the element *)
+  size: Bitvector.t; (* size (in bytes) of the element *)
+  data: ('a, unit) Result.t;
+} [@@deriving bin_io, compare, sexp]
+
+type 'a t = 'a mem_node list [@@deriving bin_io, compare, sexp]
+
+
+let empty () : 'a t =
+  []
+
+(** Return an error mem_node at the given position with the given size. *)
+let error_elem ~pos ~size =
+  { pos = pos;
+    size = size;
+    data = Error ();}
+
+
+let rec add mem_region elem ~pos ~size =
+  let () = if pos + size < pos then failwith "[CWE-checker] element out of bounds for mem_region" in
+  let new_node = {
+    pos=pos;
+    size=size;
+    data=Ok(elem);
+  } in
+  match mem_region with
+  | [] -> new_node :: []
+  | head :: tail ->
+    if head.pos + head.size <= pos then
+      head :: (add tail elem ~pos ~size)
+    else if pos + size <= head.pos then
+      new_node :: mem_region
+    else begin (* head and new node intersect => at the intersection, head gets overwritten and the rest of head gets marked as error. *)
+      let tail = if head.pos + head.size > pos + size then (* mark the right end of head as error *)
+          let err = error_elem ~pos:(pos + size) ~size:(head.pos + head.size - (pos + size)) in
+          err :: tail
+        else
+          tail in
+      let tail = add tail elem ~pos ~size in (* add the new element*)
+      let tail = if head.pos < pos then (* mark the left end of head as error *)
+          let err = error_elem ~pos:(head.pos) ~size:(pos - head.pos) in
+          err :: tail
+        else
+          tail in
+      tail
+    end
+
+
+let rec get mem_region pos =
+  match mem_region with
+  | [] -> None
+  | head :: tail ->
+    if head.pos > pos then
+      None
+    else if head.pos = pos then
+      match head.data with
+      | Ok(x) -> Some(Ok(x, head.size))
+      | Error(_) -> Some(Error(()))
+    else if head.pos + head.size <= pos then
+      get tail pos
+    else
+      Some(Error(())) (* pos intersects some data, but does not equal its starting address*)
+
+(* Helper function. Removes all elements with position <= pos. *)
+let rec remove_until mem_region pos =
+  match mem_region with
+  | [] -> []
+  | hd :: tl ->
+    if hd.pos <= pos then
+      remove_until tl pos
+    else
+      mem_region
+
+
+let rec remove mem_region ~pos ~size =
+  let () = if pos + size < pos then failwith "[CWE-checker] element out of bounds for mem_region" in
+  match mem_region with
+  | [] -> []
+  | hd :: tl ->
+    if hd.pos + hd.size <= pos then
+      hd :: remove tl pos size
+    else if pos + size <= hd.pos then
+      mem_region
+    else
+      let mem_region = remove tl pos size in
+      let mem_region =
+        if hd.pos + hd.size > pos + size then
+          error_elem ~pos:(pos + size) ~size:(hd.pos + hd.size - (pos + size)) :: mem_region
+        else
+          mem_region in
+      let mem_region =
+        if hd.pos < pos then
+          error_elem ~pos:hd.pos ~size:(pos - hd.pos) :: mem_region
+        else
+          mem_region in
+      mem_region
+
+let rec mark_error mem_region ~pos ~size =
+  let () = if pos + size < pos then failwith "[CWE-checker] element out of bounds for mem_region" in
+  match mem_region with
+  | [] -> (error_elem pos size) :: []
+  | hd :: tl ->
+    if hd.pos + hd.size <= pos then
+      hd :: (mark_error tl pos size)
+    else if pos + size <= hd.pos then
+      (error_elem pos size) :: mem_region
+    else
+      let start_pos = min pos hd.pos in
+      let end_pos_plus_one = max (pos + size) (hd.pos + hd.size) in
+      mark_error tl ~pos:start_pos ~size:(end_pos_plus_one - start_pos)
+
+
+(* TODO: This is probably a very inefficient implementation in some cases. Write a faster implementation if necessary. *)
+let rec merge mem_region1 mem_region2 ~data_merge =
+  match (mem_region1, mem_region2) with
+  | (value, [])
+  | ([], value) -> value
+  | (hd1 :: tl1, hd2 :: tl2) ->
+    if hd1.pos + hd1.size <= hd2.pos then
+      hd1 :: merge tl1 mem_region2 data_merge
+    else if hd2.pos + hd2.size <= hd1.pos then
+      hd2 :: merge mem_region1 tl2 data_merge
+    else if hd1.pos = hd2.pos && hd1.size = hd2.size then
+      match (hd1.data, hd2.data) with
+      | (Ok(data1), Ok(data2)) -> begin
+          match data_merge data1 data2 with
+          | Some(Ok(value)) -> { hd1 with data = Ok(value) } :: merge tl1 tl2 ~data_merge
+          | Some(Error(_)) -> {hd1 with data = Error(())} :: merge tl1 tl2 ~data_merge
+          | None -> merge tl1 tl2 data_merge
+        end
+      | _ -> { hd1 with data = Error(()) } :: merge tl1 tl2 ~data_merge
+    else
+      let start_pos = min hd1.pos hd2.pos in
+      let end_pos_plus_one = max (hd1.pos + hd1.size) (hd2.pos + hd2.size) in
+      let mem_region = merge tl1 tl2 data_merge in
+      mark_error mem_region ~pos:start_pos ~size:(end_pos_plus_one - start_pos)
+
+
+let rec equal (mem_region1:'a t) (mem_region2:'a t) ~data_equal : bool =
+  match (mem_region1, mem_region2) with
+  | ([], []) -> true
+  | (hd1 :: tl1, hd2 :: tl2) ->
+    if hd1.pos = hd2.pos && hd1.size = hd2.size then
+      match (hd1.data, hd2.data) with
+      | (Ok(data1), Ok(data2)) when data_equal data1 data2 ->
+        equal tl1 tl2 data_equal
+      | (Error(()), Error(())) -> equal tl1 tl2 data_equal
+      | _ -> false
+    else
+      false
+  | _ -> false

src/analysis/mem_region.mli

@@ -0,0 +1,39 @@
+(** contains an abstract memory region data type where you can assign arbitrary data to locations
+    inside the memory regions. A memory region has no fixed size, so it can be used
+    for memory regions of variable size like arrays or stacks.
+
+    TODO: Right now this data structure is unsuited for elements that get only partially loaded. *)
+
+open Bap.Std
+open Core_kernel
+
+type 'a t [@@deriving bin_io, compare, sexp]
+
+
+(** Get an empty memory region- *)
+val empty: unit -> 'a t
+
+
+(** Add an element to the memory region. If the element intersects existing elements,
+    the non-overwritten part gets marked as Error *)
+val add: 'a t -> 'a -> pos:Bitvector.t -> size:Bitvector.t -> 'a t
+
+(** Mark the memory region between pos (included) and pos+size (excluded) as empty.
+    If elements get partially removed, mark the non-removed parts as Error *)
+val remove: 'a t -> pos:Bitvector.t -> size:Bitvector.t -> 'a t
+
+(** Returns the element and its size at position pos or None, when there is no element at that position.
+    If pos intersects an element but does not match its starting position, it returns Some(Error(())). *)
+val get: 'a t -> Bitvector.t -> (('a * Bitvector.t), unit) Result.t Option.t
+
+(** Merge two memory regions. Elements with the same position and size get merged using
+    data_merge, other intersecting elements get marked as Error. Note that data_merge
+    may return None (to remove the elements from the memory region) or Some(Error(_)) to
+    mark the merged element as error. *)
+val merge: 'a t -> 'a t -> data_merge:('a -> 'a -> ('a, 'b) result option) -> 'a t
+
+(** Check whether two memory regions are equal. *)
+val equal: 'a t -> 'a t -> data_equal:('a -> 'a -> bool) -> bool
+
+(** Mark an area in the mem_region as containing errors. *)
+val mark_error: 'a t -> pos:Bitvector.t -> size:Bitvector.t -> 'a t