From f03e7c2dbd3c7610c36312c75746042eadaf37bd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 29 Jul 2021 18:33:02 +0200
Subject: [PATCH] [Eva] Taint domain: changes the propagation of data-taint.
A memory location becomes data-tainted through an assignment if the location
assigned depends on data-tainted values.
---
src/plugins/value/domains/taint_domain.ml | 7 +++++--
tests/value/oracle/taint.res.oracle | 4 ++--
2 files changed, 7 insertions(+), 4 deletions(-)
diff --git a/src/plugins/value/domains/taint_domain.ml b/src/plugins/value/domains/taint_domain.ml
index adb32ee38ed..fb9f072b6f9 100644
--- a/src/plugins/value/domains/taint_domain.ml
+++ b/src/plugins/value/domains/taint_domain.ml
@@ -210,8 +210,11 @@ module TransferTaint = struct
let lv_zone, lv_indirect_zone, singleton = compute_zones lval to_loc in
let exp_zone = Value_util.zone_of_expr to_loc exp in
(* [lv] becomes data-tainted if a memory location on which the value of
- [exp] depends on is data-tainted. *)
- let data_tainted = Zone.intersects state.locs_data exp_zone in
+ [exp] or the location of [lval] depends on is data-tainted. *)
+ let data_tainted =
+ Zone.intersects state.locs_data exp_zone
+ || Zone.intersects state.locs_data lv_indirect_zone
+ in
(* [lv] becomes control-tainted if:
- the current call depends on a tainted assume statements of a caller;
- the execution of the assignment depends on a tainted assume statement;
diff --git a/tests/value/oracle/taint.res.oracle b/tests/value/oracle/taint.res.oracle
index 7f657cbe017..77cc014292c 100644
--- a/tests/value/oracle/taint.res.oracle
+++ b/tests/value/oracle/taint.res.oracle
@@ -12,7 +12,7 @@
Frama_C_dump_each:
# taint:
Locations (data):
- tainted; t; u; x
+ tainted; t; u; x; buf[0]
Locations (control):
w; buf[0]
==END OF DUMP==
@@ -142,7 +142,7 @@
Frama_C_dump_each:
# taint:
Locations (data):
- tainted; t; u; x; t
+ tainted; t; u; x; buf[0]; t
Locations (control):
t; u; w; x; y; buf[0..1]
==END OF DUMP==
--
GitLab