From 7b0be2b44427d2f9c0c60eb09d06c68015a131db 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:33:56 +0200
Subject: [PATCH] [Eva] Registers new information about AST markers: taint
status.
---
src/plugins/eva/api/general_requests.ml | 56 +++++++++++++++++++++++++
1 file changed, 56 insertions(+)
diff --git a/src/plugins/eva/api/general_requests.ml b/src/plugins/eva/api/general_requests.ml
index 22f83de6bc4..856f90d4df8 100644
--- a/src/plugins/eva/api/general_requests.ml
+++ b/src/plugins/eva/api/general_requests.ml
@@ -188,6 +188,62 @@ let () =
~enable:Analysis.is_computed
print_value
+let print_taint fmt marker =
+ let loc = Cil_datatype.Location.unknown in
+ let expr, stmt =
+ match marker with
+ | Printer_tag.PLval (_kf, Kstmt stmt, lval) ->
+ Cil.new_exp ~loc (Lval lval), stmt
+ | Printer_tag.PExp (_kf, Kstmt stmt, expr) -> expr, stmt
+ | PVDecl (_kf, Kstmt stmt, vi) ->
+ Cil.new_exp ~loc (Lval (Var vi, NoOffset)), stmt
+ | PTermLval (_kf, Kstmt stmt, _ip, tlval) ->
+ begin
+ try
+ let result = None in
+ let lval = !Db.Properties.Interp.term_lval_to_lval ~result tlval in
+ Cil.new_exp ~loc (Lval lval), stmt
+ with Db.Properties.Interp.No_conversion -> raise Not_found
+ end
+ | _ -> raise Not_found
+ in
+ let evaluate_taint request =
+ let deps = Results.expr_dependencies expr request in
+ Result.get_ok (Results.is_tainted deps.data request),
+ Result.get_ok (Results.is_tainted deps.indirect request)
+ in
+ let before = evaluate_taint Results.(before stmt) in
+ let after = evaluate_taint Results.(after stmt) in
+ let str_taint = function
+ | Results.Untainted -> "untainted"
+ | Direct -> "direct taint"
+ | Indirect -> "indirect taint"
+ in
+ let pretty fmt = let open Results in function
+ | taint, Untainted -> Format.fprintf fmt "%s" (str_taint taint)
+ | t1, t2 ->
+ Format.fprintf fmt
+ "%s to the value, %s %s to values used to compute lvalues addresses"
+ (str_taint t1) (if t1 = Untainted then "but" else "and") (str_taint t2)
+ in
+ if before = after
+ then Format.fprintf fmt "%a" pretty before
+ else Format.fprintf fmt "Before: %a@\nAfter: %a" pretty before pretty after
+
+let () =
+ let enable () = Analysis.is_computed () && Taint_domain.Store.is_computed () in
+ let title =
+ "Taint status:\n\
+ - Direct taint: data dependency from values provided by the attacker, \
+ meaning that the attacker may be able to alter this value\n\
+ - Indirect taint: the attacker cannot directly alter this value, but he \
+ may be able to impact the path by which its value is computed.\n\
+ - Untainted: cannot be modified by the attacker."
+ in
+ Server.Kernel_ast.Information.register
+ ~id:"eva.taint" ~label:"Taint" ~descr: "Taint status according to Eva"
+ ~title ~enable print_taint
+
let () =
Analysis.register_computation_hook
(fun _ -> Server.Kernel_ast.Information.update ())
--
GitLab