From b5881be306b5a0f3630cfb4ce024b7e91d65c0b6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 9 Jul 2021 15:49:53 +0200
Subject: [PATCH] [Eva] New general request about "red" and tainted properties.
---
Makefile | 7 +--
src/plugins/value/api/general_requests.ml | 77 +++++++++++++++++++++++
src/plugins/value/utils/red_statuses.ml | 18 ++++++
src/plugins/value/utils/red_statuses.mli | 3 +
4 files changed, 101 insertions(+), 4 deletions(-)
diff --git a/Makefile b/Makefile
index fb909f46afa..9f8f99e9b5e 100644
--- a/Makefile
+++ b/Makefile
@@ -904,11 +904,10 @@ PLUGIN_CMO:= partitioning/split_strategy domains/domain_mode value_parameters \
partitioning/partitioning_index partitioning/trace_partitioning \
engine/mem_exec engine/iterator engine/initialization \
engine/compute_functions engine/analysis register \
- api/general_requests \
- utils/unit_tests \
- api/values_request \
domains/taint_domain \
- $(APRON_CMO) $(NUMERORS_CMO)
+ $(APRON_CMO) $(NUMERORS_CMO) \
+ api/general_requests api/values_request \
+ utils/unit_tests
PLUGIN_CMI:= values/abstract_value values/abstract_location \
domains/abstract_domain domains/simpler_domains
PLUGIN_DEPENDENCIES:=Callgraph LoopAnalysis RteGen Server
diff --git a/src/plugins/value/api/general_requests.ml b/src/plugins/value/api/general_requests.ml
index 66c110104c2..95359daf0e6 100644
--- a/src/plugins/value/api/general_requests.ml
+++ b/src/plugins/value/api/general_requests.ml
@@ -119,4 +119,81 @@ let () = Request.register ~package
~output:(module DeadCode)
dead_code
+
+(* ----- Red and tainted alarms --------------------------------------------- *)
+
+
+module Taint = struct
+ open Server.Data
+ open Taint_domain
+
+ let dictionary = Enum.dictionary ()
+
+ let tag value name label descr =
+ Enum.tag ~name
+ ~label:(Markdown.plain label)
+ ~descr:(Markdown.plain descr) ~value dictionary
+
+ let tag_not_computed =
+ tag (Error NotComputed) "not_computed" ""
+ "The Eva taint analysis has not been computed"
+
+ let tag_error =
+ tag (Error LogicError) "error" "Error"
+ "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"
+
+ 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_not_tainted =
+ tag (Ok false) "not_tainted" "no"
+ "Untainted property: this property is safe, \
+ according to the Eva taint domain."
+
+ 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
+ end
+
+ let data = Request.dictionary ~package ~name:"taintStatus"
+ ~descr:(Markdown.plain "TODO") dictionary
+
+ include (val data : S with type t = (bool, taint_error) result)
+end
+
+
+let model = States.model ()
+
+let () = States.column model ~name:"priority"
+ ~descr:(Markdown.plain "Is the property invalid in some context \
+ of the analysis?")
+ ~data:(module Data.Jbool)
+ ~get:(fun ip -> Red_statuses.is_red ip)
+
+let () = States.column model ~name:"taint"
+ ~descr:(Markdown.plain "Is the property tainted according to \
+ the Eva taint domain?")
+ ~data:(module Taint)
+ ~get:(fun ip -> Taint_domain.is_tainted_property ip)
+
+let _array =
+ States.register_array
+ ~package
+ ~name:"properties"
+ ~descr:(Markdown.plain "Status of Registered Properties")
+ ~key:(fun ip -> Kernel_ast.Marker.create (PIP ip))
+ ~keyType:Kernel_ast.Marker.jproperty
+ ~iter:Property_status.iter
+ model
+
(**************************************************************************)
diff --git a/src/plugins/value/utils/red_statuses.ml b/src/plugins/value/utils/red_statuses.ml
index f57c4127228..42440721ae2 100644
--- a/src/plugins/value/utils/red_statuses.ml
+++ b/src/plugins/value/utils/red_statuses.ml
@@ -94,6 +94,24 @@ let add_red_property ki ip =
add_red_ap Kglobal (Prop ip')
| _ -> add_red_ap ki (Prop ip)
+let is_red ip =
+ let kinstr = Property.get_kinstr ip in
+ let ap =
+ match ip with
+ | Property.IPCodeAnnot ica ->
+ begin
+ match Alarms.find ica.ica_ca with
+ | Some a -> Alarm a
+ | None -> Prop ip
+ end
+ | _ -> Prop ip
+ in
+ try
+ let map = RedStatusesTable.find kinstr in
+ let callstacks = AlarmOrProp.Map.find ap map in
+ not (Callstacks.is_empty callstacks)
+ with Not_found -> false
+
let is_red_in_callstack kinstr ap callstack =
try
let map = RedStatusesTable.find kinstr in
diff --git a/src/plugins/value/utils/red_statuses.mli b/src/plugins/value/utils/red_statuses.mli
index b8443410be9..0a9f5f0f416 100644
--- a/src/plugins/value/utils/red_statuses.mli
+++ b/src/plugins/value/utils/red_statuses.mli
@@ -34,6 +34,9 @@ type alarm_or_property = Alarm of Alarms.t | Prop of Property.t
module AlarmOrProp : Datatype.S with type t := alarm_or_property
+(* Whether a red status has been emitted for a property in any callstack. *)
+val is_red: Property.t -> bool
+
(* Whether a red status has been emitted for an alarm or a property at the given
kinstr in the given callstack. *)
val is_red_in_callstack:
--
GitLab