[Eva] Taint domain: changes the API to distinguish between data and control taint.

ivette/src/frama-c/api/generated/plugins/eva/general/index.ts

@@ -119,17 +119,23 @@ const getDeadCode_internal: Server.GetRequest<Json.key<'#fct'>,deadCode> = {
 /** Get the lists of unreachable and of non terminating statements in a function */
 export const getDeadCode: Server.GetRequest<Json.key<'#fct'>,deadCode>= getDeadCode_internal;
 
-/** TODO */
+/** Taint status of logical properties */
 export enum taintStatus {
-  /** The Eva taint analysis has not been computed */
+  /** **Not computed:**
+      the Eva taint domain has not been enabled, or the Eva analysis has not been run */
   not_computed = 'not_computed',
-  /** Error: the memory zone on which this property depends could not be computed */
+  /** **Error:**
+      the memory zone on which this property depends could not be computed */
   error = 'error',
-  /** No taint for this kind of property */
+  /** **Not applicable:** no taint for this kind of property */
   not_applicable = 'not_applicable',
-  /** Tainted property: this property is related to a memory zone that can be affected by an attacker, according to the Eva taint domain. */
-  tainted = 'tainted',
-  /** Untainted property: this property is safe, according to the Eva taint domain. */
+  /** **Data tainted:**
+      this property is related to a memory location that can be affected by an attacker */
+  data_tainted = 'data_tainted',
+  /** **Control tainted:**
+      this property is related to a memory location whose assignment depends on path conditions that can be affected by an attacker */
+  control_tainted = 'control_tainted',
+  /** **Untainted property:** this property is safe */
   not_tainted = 'not_tainted',
 }
 

ivette/src/frama-c/kernel/Properties.tsx

@@ -251,7 +251,8 @@ const renderTaint: Renderer<any> =
     let color = 'black';
     switch (taint.name) {
       case 'not_tainted': id = 'DROP.EMPTY'; color = '#00B900'; break;
-      case 'tainted': id = 'DROP.FILLED'; color = '#FF8300'; break;
+      case 'data_tainted': id = 'DROP.FILLED'; color = '#FF8300'; break;
+      case 'control_tainted': id = 'DROP.FILLED'; color = '#73BBBB'; break;
       case 'error': id = 'HELP'; break;
       default:
     }

src/plugins/value/api/general_requests.ml

@@ -129,46 +129,56 @@ module Taint = struct
 
   let dictionary = Enum.dictionary ()
 
-  let tag value name label descr =
+  let tag value name label short_descr long_descr =
     Enum.tag ~name
       ~label:(Markdown.plain label)
-      ~descr:(Markdown.plain descr) ~value dictionary
+      ~descr:(Markdown.bold (short_descr ^ ": ") @ Markdown.plain long_descr)
+      ~value dictionary
 
   let tag_not_computed =
     tag (Error NotComputed) "not_computed" ""
-      "The Eva taint analysis has not been computed"
+      "Not computed" "the Eva taint domain has not been enabled, \
+                      or the Eva analysis has not been run"
 
   let tag_error =
     tag (Error LogicError) "error" "Error"
-      "Error: the memory zone on which this property depends could not be computed"
+      "Error" "the memory zone on which this property depends \
+               could not be computed"
 
   let tag_not_applicable =
     tag (Error Irrelevant) "not_applicable" "—"
-      "No taint for this kind of property"
+      "Not applicable" "no taint for this kind of property"
 
-  let tag_tainted =
-    tag (Ok true) "tainted" "yes"
-      "Tainted property: this property is related to a memory zone that \
-       can be affected by an attacker, according to the Eva taint domain"
+  let tag_data_tainted =
+    tag (Ok Data) "data_tainted" "Tainted (data)"
+      "Data tainted"
+      "this property is related to a memory location that can be affected \
+       by an attacker"
 
-  let tag_not_tainted =
-    tag (Ok false) "not_tainted" "no"
-      "Untainted property: this property is safe, \
-       according to the Eva taint domain"
+  let tag_control_tainted =
+    tag (Ok Control) "control_tainted" "Tainted (control)"
+      "Control tainted"
+      "this property is related to a memory location whose assignment depends \
+       on path conditions that can be affected by an attacker"
+
+  let tag_untainted =
+    tag (Ok None) "not_tainted" "Untainted"
+      "Untainted property" "this property is safe"
 
   let () = Enum.set_lookup dictionary
       begin function
         | Error Taint_domain.NotComputed -> tag_not_computed
         | Error Taint_domain.Irrelevant -> tag_not_applicable
         | Error Taint_domain.LogicError -> tag_error
-        | Ok true -> tag_tainted
-        | Ok false -> tag_not_tainted
+        | Ok Data -> tag_data_tainted
+        | Ok Control -> tag_control_tainted
+        | Ok None -> tag_untainted
       end
 
   let data = Request.dictionary ~package ~name:"taintStatus"
       ~descr:(Markdown.plain "Taint status of logical properties") dictionary
 
-  include (val data : S with type t = (bool, taint_error) result)
+  include (val data : S with type t = taint_result)
 end
 
 

src/plugins/value/domains/taint_domain.ml

@@ -599,6 +599,8 @@ let () = Abstractions.register_hook interpret_taint_logic
 
 
 type taint_error = NotComputed | Irrelevant | LogicError
+type taint_ok = Data | Control | None
+type taint_result = (taint_ok, taint_error) result
 
 let zone_of_predicate env predicate =
   let logic_deps = Eval_terms.predicate_deps env predicate in
@@ -631,10 +633,13 @@ let is_tainted_property ip =
     let+ stmt = get_stmt ip in
     let+ predicate = get_predicate ip in
     match Store.get_stmt_state ~after:false stmt with
-    | `Bottom -> Ok false
+    | `Bottom -> Ok None
     | `Value state ->
       let cvalue = Db.Value.get_stmt_state ~after:false stmt in
       let env = Eval_terms.env_only_here cvalue in
       let+ zone = zone_of_predicate env predicate in
-      let tainted = Zone.intersects zone state.locs_data in
-      Ok tainted
+      if Zone.intersects zone state.locs_data
+      then Ok Data
+      else if Zone.intersects zone state.locs_control
+      then Ok Control
+      else Ok None

src/plugins/value/domains/taint_domain.mli

@@ -36,4 +36,17 @@ type taint_error =
   | LogicError  (** The memory zone on which the property depends could not
                     be computed. *)
 
-val is_tainted_property: Property.t -> (bool, taint_error) result
+type taint_ok =
+  | Data    (** Data-taint: there is a data dependency from the values provided
+                by the attacker to the given property, meaning that the attacker
+                may alter the values on which the property depends. *)
+  | Control (** Control-taint: there is a control-dependency from the values
+                provided by the attacker to the given property. The attacker
+                cannot directly alter the values on which the property depends,
+                but he may be able to choose the path where these values are
+                computed. *)
+  | None    (** No taint: the property cannot be altered by the attacker. *)
+
+type taint_result = (taint_ok, taint_error) result
+
+val is_tainted_property: Property.t -> taint_result