From b4948117bb9eee0ba43750f30a82d2179b4f3afc Mon Sep 17 00:00:00 2001
From: Maxime Jacquemin <maxime.jacquemin@cea.fr>
Date: Wed, 4 Jan 2023 16:19:02 +0100
Subject: [PATCH] [Ivette] Taints in the AST
---
.../frama-c/plugins/eva/api/general/index.ts | 93 ++---
ivette/src/sandbox/codemirror6.tsx | 201 ++++++----
ivette/src/sandbox/dark-code.css | 22 ++
src/plugins/eva/api/general_requests.ml | 360 ++++++++----------
4 files changed, 357 insertions(+), 319 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 ff0ce5ec9b9..596145f3a59 100644
--- a/ivette/src/frama-c/plugins/eva/api/general/index.ts
+++ b/ivette/src/frama-c/plugins/eva/api/general/index.ts
@@ -219,63 +219,6 @@ const getDeadCode_internal: Server.GetRequest<Json.key<'#fct'>,deadCode> = {
/** Get the lists of unreachable and of non terminating statements in a function */
export const getDeadCode: Server.GetRequest<Json.key<'#fct'>,deadCode>= getDeadCode_internal;
-const taintedLvalues_internal: Server.GetRequest<
- Json.key<'#fundec'>,
- { lval: Json.key<'#lval'>,
- before:
- { data: "direct" | "indirect" | "untainted",
- indirect: "direct" | "indirect" | "untainted" },
- after:
- { data: "direct" | "indirect" | "untainted",
- indirect: "direct" | "indirect" | "untainted" } }[]
- > = {
- kind: Server.RqKind.GET,
- name: 'plugins.eva.general.taintedLvalues',
- input: Json.jKey<'#fundec'>('#fundec'),
- output: Json.jArray(
- Json.jObject({
- lval: Json.jKey<'#lval'>('#lval'),
- before: Json.jObject({
- data: Json.jUnion<"direct" | "indirect" | "untainted">(
- Json.jTag("direct"),
- Json.jTag("indirect"),
- Json.jTag("untainted"),
- ),
- indirect: Json.jUnion<"direct" | "indirect" |
- "untainted">(
- Json.jTag("direct"),
- Json.jTag("indirect"),
- Json.jTag("untainted"),
- ),
- }),
- after: Json.jObject({
- data: Json.jUnion<"direct" | "indirect" | "untainted">(
- Json.jTag("direct"),
- Json.jTag("indirect"),
- Json.jTag("untainted"),
- ),
- indirect: Json.jUnion<"direct" | "indirect" |
- "untainted">(
- Json.jTag("direct"),
- Json.jTag("indirect"),
- Json.jTag("untainted"),
- ),
- }),
- })),
- signals: [],
-};
-/** Get the tainted lvalues of a given function */
-export const taintedLvalues: Server.GetRequest<
- Json.key<'#fundec'>,
- { lval: Json.key<'#lval'>,
- before:
- { data: "direct" | "indirect" | "untainted",
- indirect: "direct" | "indirect" | "untainted" },
- after:
- { data: "direct" | "indirect" | "untainted",
- indirect: "direct" | "indirect" | "untainted" } }[]
- >= taintedLvalues_internal;
-
/** Taint status of logical properties */
export enum taintStatus {
/** **Not computed:**
@@ -314,6 +257,42 @@ const taintStatusTags_internal: Server.GetRequest<null,tag[]> = {
/** Registered tags for the above type. */
export const taintStatusTags: Server.GetRequest<null,tag[]>= taintStatusTags_internal;
+/** Lvalue taint status */
+export interface LvalueTaints {
+ /** tainted lvalue */
+ lval: Json.key<'#lval'>;
+ /** taint status */
+ taint: taintStatus;
+}
+
+/** Decoder for `LvalueTaints` */
+export const jLvalueTaints: Json.Decoder<LvalueTaints> =
+ Json.jObject({ lval: Json.jKey<'#lval'>('#lval'), taint: jTaintStatus,});
+
+/** Natural order for `LvalueTaints` */
+export const byLvalueTaints: Compare.Order<LvalueTaints> =
+ Compare.byFields
+ <{ lval: Json.key<'#lval'>, taint: taintStatus }>({
+ lval: Compare.string,
+ taint: byTaintStatus,
+ });
+
+const taintedLvalues_internal: Server.GetRequest<
+ Json.key<'#fundec'>,
+ LvalueTaints[]
+ > = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.eva.general.taintedLvalues',
+ input: Json.jKey<'#fundec'>('#fundec'),
+ output: Json.jArray(jLvalueTaints),
+ signals: [],
+};
+/** Get the tainted lvalues of a given function */
+export const taintedLvalues: Server.GetRequest<
+ Json.key<'#fundec'>,
+ LvalueTaints[]
+ >= taintedLvalues_internal;
+
/** Data for array rows [`properties`](#properties) */
export interface propertiesData {
/** Entry identifier. */
diff --git a/ivette/src/sandbox/codemirror6.tsx b/ivette/src/sandbox/codemirror6.tsx
index b2336e5450a..67276e47a59 100644
--- a/ivette/src/sandbox/codemirror6.tsx
+++ b/ivette/src/sandbox/codemirror6.tsx
@@ -6,6 +6,7 @@ import { EditorView, ViewPlugin, ViewUpdate } from '@codemirror/view';
import { Decoration, DecorationSet } from '@codemirror/view';
import { DOMEventMap as EventMap } from '@codemirror/view';
import { GutterMarker, gutter } from '@codemirror/view';
+import { showTooltip, Tooltip } from '@codemirror/view';
import { parser } from '@lezer/cpp';
import { tags } from '@lezer/highlight';
@@ -18,7 +19,7 @@ import * as Dome from 'dome';
import * as Utils from 'dome/data/arrays';
import * as Server from 'frama-c/server';
import * as States from 'frama-c/states';
-import type { key } from 'dome/data/json';
+import { key } from 'dome/data/json';
import * as Ast from 'frama-c/kernel/api/ast';
import { text } from 'frama-c/kernel/api/data';
import * as Eva from 'frama-c/plugins/eva/api/general';
@@ -35,10 +36,9 @@ import './dark-code.css';
// CodeMirror state's extensions types definitions
// -----------------------------------------------------------------------------
-// Helper types definitions
+// Helper types definitions.
export type Get<A> = (state: EditorState | undefined) => A;
export type Set<A> = (view: EditorView | null, value: A) => void;
-export type Equal<A> = (left: A, right: A) => boolean;
export interface Data<A, S> { init: A, get: Get<A>, structure: S }
// Event handlers type definition.
@@ -143,12 +143,12 @@ function getExtension<A>(dep: Dependency<A>): Extension {
// provided through the optional parameters <equal>. Providing an equality test
// for complex types can help improve performances by avoiding recomputing
// extensions depending on the field.
-export function createField<A>(init: A, equal?: Equal<A>): Field<A> {
+export function createField<A>(init: A): Field<A> {
const annot = Annotation.define<A>();
const create = (): A => init;
type Update<A> = (current: A, transaction: Transaction) => A;
const update: Update<A> = (current, tr) => tr.annotation(annot) ?? current;
- const field = StateField.define<A>({ create, update, compare: equal });
+ const field = StateField.define<A>({ create, update });
const get: Get<A> = (state) => state?.field(field) ?? init;
const useSet: Set<A> = (v, a) =>
React.useEffect(() => v?.dispatch({ annotations: annot.of(a) }), [v, a]);
@@ -204,6 +204,23 @@ export function createGutter<I extends Dict>(
return enables.concat(extension);
}
+// A Tooltip is an extension that adds decorations as a floating DOM element
+// above or below some text. See the CodeMirror's documentation on Tooltip
+// for further details.
+export function createTooltip<I extends Dict>(
+ deps: Dependencies<I>,
+ fn: (input: I) => Tooltip | Tooltip[] | undefined,
+): Extension {
+ const { structure, extension } = createAspect(deps, fn);
+ const show = showTooltip.computeN([structure], st => {
+ const tip = st.facet(structure);
+ if (tip === undefined) return [null];
+ if ('length' in tip) return tip;
+ return [tip];
+ });
+ return [extension, show];
+}
+
// An Event Handler is an extention responsible of performing a computation each
// time a DOM event (like <mouseup> or <contextmenu>) happens.
export function createEventHandler<I extends Dict>(
@@ -223,7 +240,7 @@ export function createEventHandler<I extends Dict>(
// -----------------------------------------------------------------------------
-// Utilitary types
+// Utilitary types and functions
// -----------------------------------------------------------------------------
// An alias type for functions and locations.
@@ -237,6 +254,14 @@ type Caller = { fct: key<'#fct'>, marker: key<'#stmt'> };
// A range is just a pair of position in the code.
interface Range { from: number, to: number }
+// Type checking that an input is defined.
+function isDef<A>(a: A | undefined): a is A { return a !== undefined; }
+
+// Map a function over a list, removing all inputs that returned undefined.
+function mapFilter<A, B>(xs: A[], fn: (x: A) => B | undefined): B[] {
+ return xs.map(fn).filter(isDef);
+}
+
// -----------------------------------------------------------------------------
@@ -246,29 +271,35 @@ interface Range { from: number, to: number }
// The code is given by the server has a tree but implemented with arrays and
// without information on the ranges of each element. It will be converted in a
// good old tree that carry those information.
-interface Tree extends Range { id?: string, children: Tree[] }
+interface Leaf extends Range { text: string }
+interface Node extends Range { id: string, children: Tree[] }
+type Tree = Leaf | Node;
-// A leaf tree with no children.
-const leaf = (from: number, to: number): Tree => ({ from, to, children: [] });
+// Utility functions on trees.
+function isLeaf (t: Tree): t is Leaf { return 'text' in t; }
+function isNode (t: Tree): t is Node { return 'id' in t && 'children' in t; }
+const empty: Tree = { text: '', from: 0, to: 0 };
// Convert an Ivette text (i.e a function's code) into a Tree, adding range
// information to each construction.
function textToTree(t: text): Tree | undefined {
- function aux(t: text, from: number): Tree | undefined {
- if (t === null) return undefined;
- if (typeof t === 'string') return leaf(from, from + t.length);
+ function aux(t: text, from: number): [Tree | undefined, number] {
+ if (t === null) return [undefined, from];
+ if (typeof t === 'string') {
+ const to = from + t.length;
+ return [{ text: t, from, to }, to];
+ }
+ if (t.length < 2 || typeof t[0] !== 'string') return [undefined, from];
const children: Tree[] = []; let acc = from;
for (const child of t.slice(1)) {
- const node = aux(child, acc);
- if (node) { acc = node.to; children.push(node); }
+ const [node, to] = aux(child, acc);
+ if (node) children.push(node);
+ acc = to;
}
- if (children.length === 0) return undefined;
- const to = children[children.length - 1].to;
- const finalFrom = children[0].from;
- const id = typeof t[0] === 'string' && t[0][0] === '#' ? t[0] : undefined;
- return { id, from: finalFrom, to, children };
+ return [{ id: t[0], from, to: acc, children }, acc];
}
- return aux(t, 0);
+ const [res] = aux(t, 0);
+ return res;
}
// Convert an Ivette text into a string to be displayed.
@@ -283,7 +314,8 @@ function textToString(text: text): string {
function markersRangesOfTree(tree: Tree): Map<string, Range>{
const ranges: Map<string, Range> = new Map();
const toRanges = (tree: Tree): void => {
- if (tree.id) ranges.set(tree.id, tree);
+ if (!isNode(tree)) return;
+ ranges.set(tree.id, tree);
for (const child of tree.children) toRanges(child);
};
toRanges(tree);
@@ -292,22 +324,15 @@ function markersRangesOfTree(tree: Tree): Map<string, Range>{
// Find the closest covering tagged node of a given position. Returns
// undefined if there is not relevant covering node.
-function coveringNode(tree: Tree, pos: number): Tree | undefined {
+function coveringNode(tree: Tree, pos: number): Node | undefined {
+ if (isLeaf(tree)) return undefined;
if (pos < tree.from || pos > tree.to) return undefined;
- if (pos === tree.from) return tree;
- const res = Utils.first(tree.children, (c) => coveringNode(c, pos));
- if (res) return res.id ? res : tree;
+ const child = Utils.first(tree.children, (c) => coveringNode(c, pos));
+ if (child && isNode(child)) return child;
if (tree.from <= pos && pos < tree.to) return tree;
return undefined;
}
-// Find the subtree whose root as the given marker as id, or undefined if it
-// does not exists in the tree.
-function findMarker(tree: Tree, marker: Marker): Tree | undefined {
- if (tree.id === marker) return tree;
- return Utils.first(tree.children, (c) => findMarker(c, marker));
-}
-
// -----------------------------------------------------------------------------
@@ -333,7 +358,7 @@ function createTextField(): Field<text> {
// This aspect computes the tree representing the currently displayed function's
// code, represented by the <Text> field.
-const Tree = createAspect({ t: Text }, ({ t }) => textToTree(t) ?? leaf(0, 0));
+const Tree = createAspect({ t: Text }, ({ t }) => textToTree(t) ?? empty);
// This aspect computes the markers ranges of the currently displayed function's
// tree, represented by the <Tree> aspect.
@@ -420,10 +445,10 @@ const CodeDecorator = createCodeDecorator();
function createCodeDecorator(): Extension {
const hoveredClass = Decoration.mark({ class: 'cm-hovered-code' });
const selectedClass = Decoration.mark({ class: 'cm-selected-code' });
- const deps = { tree: Tree, marker: Marker, hovered: Hovered };
- return createDecorator(deps, ({ tree, marker: m, hovered: h }) => {
- const selected = m && findMarker(tree, m);
- const hovered = h && findMarker(tree, h);
+ const deps = { ranges: Ranges, marker: Marker, hovered: Hovered };
+ return createDecorator(deps, ({ ranges, marker: m, hovered: h }) => {
+ const selected = m && ranges.get(m);
+ const hovered = h && ranges.get(h);
const range = selected && selectedClass.range(selected.from, selected.to);
const add = hovered && [ hoveredClass.range(hovered.from, hovered.to) ];
const set = range ? RangeSet.of(range) : RangeSet.empty;
@@ -447,11 +472,9 @@ function createDeadCodeDecorator(): Extension {
const deps = { dead: Dead, ranges: Ranges };
return createDecorator(deps, ({ dead, ranges }) => {
const range = (marker: string): Range | undefined => ranges.get(marker);
- function isDef<A>(a: A | undefined): a is A { return a !== undefined; }
- const getRanges = (xs: string[]): Range[] => xs.map(range).filter(isDef);
- const unreachableRanges = getRanges(dead.unreachable);
+ const unreachableRanges = mapFilter(dead.unreachable, range);
const unreachable = unreachableRanges.map(r => uClass.range(r.from, r.to));
- const nonTermRanges = getRanges(dead.nonTerminating);
+ const nonTermRanges = mapFilter(dead.nonTerminating, range);
const nonTerm = nonTermRanges.map(r => tClass.range(r.from, r.to));
return RangeSet.of(unreachable.concat(nonTerm), true);
});
@@ -475,16 +498,11 @@ const PropertiesStatuses = createField<Properties.statusData[]>([]);
const PropertiesRanges = createPropertiesRange();
interface PropertyRange extends Properties.statusData { range: Range }
function createPropertiesRange(): Aspect<PropertyRange[]> {
- const deps = { statuses: PropertiesStatuses, ranges: Ranges };
- return createAspect(deps, ({ statuses, ranges }) => {
- type R = PropertyRange | undefined;
- const isDef = (r: R): r is PropertyRange => r !== undefined;
- const fn = (p: Properties.statusData): R => {
- const range = ranges.get(p.key);
- return range && { ...p, range };
- };
- return statuses.map(fn).filter(isDef);
- });
+ const deps = { props: PropertiesStatuses, ranges: Ranges };
+ return createAspect(deps, ({ props, ranges }) => mapFilter(props, (p) => {
+ const range = ranges.get(p.key);
+ return range && { ...p, range };
+ }));
}
// This aspect computes the tag associated to each property.
@@ -657,6 +675,62 @@ function createContextMenuHandler(): Extension {
+// -----------------------------------------------------------------------------
+// Tainted lvalues
+// -----------------------------------------------------------------------------
+
+type Taints = Eva.LvalueTaints;
+const TaintedLvalues = createField<Taints[] | undefined>(undefined);
+
+function textOfTaint(taint: Eva.taintStatus): string {
+ switch (taint) {
+ case 'not_computed': return 'The taint has not been computed';
+ case 'error': return 'There was an error during the taint computation';
+ case 'not_applicable': return 'No taint for this lvalue';
+ case 'direct_taint': return 'This lvalue can be affected by an attacker';
+ case 'indirect_taint':
+ return 'This lvalue depends on path conditions that can \
+ be affected by an attacker';
+ case 'not_tainted': return 'This lvalue is safe'
+ }
+ return '';
+}
+
+const TaintedLvaluesDecorator = createTaintedLvaluesDecorator();
+function createTaintedLvaluesDecorator(): Extension {
+ const mark = Decoration.mark({ class: 'cm-tainted' });
+ const deps = { ranges: Ranges, tainted: TaintedLvalues };
+ return createDecorator(deps, ({ ranges, tainted = [] }) => {
+ const find = (t: Taints): Range | undefined => ranges.get(t.lval);
+ const marks = mapFilter(tainted, find).map(r => mark.range(r.from, r.to));
+ return RangeSet.of(marks, true);
+ });
+}
+
+const TaintTooltip = createTaintTooltip();
+function createTaintTooltip(): Extension {
+ const deps = { hovered: Hovered, ranges: Ranges, tainted: TaintedLvalues };
+ return createTooltip(deps, ({ hovered, ranges, tainted }) => {
+ const hoveredTaint = tainted?.find(t => t.lval === hovered);
+ const hoveredNode = hovered && ranges.get(hovered);
+ if (!hoveredTaint || !hoveredNode) return undefined;
+ return {
+ pos: hoveredNode.from,
+ above: true,
+ strictSide: true,
+ arrow: true,
+ create: () => {
+ const dom = document.createElement('div');
+ dom.className = 'cm-tainted-tooltip';
+ dom.textContent = textOfTaint(hoveredTaint.taint);
+ return { dom };
+ }
+ }
+ });
+}
+
+
+
// -----------------------------------------------------------------------------
// Code highlighting and parsing
// -----------------------------------------------------------------------------
@@ -712,6 +786,13 @@ function useFctCallers(fct: Fct): Caller[] {
return result.map(([fct, marker]) => ({ fct, marker }));
}
+// Server request handler returning the tainted lvalues.
+function useFctTaints(fct: Fct): Eva.LvalueTaints[] {
+ const req = React.useMemo(() => Server.send(Eva.taintedLvalues, fct), [fct]);
+ const { result = [] } = Dome.usePromise(req);
+ return result;
+}
+
// -----------------------------------------------------------------------------
@@ -727,6 +808,8 @@ const baseExtensions: Extension[] = [
ContextMenuHandler,
PropertiesGutter,
foldGutter(),
+ TaintedLvaluesDecorator,
+ TaintTooltip,
Highlight, new LanguageSupport(cppLanguage),
];
@@ -773,21 +856,7 @@ function Editor(): JSX.Element {
Hovered.set(editor.current, hovered?.marker);
Dead.set(editor.current, useFctDead(fct));
Callers.set(editor.current, useFctCallers(fct));
-
- /*
- const getTaints = Eva.taintedLvalues;
- const taintReq = React.useMemo(() => Server.send(getTaints, fct), [fct]);
- const { result: taints } = Dome.usePromise(taintReq);
-
- if (taints && data) {
- console.log('-----');
- for (const taint of taints) {
- const range = data.ranges.get(taint.lval);
- console.log (taint.lval, range, taint.before, taint.after);
- }
- console.log('-----');
- }
- */
+ TaintedLvalues.set(editor.current, useFctTaints(fct));
return <div className='cm-global-box' ref={parent} />;
}
diff --git a/ivette/src/sandbox/dark-code.css b/ivette/src/sandbox/dark-code.css
index b6db04d0853..0f2c5b341f7 100644
--- a/ivette/src/sandbox/dark-code.css
+++ b/ivette/src/sandbox/dark-code.css
@@ -38,6 +38,28 @@
.cm-dead-code { color: var(--dead-code); }
.cm-non-term-code { color: var(--dead-code); }
+.cm-tainted {
+ text-decoration: underline var(--warning) solid 1px;
+ text-decoration-skip-ink: none;
+ text-underline-position: under;
+}
+
+.cm-tooltip.cm-tainted-tooltip {
+ background-color: var(--background-softer);
+ color: var(--text-highlighted);
+ border: 1px solid var(--background-profound);
+ padding: 2px 7px;
+ border-radius: 4px;
+}
+
+.cm-tooltip-above.cm-tainted-tooltip .cm-tooltip-arrow:before {
+ border-top-color: var(--background-profound);
+}
+
+.cm-tooltip-above.cm-tainted-tooltip .cm-tooltip-arrow:after {
+ border-top-color: var(--background-softer);
+}
+
.cm-def { color: var(--codemirror-def); }
.cm-comment { color: var(--codemirror-comment); }
diff --git a/src/plugins/eva/api/general_requests.ml b/src/plugins/eva/api/general_requests.ml
index 59ea193b414..7525067edf4 100644
--- a/src/plugins/eva/api/general_requests.ml
+++ b/src/plugins/eva/api/general_requests.ml
@@ -69,6 +69,8 @@ let () = Request.register ~package
~input:(module Kernel_ast.Kf) ~output:(module Data.Jlist (CallSite))
callers
+
+
(* ----- Functions ---------------------------------------------------------- *)
module Functions =
@@ -93,6 +95,8 @@ struct
Analysis.register_computation_hook (fun _ -> f () ))
end
+
+
(* ----- Dead code: unreachable and non-terminating statements -------------- *)
type dead_code =
@@ -109,6 +113,7 @@ module DeadCode = struct
let unreachable = Record.field record ~name:"unreachable"
~descr:(Markdown.plain "List of unreachable statements.")
(module Data.Jlist (Kernel_ast.Marker))
+
let non_terminating = Record.field record ~name:"nonTerminating"
~descr:(Markdown.plain "List of reachable but non terminating statements.")
(module Data.Jlist (Kernel_ast.Marker))
@@ -159,7 +164,9 @@ let () = Request.register ~package
~output:(module DeadCode)
dead_code
-(* ----- Register Eva information ------------------------------------------- *)
+
+
+(* ----- Register Eva values information ------------------------------------ *)
let term_lval_to_lval tlval =
try Logic_to_c.term_lval_to_lval tlval
@@ -199,167 +206,79 @@ let () =
~enable:Analysis.is_computed
print_value
-let evaluate_taint expr request =
- let (let+) = Option.bind in
- let Results.{ data ; indirect } = Results.expr_dependencies expr request in
- let+ data = Results.is_tainted data request |> Result.to_option in
- let+ indirect = Results.is_tainted indirect request |> Result.to_option in
- Some (data, indirect)
-
-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) ->
- let lval = term_lval_to_lval tlval in
- Cil.new_exp ~loc (Lval lval), stmt
- | _ -> 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 ())
+(* ----- Register Eva taints information ------------------------------------ *)
+let expr_of_lval v = Cil.new_exp ~loc:Cil_datatype.Location.unknown (Lval v)
+module EvaTaints = struct
+ open Results
-module LvalueTaints = struct
- module Lval = Kernel_ast.Lval
-
- type taints = { data: Results.taint ; indirect: Results.taint }
- type lvalue_taints = { lval: Lval.t ; before: taints ; after: taints }
-
- module Taint: Data.S with type t = Results.taint = struct
- type t = Results.taint
- let tag strs = Package.Junion (List.map (fun s -> Package.Jtag s) strs)
- let jtype = tag [ "direct" ; "indirect" ; "untainted" ]
- let to_json = function
- | Results.Direct -> Json.of_string "direct"
- | Results.Indirect -> Json.of_string "indirect"
- | Results.Untainted -> Json.of_string "untainted"
- let of_json json =
- match Yojson.Basic.Util.to_string json with
- | "direct" -> Results.Direct
- | "indirect" -> Results.Indirect
- | "untainted" -> Results.Untainted
- | _ -> Data.failure "Not a valid taint status"
- end
+ let evaluate expr request =
+ let (let+) = Option.bind in
+ let { data ; indirect } = expr_dependencies expr request in
+ let+ data = is_tainted data request |> Result.to_option in
+ let+ indirect = is_tainted indirect request |> Result.to_option in
+ Some (data, indirect)
- module Taints: Data.S with type t = taints = struct
- type t = taints
- let tag strs = Package.Jrecord (List.map (fun s -> (s, Taint.jtype)) strs)
- let jtype = tag [ "data" ; "indirect" ]
- let to_json { data ; indirect } =
- let data = Taint.to_json data in
- let indirect = Taint.to_json indirect in
- `Assoc [ ("data", data) ; ("indirect", indirect) ]
- let of_json = function
- | `Assoc [ ("data", data) ; ("indirect", indirect) ] ->
- { data = Taint.of_json data ; indirect = Taint.of_json indirect }
- | _ -> Data.failure "Not a valid taints record"
- end
+ let expr_of_marker = let open Printer_tag in function
+ | PLval (_, Kstmt stmt, lval) -> Some (expr_of_lval lval, stmt)
+ | PExp (_, Kstmt stmt, expr) -> Some (expr, stmt)
+ | PVDecl (_, Kstmt stmt, vi) -> Some (expr_of_lval (Var vi, NoOffset), stmt)
+ | PTermLval (_, Kstmt stmt, _, tlval) ->
+ Some (term_lval_to_lval tlval |> expr_of_lval, stmt)
+ | _ -> None
- module LvalueTaints: Data.S with type t = lvalue_taints = struct
- type t = lvalue_taints
- let jtype = Package.Jrecord [
- ("lval", Lval.jtype) ;
- ("before", Taints.jtype) ;
- ("after", Taints.jtype)
- ]
- let to_json { lval ; before ; after } =
- let lval = Lval.to_json lval in
- let before = Taints.to_json before in
- let after = Taints.to_json after in
- `Assoc [ ("lval", lval) ; ("before", before) ; ("after", after) ]
- let of_json = function
- | `Assoc [ ("lval", lval) ; ("before", before) ; ("after", after) ] ->
- let lval = Lval.of_json lval in
- let before = Taints.of_json before in
- let after = Taints.of_json after in
- { lval ; before ; after }
- | _ -> Data.failure "Not a valid lval taints"
- end
+ let of_marker marker =
+ let (let+) = Option.bind in
+ let+ expr, stmt = expr_of_marker marker in
+ let+ before = evaluate expr (before stmt) in
+ let+ after = evaluate expr (after stmt) in
+ Some (before, after)
- class tainted_lvalues taints = object (self)
- inherit Visitor.generic_frama_c_visitor
- (Visitor_behavior.copy (Project.current ()))
- method! vlval lval =
- match self#current_stmt with
- | None -> DoChildren
- | Some stmt ->
- let expr = Cil.new_exp ~loc:Cil_datatype.Location.unknown (Lval lval) in
- let before = evaluate_taint expr Results.(before stmt) in
- let after = evaluate_taint expr Results.(after stmt) in
- let add r = Cil_datatype.Lval.Hashtbl.add taints lval (stmt, r) in
- let is_tainted (d, i) = Results.(d != Untainted || i != Untainted) in
- let is_tainted b a = is_tainted b || is_tainted a in
- match before, after with
- | Some b, Some a when is_tainted b a -> add (b, a) ; DoChildren
- | _, _ -> DoChildren
- end
+ let to_string = function
+ | Untainted -> "untainted"
+ | Direct -> "direct taint"
+ | Indirect -> "indirect taint"
- let to_value_taints lval (stmt, ((bdir, bind), (adir, aind))) ls =
- let before = { data = bdir ; indirect = bind } in
- let after = { data = adir ; indirect = aind } in
- { lval = (Kstmt stmt, lval) ; before ; after } :: ls
+ let pretty fmt = function
+ | taint, Untainted -> Format.fprintf fmt "%s" (to_string taint)
+ | data, indirect ->
+ let sep = match data with Untainted -> "but" | _ -> "and" in
+ Format.fprintf fmt
+ "%s to the value, %s %s to values used to compute lvalues adresses"
+ (to_string data) sep (to_string indirect)
+
+ let print_taint fmt marker =
+ let before, after = of_marker marker |> Option.get in
+ if before = after then Format.fprintf fmt "%a" pretty before
+ else Format.fprintf fmt "Before: %a@\nAfter: %a" pretty before pretty after
+
+ let eva_taints_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."
- let tainted_lvals_of_func fundec =
- let taints = Cil_datatype.Lval.Hashtbl.create 17 in
- ignore (Visitor.visitFramacFunction (new tainted_lvalues taints) fundec) ;
- Cil_datatype.Lval.Hashtbl.fold to_value_taints taints [] |> List.rev
+ let () =
+ let taint_computed = Taint_domain.Store.is_computed in
+ let enable () = Analysis.is_computed () && taint_computed () in
+ Server.Kernel_ast.Information.register
+ ~id:"eva.taint" ~label:"Taint" ~descr: "Taint status according to Eva"
+ ~title:eva_taints_title ~enable print_taint
- let () = Request.register ~package ~kind:`GET ~name:"taintedLvalues"
- ~descr:(Markdown.plain "Get the tainted lvalues of a given function")
- ~input:(module (Kernel_ast.Fundec))
- ~output:(module (Data.Jlist (LvalueTaints)))
- tainted_lvals_of_func
+ let update = Server.Kernel_ast.Information.update
+ let () = Analysis.register_computation_hook (fun _ -> update ())
end
-(* ----- Red and tainted alarms --------------------------------------------- *)
+(* ----- Taint statuses ----------------------------------------------------- *)
-module Taint = struct
+module TaintStatus = struct
open Server.Data
type taint = Results.taint = Direct | Indirect | Untainted
@@ -374,49 +293,98 @@ module Taint = struct
~value dictionary
let tag_not_computed =
- tag (Error NotComputed) "not_computed" ""
- "Not computed" "the Eva taint domain has not been enabled, \
- or the Eva analysis has not been run"
+ tag (Error NotComputed) "not_computed" "" "Not computed"
+ "the Eva taint domain has not been enabled, \
+ or the Eva analysis has not been run"
let tag_error =
- tag (Error LogicError) "error" "Error"
- "Error" "the memory zone on which this property depends \
- could not be computed"
+ 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" "—"
- "Not applicable" "no taint for this kind of property"
+ tag (Error Irrelevant) "not_applicable" "—" "Not applicable"
+ "no taint for this kind of property"
let tag_direct_taint =
- tag (Ok Direct) "direct_taint" "Tainted (direct)"
- "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_indirect_taint =
- tag (Ok Indirect) "indirect_taint" "Tainted (indirect)"
- "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 Untainted) "not_tainted" "Untainted"
- "Untainted property" "this property is safe"
-
- let () = Enum.set_lookup dictionary
- begin function
- | 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
+ tag (Ok Untainted) "not_tainted" "Untainted" "Untainted property"
+ "this property is safe"
+
+ let () = Enum.set_lookup dictionary @@ function
+ | 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
let data = Request.dictionary ~package ~name:"taintStatus"
~descr:(Markdown.plain "Taint status of logical properties") dictionary
include (val data : S with type t = (taint, error) result)
+end
+
+
+
+(* ----- Tainted lvalues ---------------------------------------------------- *)
+
+module LvalueTaints = struct
+ module Table = Cil_datatype.Lval.Hashtbl
+
+ module Status = struct
+ type record
+ let record: record Data.Record.signature = Data.Record.signature ()
+ let field name d = Data.Record.field record ~name ~descr:(Markdown.plain d)
+ let lval_field = field "lval" "tainted lvalue" (module Kernel_ast.Lval)
+ let taint_field = field "taint" "taint status" (module TaintStatus)
+ let name, descr = "LvalueTaints", Markdown.plain "Lvalue taint status"
+ let publication = Data.Record.publish record ~package ~name ~descr
+ include (val publication: Data.Record.S with type r = record)
+ let create lval taint = set lval_field lval @@ set taint_field taint default
+ end
+
+ let current_project () = Visitor_behavior.copy (Project.current ())
+ class tainted_lvalues taints = object (self)
+ inherit Visitor.generic_frama_c_visitor (current_project ())
+ method! vlval lval =
+ let expr = expr_of_lval lval in
+ match self#current_stmt with
+ | None -> DoChildren
+ | Some stmt ->
+ match Results.after stmt |> EvaTaints.evaluate expr with
+ | Some (Results.Untainted, _) -> DoChildren
+ | Some (t, _) -> Table.add taints lval (Kstmt stmt, t) ; DoChildren
+ | None -> DoChildren
+ end
+
+ let get_tainted_lvals fundec =
+ let taints = Table.create 17 in
+ Visitor.visitFramacFunction (new tainted_lvalues taints) fundec |> ignore ;
+ let fn lval (ki, taint) acc = Status.create (ki, lval) (Ok taint) :: acc in
+ Table.fold fn taints [] |> List.rev
+
+ let () = Request.register ~package ~kind:`GET ~name:"taintedLvalues"
+ ~descr:(Markdown.plain "Get the tainted lvalues of a given function")
+ ~input:(module (Kernel_ast.Fundec))
+ ~output:(module (Data.Jlist (Status)))
+ get_tainted_lvals
+end
+
+
+
+(* ----- Red and tainted alarms --------------------------------------------- *)
+
+module PropertiesData = struct
+ open TaintStatus
let zone_of_predicate kinstr predicate =
let state = Results.(before_kinstr kinstr |> get_cvalue_model) in
@@ -439,40 +407,39 @@ module Taint = struct
| _ -> Error Irrelevant
let is_tainted_property ip =
- if not (Analysis.is_computed () && Taint_domain.Store.is_computed ())
- then Error NotComputed
- else
+ if Analysis.is_computed () && Taint_domain.Store.is_computed () then
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"
- ~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)
+ else Error NotComputed
-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.is_tainted_property ip)
+ let () =
+ let model = States.model () in
+ let descr = "Is the property invalid in some context of the analysis?" in
+ States.column model
+ ~name:"priority"
+ ~descr:(Markdown.plain descr)
+ ~data:(module Data.Jbool)
+ ~get:Red_statuses.is_red ;
+ let descr = "Is the property tainted according to the Eva taint domain?" in
+ States.column model
+ ~name:"taint"
+ ~descr:(Markdown.plain descr)
+ ~data:(module TaintStatus)
+ ~get:is_tainted_property ;
+ ignore @@ 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
+end
-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
(* ----- Analysis statistics ------------------------------------------------ *)
@@ -684,6 +651,7 @@ let _array =
model
+
(* ----- Domains states ----------------------------------------------------- *)
let compute_lval_deps request lval =
--
GitLab