Legend:
Library
Module
Module type
Parameter
Class
Class type
Propagate taint through expressions.
Semantics
Grammar
The following syntactic forms are used in propagation rules:
*a - load from address a, where a is immediate value; *a <- v - store value v at address a; exp ~> v - expression reduces to value v; v -> t - value v is tainted by a taint t; <bop> - BIL binary operation or BIL concat expression; <uop> - BIL unary, extract or cast expression.
Rules
Value v is tainted by taint t, denoted as v -> t, if there exists a deriviation of the following rules, proving this fact.
*a ~> v
a -> t
---------------- :: p_load
v -> t
*a <- v
v -> t
---------------- :: p_store
a -> t
v1 <bop> v2 ~> v3
v1 -> t
----------------- :: p_bop_lhs
v3 -> t
v1 <bop> v2 ~> v3
v2 -> t
----------------- :: p_bop_rhs
v3 -> t
<uop> v1 ~> v2
v1 -> t
----------------- :: p_uop
v2 -> t
Note 1: this class overrides only methods, that computes non-leaf expressions, leaving a space for extension for derived classes.
Note 2: we do not propagate taint from condition to branches in the if/then/else expression, since we're propagating only data dependency, not control dependency.
Although, one can argue, that in expression if c then x else y the result depends on c, since if we change c we will get different results, there is a good reason for not propagating this dependency - the consistency with BIR and BIL. Consider, BIL's if statement or BIR's conditional jump. If we will start to propagate taint from condition in ite expression, then we should also propagate it in BIL's and BIR's conditionals. Unfortunatelly the latter is not possible.