From abb37033fce269bf0fc857cf9333e7271f6e2cb9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 21 Sep 2022 14:24:33 +0200
Subject: [PATCH] [Eva] Results: exports new function to evaluate the taint of
a memory zone.
In the taint domain:
- exports generic function [is_tainted] evaluating the taint of a memory zone
in a given state. Removes function [is_tainted_property].
- returns Direct/Indirect/Untainted instead of Data/Control/None.
Implements [is_tainted_property] in the general request,
using [Results.is_tainted].
---
.../frama-c/plugins/eva/api/general/index.ts | 8 +--
src/plugins/eva/Eva.mli | 16 +++++
src/plugins/eva/api/general_requests.ml | 66 ++++++++++++++-----
src/plugins/eva/domains/taint_domain.ml | 63 +++++-------------
src/plugins/eva/domains/taint_domain.mli | 26 ++------
src/plugins/eva/utils/results.ml | 14 ++++
src/plugins/eva/utils/results.mli | 16 +++++
7 files changed, 119 insertions(+), 90 deletions(-)
diff --git a/ivette/src/frama-c/plugins/eva/api/general/index.ts b/ivette/src/frama-c/plugins/eva/api/general/index.ts
index 0cc4595adf3..cf5797288c8 100644
--- a/ivette/src/frama-c/plugins/eva/api/general/index.ts
+++ b/ivette/src/frama-c/plugins/eva/api/general/index.ts
@@ -247,12 +247,12 @@ export enum taintStatus {
error = 'error',
/** **Not applicable:** no taint for this kind of property */
not_applicable = 'not_applicable',
- /** **Data tainted:**
+ /** **Direct taint:**
this property is related to a memory location that can be affected by an attacker */
- data_tainted = 'data_tainted',
- /** **Control tainted:**
+ direct_taint = 'direct_taint',
+ /** **Indirect taint:**
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',
+ indirect_taint = 'indirect_taint',
/** **Untainted property:** this property is safe */
not_tainted = 'not_tainted',
}
diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index df135da7849..9a535134ce6 100644
--- a/src/plugins/eva/Eva.mli
+++ b/src/plugins/eva/Eva.mli
@@ -289,6 +289,22 @@ module Results: sig
(** Memory zone read to compute data addresses. *)
}
+ (** Taint of a memory zone, according to the taint domain. *)
+ type taint =
+ | Direct
+ (** Direct data dependency from values provided by the attacker to the given
+ memory zone, meaning that the attacker may be able to alter its value. *)
+ | Indirect
+ (** Indirect dependency from values provided by the attacker to the given
+ memory zone. The attacker cannot directly alter this memory, but he may
+ be able to impact on the path by which its value is computed. *)
+ | Untainted
+ (** No taint: the given memory zone cannot be modified by the attacker. *)
+
+ (** Evaluates the taint of a given memory zone, according to the taint domain.
+ Returns an error if the taint domain was not enabled. *)
+ val is_tainted : Locations.Zone.t -> request -> (taint, error) Result.t
+
(** Computes (an overapproximation of) the memory dependencies of an
expression. *)
val expr_dependencies : Cil_types.exp -> request -> deps
diff --git a/src/plugins/eva/api/general_requests.ml b/src/plugins/eva/api/general_requests.ml
index 691e7f73881..22f83de6bc4 100644
--- a/src/plugins/eva/api/general_requests.ml
+++ b/src/plugins/eva/api/general_requests.ml
@@ -196,7 +196,9 @@ let () =
module Taint = struct
open Server.Data
- open Taint_domain
+
+ type taint = Results.taint = Direct | Indirect | Untainted
+ type error = NotComputed | Irrelevant | LogicError
let dictionary = Enum.dictionary ()
@@ -220,39 +222,69 @@ module Taint = struct
tag (Error Irrelevant) "not_applicable" "—"
"Not applicable" "no taint for this kind of property"
- let tag_data_tainted =
- tag (Ok Data) "data_tainted" "Tainted (data)"
- "Data tainted"
+ let tag_direct_taint =
+ tag (Ok Direct) "direct_taint" "Tainted (direct)"
+ "Direct taint"
"this property is related to a memory location that can be affected \
by an attacker"
- let tag_control_tainted =
- tag (Ok Control) "control_tainted" "Tainted (control)"
- "Control tainted"
+ let tag_indirect_taint =
+ tag (Ok Indirect) "indirect_taint" "Tainted (indirect)"
+ "Indirect taint"
"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"
+ tag (Ok Untainted) "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 Data -> tag_data_tainted
- | Ok Control -> tag_control_tainted
- | Ok None -> tag_untainted
+ | Error NotComputed -> tag_not_computed
+ | Error Irrelevant -> tag_not_applicable
+ | Error LogicError -> tag_error
+ | Ok Direct -> tag_direct_taint
+ | Ok Indirect -> tag_indirect_taint
+ | Ok Untainted -> 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 = taint_result)
+ include (val data : S with type t = (taint, error) result)
+
+ let zone_of_predicate kinstr predicate =
+ let state = Results.(before_kinstr kinstr |> get_cvalue_model) in
+ let env = Eval_terms.env_only_here state in
+ let logic_deps = Eval_terms.predicate_deps env predicate in
+ match Option.map Cil_datatype.Logic_label.Map.bindings logic_deps with
+ | Some [ BuiltinLabel Here, zone ] -> Ok zone
+ | _ -> Error LogicError
+
+ let get_predicate = function
+ | Property.IPCodeAnnot ica ->
+ begin
+ match ica.ica_ca.annot_content with
+ | AAssert (_, predicate) | AInvariant (_, _, predicate) ->
+ Ok predicate.tp_statement
+ | _ -> Error Irrelevant
+ end
+ | IPPropertyInstance { ii_pred = None } -> Error LogicError
+ | IPPropertyInstance { ii_pred = Some ip } -> Ok ip.ip_content.tp_statement
+ | _ -> Error Irrelevant
+
+ let is_tainted_property ip =
+ if not (Analysis.is_computed () && Taint_domain.Store.is_computed ())
+ then Error NotComputed
+ else
+ let (let+) = Result.bind in
+ let kinstr = Property.get_kinstr ip in
+ let+ predicate = get_predicate ip in
+ let+ zone = zone_of_predicate kinstr predicate in
+ let result = Results.(before_kinstr kinstr |> is_tainted zone) in
+ Result.map_error (fun _ -> NotComputed) result
end
-
let model = States.model ()
let () = States.column model ~name:"priority"
@@ -265,7 +297,7 @@ 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)
+ ~get:(fun ip -> Taint.is_tainted_property ip)
let _array =
States.register_array
diff --git a/src/plugins/eva/domains/taint_domain.ml b/src/plugins/eva/domains/taint_domain.ml
index f32bc939b95..dc1f05c9ba4 100644
--- a/src/plugins/eva/domains/taint_domain.ml
+++ b/src/plugins/eva/domains/taint_domain.ml
@@ -24,7 +24,7 @@ open Cil_types
open Cil_datatype
open Locations
-type taint = {
+type taint_state = {
(* Over-approximation of the memory locations that are tainted due to a data
dependency. *)
locs_data: Zone.t;
@@ -73,7 +73,7 @@ module LatticeTaint = struct
include Datatype.Make_with_collections(struct
include Datatype.Serializable_undefined
- type t = taint
+ type t = taint_state
let name = "taint"
@@ -296,7 +296,7 @@ end
module TaintDomain = struct
- type state = taint
+ type state = taint_state
type value = Cvalue.V.t
type location = Precise_locs.precise_location
type origin
@@ -595,48 +595,15 @@ let flag =
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
- let deps_list = Option.map Logic_label.Map.bindings logic_deps in
- match deps_list with
- | Some [ BuiltinLabel Here, zone ] -> Ok zone
- | _ -> Error LogicError
-
-let get_predicate = function
- | Property.IPCodeAnnot ica ->
- begin
- match ica.ica_ca.annot_content with
- | AAssert (_, predicate) | AInvariant (_, _, predicate) ->
- Ok predicate.tp_statement
- | _ -> Error Irrelevant
- end
- | IPPropertyInstance { ii_pred = None } -> Error LogicError
- | IPPropertyInstance { ii_pred = Some pred } -> Ok pred.ip_content.tp_statement
- | _ -> Error Irrelevant
-
-let get_stmt ip =
- let kinstr = Property.get_kinstr ip in
- match kinstr with
- | Kglobal -> Error Irrelevant
- | Kstmt stmt -> Ok stmt
-
-let is_tainted_property ip =
- let (let+) = Result.bind in
- if not (Store.is_computed ()) then Error NotComputed else
- let+ stmt = get_stmt ip in
- let+ predicate = get_predicate ip in
- match Store.get_stmt_state ~after:false stmt with
- | `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
- if Zone.intersects zone state.locs_data
- then Ok Data
- else if Zone.intersects zone state.locs_control
- then Ok Control
- else Ok None
+type taint = Direct | Indirect | Untainted
+
+let is_tainted state ?indirect zone =
+ let intersects_any_taint z =
+ Zone.intersects (Zone.join state.locs_data state.locs_control) z
+ in
+ if Zone.intersects zone state.locs_data
+ then Direct
+ else if Zone.intersects zone state.locs_control
+ || Option.fold indirect ~none:false ~some:intersects_any_taint
+ then Indirect
+ else Untainted
diff --git a/src/plugins/eva/domains/taint_domain.mli b/src/plugins/eva/domains/taint_domain.mli
index 7d911a85ec3..263dcf4d714 100644
--- a/src/plugins/eva/domains/taint_domain.mli
+++ b/src/plugins/eva/domains/taint_domain.mli
@@ -28,25 +28,9 @@ include Abstract_domain.Leaf
val flag: Abstractions.flag
-type taint_error =
- | NotComputed (** The Eva analysis has not been run, or the taint domain
- was not enabled. *)
- | Irrelevant (** Properties other than assertions, invariants and
- preconditions are irrelevant here. *)
- | LogicError (** The memory zone on which the property depends could not
- be computed. *)
+type taint = | Direct | Indirect | Untainted
-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
+(** Is a memory zone tainted according to a given state?Â
+ If [indirect] is provided, return an [Indirect] taint if [indirect] is
+ tainted (either directly or indirectly). *)
+val is_tainted: state -> ?indirect:Locations.Zone.t -> Locations.Zone.t -> taint
diff --git a/src/plugins/eva/utils/results.ml b/src/plugins/eva/utils/results.ml
index c7b44e783a1..d57d536e50b 100644
--- a/src/plugins/eva/utils/results.ml
+++ b/src/plugins/eva/utils/results.ml
@@ -320,6 +320,11 @@ struct
| Some extract ->
convert (Response.map_join extract Cvalue.Model.join (get req))
+ let get_state req key join =
+ match A.Dom.get key with
+ | None -> Result.error DisabledDomain
+ | Some extract -> convert (Response.map_join extract join (get req))
+
let print_states ?filter req =
let state = Response.map_join (fun x -> x) A.Dom.join (get req) in
let print (type s)
@@ -738,6 +743,15 @@ let expr_dependencies expr request =
let lval_to_loc lv = eval_address lv request |> as_precise_loc in
Eva_utils.deps_of_expr lval_to_loc expr
+(* Taint *)
+
+type taint = Taint_domain.taint = Direct | Indirect | Untainted
+
+let is_tainted zone request =
+ let module M = Make () in
+ let state = M.get_state request Taint_domain.key Taint_domain.join in
+ Result.map (fun state -> Taint_domain.is_tainted state zone) state
+
(* Reachability *)
let is_empty rq =
diff --git a/src/plugins/eva/utils/results.mli b/src/plugins/eva/utils/results.mli
index ec7bc51d785..d221fe82aa3 100644
--- a/src/plugins/eva/utils/results.mli
+++ b/src/plugins/eva/utils/results.mli
@@ -194,6 +194,22 @@ type deps = Function_Froms.Deps.deps = {
(** Memory zone read to compute data addresses. *)
}
+(** Taint of a memory zone, according to the taint domain. *)
+type taint =
+ | Direct
+ (** Direct data dependency from values provided by the attacker to the given
+ memory zone, meaning that the attacker may be able to alter its value. *)
+ | Indirect
+ (** Indirect dependency from values provided by the attacker to the given
+ memory zone. The attacker cannot directly alter this memory, but he may
+ be able to impact on the path by which its value is computed. *)
+ | Untainted
+ (** No taint: the given memory zone cannot be modified by the attacker. *)
+
+(** Evaluates the taint of a given memory zone, according to the taint domain.
+ Returns an error if the taint domain was not enabled. *)
+val is_tainted : Locations.Zone.t -> request -> (taint, error) Result.t
+
(** Computes (an overapproximation of) the memory dependencies of an
expression. *)
val expr_dependencies : Cil_types.exp -> request -> deps
--
GitLab