This issue contains a proposal/ implementation direction for taint checking
Taint checking
Class TaintRunner can be used to run taint checking on a symbolic statespace.
It is executed given a statespace, node, state and tainted value. Where the node and state are the introduction point of the taint.
The taint runner will follow symbolic tree maintaining internal taint records according to which instructions it encounters.
A taint record will have a reference to its corresponding statespace.node and state, and will have stored which memory locations are tainted.
After running the TaintRunner will return an TaintResult object.
This object can be used to easily check if values are tainted, example:
node = statespace.nodes[0]
state = node.states[0]
taint_result = taint_runner.execute(statespace, node, state, stack_indexes=[0])
state = node.states[2]
stack = state.mstate.stack
# One option would be:
tainted = taint_result.check(stack[0])
# Another would be:
tainted = taint_result.check(stack_index=0)
There are two ways we can go with the internal state. The first is to maintain some kind of mirror of the current state, with instead of z3
expressions bools indicating taint.
Another would be to have a list of tainted expressions, and check if they are used.
I'd propose the first one as this will probably be more robust.
Usecases
One possible usecase is integer overflow detection. When we find an instruction that overflows the overflowed value will be tainted. The result of an analysis run could be used to find all operations that store or use this value. This is useful for false positive detection.
JoranHonig
commented
6 years ago
This issue contains a proposal/ implementation direction for taint checking
Taint checking
Class TaintRunner can be used to run taint checking on a symbolic statespace. It is executed given a statespace, node, state and tainted value. Where the node and state are the introduction point of the taint. The taint runner will follow symbolic tree maintaining internal taint records according to which instructions it encounters. A taint record will have a reference to its corresponding statespace.node and state, and will have stored which memory locations are tainted. After running the TaintRunner will return an TaintResult object.
This object can be used to easily check if values are tainted, example:
There are two ways we can go with the internal state. The first is to maintain some kind of mirror of the current state, with instead of z3 expressions bools indicating taint.
Another would be to have a list of tainted expressions, and check if they are used.
I'd propose the first one as this will probably be more robust.
Usecases
One possible usecase is integer overflow detection. When we find an instruction that overflows the overflowed value will be tainted. The result of an analysis run could be used to find all operations that store or use this value. This is useful for false positive detection.