Taint Analysis

plugins.eva.taint.taintNames (STATE)

List of taint names

plugins.eva.taint.signalTaintNames (SIGNAL)

Signal for state taintNames

plugins.eva.taint.getTaintNames (GET)

Getter for state taintNames

input ::= null

output ::= string []

plugins.eva.taint.currentTaints (STATE)

Names of the currently selected taints, if any

plugins.eva.taint.signalCurrentTaints (SIGNAL)

Signal for state currentTaints

plugins.eva.taint.getCurrentTaints (GET)

Getter for state currentTaints

input ::= null

output ::= string []

plugins.eva.taint.setCurrentTaints (SET)

Setter for state currentTaints

input ::= string []

output ::= null

plugins.eva.taint.taintStatus (DATA)

Taint status of logical properties

taintStatus ::= tags…

Tags Value Description
"not_computed" Not computed: the Eva taint domain has not been enabled, or the Eva analysis has not been run
Error "error" Error: the memory zone on which this property depends could not be computed
— "not_applicable" Not applicable: no taint for this kind of property
Tainted (direct) "direct_taint" Direct taint: this property is related to a memory location that can be affected by an attacker
Tainted (indirect) "indirect_taint" Indirect taint: this property is related to a memory location whose assignment depends on path conditions that can be affected by an attacker
Untainted "not_tainted" Untainted property: this property is safe

plugins.eva.taint.taintStatusTags (GET)

Registered tags for the above type.

input ::= null

output ::= tag []

plugins.eva.taint.LvalueTaints (DATA)

Lvalue taint status

LvalueTaints ::= { fields… }

Field Format Description
"lval" marker tainted lvalue
"taint" taintStatus taint status

plugins.eva.taint.taintedLvalues (GET)

Get the tainted lvalues of a given function

input ::= decl

output ::= LvalueTaints []

signals