[taintAnalysis] merge alarm types for patron

Author: spearo2

src/instance/taintAnalysis.ml

@@ -106,11 +106,35 @@ let inspect_aexp_bo node aexp itvmem mem queries =
           }
           :: queries)
         taint queries
+  | BufferOverrunLib ("fread", [ _; _; cnt ], loc) ->
+      let pid = InterCfg.Node.get_pid node in
+      let taint = TaintSem.eval pid cnt itvmem mem |> TaintDom.Val.user_input in
+      TaintDom.UserInput.fold
+        (fun (src_node, src_loc) queries ->
+          let desc =
+            "source = " ^ Node.to_string src_node ^ " @ "
+            ^ CilHelper.s_location src_loc
+          in
+          {
+            node;
+            exp = aexp;
+            loc;
+            allocsite = None;
+            status = UnProven;
+            desc;
+            src = Some (src_node, src_loc);
+          }
+          :: queries)
+        taint queries
   | _ -> queries
 
-let inspect_aexp_mul node aexp itvmem mem queries =
+let inspect_aexp_io node aexp itvmem mem queries =
   match aexp with
-  | MulExp (e, loc) ->
+  | PlusIOExp (e, loc)
+  | MinusIOExp (e, loc)
+  | MultIOExp (e, loc)
+  | ShiftIOExp (e, loc)
+  | CastIOExp (e, loc) ->
       let pid = InterCfg.Node.get_pid node in
       let tv = TaintSem.eval pid e itvmem mem in
       let int_overflow, taint =
@@ -164,6 +188,30 @@ let inspect_aexp_dz node aexp itvmem mem queries =
         taint queries
   | _ -> queries
 
+let inspect_aexp_nd node aexp itvmem mem queries =
+  match aexp with
+  | DerefExp (e, loc) ->
+      let pid = InterCfg.Node.get_pid node in
+      let taint = TaintSem.eval pid e itvmem mem |> TaintDom.Val.user_input in
+      TaintDom.UserInput.fold
+        (fun (src_node, src_loc) queries ->
+          let desc =
+            "source = " ^ Node.to_string src_node ^ " @ "
+            ^ CilHelper.s_location src_loc
+          in
+          {
+            node;
+            exp = aexp;
+            loc;
+            allocsite = None;
+            status = UnProven;
+            desc;
+            src = Some (src_node, src_loc);
+          }
+          :: queries)
+        taint queries
+  | _ -> queries
+
 let generate spec (global, mem, target) =
   let nodes = InterCfg.nodesof global.icfg in
   let total = List.length nodes in
@@ -181,9 +229,9 @@ let generate spec (global, mem, target) =
             else
               match target with
               | BO -> inspect_aexp_bo node aexp ptrmem mem
-              | IO -> inspect_aexp_mul node aexp ptrmem mem
+              | IO -> inspect_aexp_io node aexp ptrmem mem
               | DZ -> inspect_aexp_dz node aexp ptrmem mem
-              | ND -> Fun.id)
+              | ND -> inspect_aexp_nd node aexp ptrmem mem)
           aexps qs
       in
       (qs, k + 1))
@@ -192,7 +240,11 @@ let generate spec (global, mem, target) =
 
 let inspect_alarm global spec inputof =
   (if !Options.bo then generate spec (global, inputof, Report.BO) else [])
-  @ (if !Options.mul then generate spec (global, inputof, Report.IO) else [])
+  @ (if
+       !Options.mult_io || !Options.plus_io || !Options.minus_io
+       || !Options.shift_io || !Options.cast_io
+     then generate spec (global, inputof, Report.IO)
+     else [])
   @ (if !Options.nd then generate spec (global, inputof, Report.ND) else [])
   @ if !Options.dz then generate spec (global, inputof, Report.DZ) else []
 
@@ -260,6 +312,6 @@ let do_analysis (global, itvdug, itvinputof) =
   let _ = Options.pfs := 100 in
   let dug = Analysis.generate_dug spec global in
   (if !Options.marshal_in then marshal_in global
-  else Analysis.perform spec global dug)
+   else Analysis.perform spec global dug)
   |> opt !Options.marshal_out marshal_out
   |> post_process spec itvdug

src/report/alarmExp.ml

@@ -17,7 +17,11 @@ module F = Format
 type t =
   | ArrayExp of lval * exp * location
   | DerefExp of exp * location
-  | MulExp of exp * location
+  | PlusIOExp of exp * location
+  | MinusIOExp of exp * location
+  | MultIOExp of exp * location
+  | ShiftIOExp of exp * location
+  | CastIOExp of exp * location
   | DivExp of exp * location
   | Strcpy of exp * exp * location
   | Strcat of exp * exp * location
@@ -32,7 +36,13 @@ let to_string t =
   match t with
   | ArrayExp (lv, e, _) -> CilHelper.s_lv lv ^ "[" ^ CilHelper.s_exp e ^ "]"
   | DerefExp (e, _) -> "*(" ^ CilHelper.s_exp e ^ ")"
-  | MulExp (e, _) | DivExp (e, _) -> CilHelper.s_exp e
+  | DivExp (e, _)
+  | PlusIOExp (e, _)
+  | MinusIOExp (e, _)
+  | MultIOExp (e, _)
+  | ShiftIOExp (e, _)
+  | CastIOExp (e, _) ->
+      CilHelper.s_exp e
   | Strcpy (e1, e2, _) ->
       "strcpy (" ^ CilHelper.s_exp e1 ^ ", " ^ CilHelper.s_exp e2 ^ ")"
   | Strncpy (e1, e2, e3, _) ->
@@ -54,7 +64,11 @@ let to_string t =
 let location_of = function
   | ArrayExp (_, _, l)
   | DerefExp (_, l)
-  | MulExp (_, l)
+  | PlusIOExp (_, l)
+  | MinusIOExp (_, l)
+  | MultIOExp (_, l)
+  | ShiftIOExp (_, l)
+  | CastIOExp (_, l)
   | DivExp (_, l)
   | Strcpy (_, _, l)
   | Strncpy (_, _, _, l)
@@ -100,11 +114,18 @@ and c_exp e loc =
   | UnOp (_, e, _) -> c_exp e loc
   | BinOp (bop, e1, e2, _) -> (
       match bop with
-      | Mult when !Options.mul ->
-          (MulExp (e, loc) :: c_exp e1 loc) @ c_exp e2 loc
+      | PlusA when !Options.plus_io ->
+          (PlusIOExp (e, loc) :: c_exp e1 loc) @ c_exp e2 loc
+      | MinusA when !Options.minus_io ->
+          (MinusIOExp (e, loc) :: c_exp e1 loc) @ c_exp e2 loc
+      | Mult when !Options.mult_io ->
+          (MultIOExp (e, loc) :: c_exp e1 loc) @ c_exp e2 loc
+      | (Shiftlt | Shiftrt) when !Options.shift_io ->
+          (ShiftIOExp (e, loc) :: c_exp e1 loc) @ c_exp e2 loc
       | Div | Mod -> (DivExp (e, loc) :: c_exp e1 loc) @ c_exp e2 loc
       | _ -> c_exp e1 loc @ c_exp e2 loc)
-  | CastE (_, e) -> c_exp e loc
+  | CastE (_, e') when !Options.cast_io -> CastIOExp (e, loc) :: c_exp e' loc
+  | CastE (_, e') -> c_exp e' loc
   | AddrOf lv -> c_lv lv loc
   | StartOf lv -> c_lv lv loc
   | _ -> []
@@ -121,6 +142,7 @@ let query_lib =
     "memchr";
     "strncmp";
     "sprintf";
+    "fread";
   ]
 
 let c_lib f es loc =
@@ -139,6 +161,10 @@ let c_lib f es loc =
       BufferOverrunLib
         (f.vname, [ List.nth es 0; List.nth es 1; List.nth es 2 ], loc)
       :: c_exps es loc
+  | "fread" ->
+      BufferOverrunLib
+        (f.vname, [ List.nth es 0; List.nth es 1; List.nth es 2 ], loc)
+      :: c_exps es loc
   | _ -> []
 
 let c_lib_taint f es loc =
@@ -148,6 +174,11 @@ let c_lib_taint f es loc =
   | "calloc" | "g_malloc" | "g_malloc_n" | "g_malloc0" | "g_try_malloc"
   | "g_try_malloc_n" | "__builtin_alloca" ->
       [ AllocSize (f.vname, List.nth es 0, loc) ]
+  | "fread" ->
+      [
+        BufferOverrunLib
+          (f.vname, [ List.nth es 0; List.nth es 1; List.nth es 2 ], loc);
+      ]
   | "printf" -> [ Printf (f.vname, List.nth es 0, loc) ]
   | "fprintf" | "sprintf" | "vfprintf" | "vsprintf" | "vasprintf" | "__asprintf"
   | "asprintf" | "vdprintf" | "dprintf" | "easprintf" | "evasprintf" ->

src/report/alarmExp.mli

@@ -15,7 +15,11 @@ open ProsysCil
 type t =
   | ArrayExp of Cil.lval * Cil.exp * Cil.location
   | DerefExp of Cil.exp * Cil.location
-  | MulExp of Cil.exp * Cil.location
+  | PlusIOExp of Cil.exp * Cil.location
+  | MinusIOExp of Cil.exp * Cil.location
+  | MultIOExp of Cil.exp * Cil.location
+  | ShiftIOExp of Cil.exp * Cil.location
+  | CastIOExp of Cil.exp * Cil.location
   | DivExp of Cil.exp * Cil.location
   | Strcpy of Cil.exp * Cil.exp * Cil.location
   | Strcat of Cil.exp * Cil.exp * Cil.location
@@ -26,6 +30,8 @@ type t =
   | AllocSize of string * Cil.exp * Cil.location
   | Printf of string * Cil.exp * Cil.location
 
+val location_of : t -> Cil.location
+
 val collect : Spec.analysis -> IntraCfg.cmd -> t list
 
 val to_string : t -> string