From c0d05ec0f3772d70a02d82fb55e6cf7a84f81c0a Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Fri, 7 Oct 2022 21:22:24 +0200
Subject: [PATCH] [Dive] add taint information
---
ivette/src/frama-c/plugins/dive/api/index.ts | 11 +++++--
ivette/src/frama-c/plugins/dive/style.json | 33 +++++++++++++++++---
src/plugins/dive/build.ml | 9 ++++--
src/plugins/dive/dive_graph.ml | 29 ++++++++++++++---
src/plugins/dive/dive_graph.mli | 4 ++-
src/plugins/dive/dive_types.ml | 1 +
src/plugins/dive/server_interface.ml | 4 ++-
7 files changed, 76 insertions(+), 15 deletions(-)
diff --git a/ivette/src/frama-c/plugins/dive/api/index.ts b/ivette/src/frama-c/plugins/dive/api/index.ts
index d3232121887..5f76720db27 100644
--- a/ivette/src/frama-c/plugins/dive/api/index.ts
+++ b/ivette/src/frama-c/plugins/dive/api/index.ts
@@ -150,7 +150,7 @@ export type node =
{ id: nodeId, label: string, kind: string, locality: nodeLocality,
is_root: boolean, backward_explored: string, forward_explored: string,
writes: location[], values?: string, range: number | string,
- type?: string };
+ type?: string, taint?: "direct" | "indirect" | "untainted" };
/** Decoder for `node` */
export const jNode: Json.Decoder<node> =
@@ -166,6 +166,12 @@ export const jNode: Json.Decoder<node> =
values: Json.jOption(Json.jString),
range: Json.jUnion<number | string>( Json.jNumber, Json.jString,),
type: Json.jOption(Json.jString),
+ taint: Json.jOption(
+ Json.jUnion<"direct" | "indirect" | "untainted">(
+ Json.jTag("direct"),
+ Json.jTag("indirect"),
+ Json.jTag("untainted"),
+ )),
});
/** Natural order for `node` */
@@ -174,7 +180,7 @@ export const byNode: Compare.Order<node> =
<{ id: nodeId, label: string, kind: string, locality: nodeLocality,
is_root: boolean, backward_explored: string, forward_explored: string,
writes: location[], values?: string, range: number | string,
- type?: string }>({
+ type?: string, taint?: "direct" | "indirect" | "untainted" }>({
id: byNodeId,
label: Compare.string,
kind: Compare.string,
@@ -186,6 +192,7 @@ export const byNode: Compare.Order<node> =
values: Compare.defined(Compare.string),
range: Compare.structural,
type: Compare.defined(Compare.string),
+ taint: Compare.defined(Compare.structural),
});
/** The dependency between two nodes */
diff --git a/ivette/src/frama-c/plugins/dive/style.json b/ivette/src/frama-c/plugins/dive/style.json
index 84d6611dee4..9b4b706fcba 100644
--- a/ivette/src/frama-c/plugins/dive/style.json
+++ b/ivette/src/frama-c/plugins/dive/style.json
@@ -45,22 +45,31 @@
"curve-style": "bezier",
"target-arrow-shape": "vee",
"target-arrow-color": "#888",
- "arrow-scale": 2.0
+ "arrow-scale": 2.0,
+ "z-compound-depth": "top"
}
},
{
"selector": "edge.multiple-selection",
"style": {
"overlay-color": "#aaa",
- "overlay-padding": "10px",
+ "overlay-padding": "4px",
"overlay-opacity": 0.4
}
},
{
- "selector": "edge.selection, :selected",
+ "selector": "edge.selection",
"style": {
"overlay-color": "#8bf",
- "overlay-padding": "10px",
+ "overlay-padding": "4px",
+ "overlay-opacity": 0.4
+ }
+ },
+ {
+ "selector": ":selected",
+ "style": {
+ "overlay-color": "#8bf",
+ "overlay-padding": "8px",
"overlay-opacity": 0.4
}
},
@@ -155,6 +164,22 @@
"ghost-opacity": "0.7"
}
},
+ {
+ "selector": "node[taint='direct']",
+ "style": {
+ "underlay-color": "#afa",
+ "underlay-padding": "14px",
+ "underlay-opacity": 1.0
+ }
+ },
+ {
+ "selector": "node[taint='indirect']",
+ "style": {
+ "underlay-color": "#afa",
+ "underlay-padding": "14px",
+ "underlay-opacity": 0.5
+ }
+ },
{
"selector": "edge[kind='callee']",
"style": {
diff --git a/src/plugins/dive/build.ml b/src/plugins/dive/build.ml
index 22a877074d1..a8ef4ad5078 100644
--- a/src/plugins/dive/build.ml
+++ b/src/plugins/dive/build.ml
@@ -103,6 +103,10 @@ struct
let to_callstacks stmt =
before stmt |> callstacks
+ let is_tainted kinstr lval =
+ let zone = to_zone kinstr lval in
+ before_kinstr kinstr |> is_tainted zone |> Result.to_option
+
let studia_direct_effect = function
| e, { Studia.Writes.direct = true } -> Some e
| _ -> None
@@ -139,8 +143,9 @@ end
let update_node_values node kinstr lval =
let typ = Cil.typeOfLval lval
- and cvalue = Eval.to_cvalue kinstr lval in
- Graph.update_node_values node cvalue typ
+ and cvalue = Eval.to_cvalue kinstr lval
+ and taint = Eval.is_tainted kinstr lval in
+ Graph.update_node_values node ~typ ~cvalue ~taint
(* --- Locations handling --- *)
diff --git a/src/plugins/dive/dive_graph.ml b/src/plugins/dive/dive_graph.ml
index 736d4eb7df4..1c60f09ba34 100644
--- a/src/plugins/dive/dive_graph.ml
+++ b/src/plugins/dive/dive_graph.ml
@@ -37,6 +37,7 @@ let new_node
node_hidden = false;
node_values = None;
node_range = Empty;
+ node_taint = None;
node_writes_computation = NotDone;
node_reads_computation = NotDone;
node_writes_stmts = [];
@@ -123,12 +124,21 @@ let edges g =
fold_edges_e (fun d acc -> d ::acc) g []
-let update_node_values node new_values typ =
- let join n = Cvalue.V.join n new_values in
- node.node_values <-
- Some (Option.fold ~some:join ~none:new_values node.node_values);
+let update_node_values node ~typ ~cvalue ~taint =
+ let join_taint t1 t2 =
+ let open Eva.Results in
+ match t1, t2 with
+ | Direct, _ | _, Direct -> Direct
+ | Indirect, _ | _, Indirect -> Indirect
+ | Untainted, Untainted -> Untainted
+ in
+ node.node_values <- Some (
+ Option.fold ~some:(Cvalue.V.join cvalue) ~none:cvalue node.node_values);
node.node_range <-
- Node_range.(upper_bound node.node_range (evaluate new_values typ))
+ Node_range.(upper_bound node.node_range (evaluate cvalue typ));
+ Option.iter (fun taint ->
+ node.node_taint <- Some (
+ Option.fold ~some:(join_taint taint) ~none:taint node.node_taint)) taint
let find_independant_nodes g roots =
let module Dfs = Graph.Traverse.Dfs (struct
@@ -325,6 +335,11 @@ struct
| Partial _ -> `String "partial"
| NotDone -> `String "no"
+ let output_taint = function
+ | Eva.Results.Direct -> `String "direct"
+ | Indirect -> `String "inddirect"
+ | Untainted -> `String "untainted"
+
let output_node node =
let label = Pretty_utils.to_string Node_kind.pretty node.node_kind in
`Assoc ([
@@ -345,6 +360,10 @@ struct
let typ = Cil.typeOfLval lval in
let str = Pretty_utils.to_string Cil_printer.pp_typ typ in
[("type", `String str)]
+ end @
+ begin match node.node_taint with
+ | None -> []
+ | Some t -> [("taint", output_taint t)]
end)
let output_dep (n1,dep,n2) =
diff --git a/src/plugins/dive/dive_graph.mli b/src/plugins/dive/dive_graph.mli
index e2991d9b23b..48047ba0396 100644
--- a/src/plugins/dive/dive_graph.mli
+++ b/src/plugins/dive/dive_graph.mli
@@ -38,7 +38,9 @@ val create_node :
val remove_node : t -> node -> unit
-val update_node_values : node -> Cvalue.V.t -> Cil_types.typ -> unit
+val update_node_values : node ->
+ typ:Cil_types.typ -> cvalue:Cvalue.V.t -> taint:Eva.Results.taint option ->
+ unit
val create_dependency : t -> Cil_types.kinstr ->
node -> dependency_kind -> node -> unit
diff --git a/src/plugins/dive/dive_types.ml b/src/plugins/dive/dive_types.ml
index 56a62322617..9f4235dc75f 100644
--- a/src/plugins/dive/dive_types.ml
+++ b/src/plugins/dive/dive_types.ml
@@ -53,6 +53,7 @@ type node = {
mutable node_hidden : bool;
mutable node_values : Cvalue.V.t option;
mutable node_range : node_range;
+ mutable node_taint : Eva.Results.taint option;
mutable node_writes_computation : computation;
mutable node_reads_computation : computation;
mutable node_writes_stmts : Cil_types.stmt list;
diff --git a/src/plugins/dive/server_interface.ml b/src/plugins/dive/server_interface.ml
index 7f8cd7e4177..c29359d807d 100644
--- a/src/plugins/dive/server_interface.ml
+++ b/src/plugins/dive/server_interface.ml
@@ -200,7 +200,9 @@ struct
"writes", Jarray Kernel_ast.KfMarker.jtype;
"values", Joption Jstring;
"range", Junion [ Jnumber ; Jstring ];
- "type", Joption Jstring
+ "type", Joption Jstring;
+ "taint", Joption (Junion [
+ Jtag "direct"; Jtag "indirect"; Jtag "untainted"])
])
end
--
GitLab