ROSE
0.9.13.72

Various tools for performing tainted flow analysis.
Example usage can be found in tests/nonsmoke/functional/roseTests/binaryTests/taintedFlow.C
Definition at line 17 of file BinaryTaintedFlow.h.
#include <BinaryTaintedFlow.h>
Classes  
class  MergeFunction 
class  State 
Taint state. More...  
class  TransferFunction 
Public Types  
enum  Taintedness { BOTTOM, NOT_TAINTED, TAINTED, TOP } 
Taint values. More...  
enum  Approximation { UNDER_APPROXIMATE, OVER_APPROXIMATE } 
Mode of operation. More...  
typedef std::pair< DataFlow::Variable, Taintedness >  VariableTaint 
VariableTaintedness pair. More...  
typedef State::Ptr  StatePtr 
Reference counting pointer to State. More...  
Public Member Functions  
TaintedFlow (const InstructionSemantics2::BaseSemantics::DispatcherPtr &userDispatcher)  
Constructs a tainted flow analysis. More...  
template<class CFG >  
void  computeFlowGraphs (const CFG &cfg, size_t cfgStartVertex) 
Compute data flow graphs. More...  
const DataFlow::VariableList &  variables () const 
List of variables. More...  
StatePtr  stateInstance (Taintedness taint) const 
Creates a new state. More...  
template<class CFG >  
void  runToFixedPoint (const CFG &cfg, size_t cfgStartVertex, const StatePtr &initialState) 
Run data flow. More...  
StatePtr  getFinalState (size_t cfgVertexId) const 
Query results. More...  
Approximation  approximation () const 
Property: approximation. More...  
void  approximation (Approximation a) 
Property: approximation. More...  
SmtSolverPtr  smtSolver () const 
Property: SMT solver. More...  
void  smtSolver (const SmtSolverPtr &solver) 
Property: SMT solver. More...  
const DataFlow::VertexFlowGraphs &  vertexFlowGraphs () const 
Property: data flow graphs. More...  
void  vertexFlowGraphs (const DataFlow::VertexFlowGraphs &graphMap) 
Property: data flow graphs. More...  
Static Public Member Functions  
static Taintedness  merge (Taintedness, Taintedness) 
Merges two taint values. More...  
static void  initDiagnostics () 
Initialize diagnostics. More...  
typedef std::pair<DataFlow::Variable, Taintedness> Rose::BinaryAnalysis::TaintedFlow::VariableTaint 
VariableTaintedness pair.
Definition at line 38 of file BinaryTaintedFlow.h.
Reference counting pointer to State.
State objects are reference counted and should not be deleted explicitly.
Definition at line 113 of file BinaryTaintedFlow.h.
Taint values.
These values form a lattice where NOT_TAINTED
and TAINTED
are children of TOP
and parents of BOTTOM
.
Definition at line 23 of file BinaryTaintedFlow.h.
Mode of operation.
The mode of operation can be set to under or overapproximate tainted flow. The only difference between the two modes are whether variable searching uses DataFlow::Variable::mustAlias (underapproximated) or DataFlow::Variable::mayAlias (overappoximated).
Definition at line 30 of file BinaryTaintedFlow.h.

inlineexplicit 
Constructs a tainted flow analysis.
The userDispatcher
is a CPU instruction dispatcher for instruction semantics and may use any semantic domain. The semantic domain will be used to identify variables in the analyzed specimen. The symbolic domain is the usual choice. The dispatcher need not have a valid state at this time; however, the state must be initialized before calling computeFlowGraphs (if that method is called).
Definition at line 175 of file BinaryTaintedFlow.h.

static 
Merges two taint values.
Given two taint values that are part of a taintedness lattice, return the least common ancestor.
Referenced by runToFixedPoint().

static 
Initialize diagnostics.
This is called by Rose::Diagnostics::initialize.

inline 
Property: approximation.
The approximation property determines whether taintedness is under or over approximated. Underapproximating mode uses mustAlias during the data flow transfer function, which limits taint flow only to those variables that certainly alias the data flow destination; while overapproximating mode uses mayAlias, which causes data to flow to all variables that could alias the data flow destination.
Definition at line 191 of file BinaryTaintedFlow.h.

inline 
Property: approximation.
The approximation property determines whether taintedness is under or over approximated. Underapproximating mode uses mustAlias during the data flow transfer function, which limits taint flow only to those variables that certainly alias the data flow destination; while overapproximating mode uses mayAlias, which causes data to flow to all variables that could alias the data flow destination.
Definition at line 192 of file BinaryTaintedFlow.h.

inline 
Property: SMT solver.
An SMT solver can be used for more accurate comparisons between variables. The default is to not use an SMT solver, in which case under and over approximations both degenerate to equality using only structural equivalence.
Definition at line 201 of file BinaryTaintedFlow.h.

inline 
Property: SMT solver.
An SMT solver can be used for more accurate comparisons between variables. The default is to not use an SMT solver, in which case under and over approximations both degenerate to equality using only structural equivalence.
Definition at line 202 of file BinaryTaintedFlow.h.

inline 
Compute data flow graphs.
This method computes a data flow graph for each reachable vertex of the control flow graph, and as a result also obtains the list of variables over which the tainted flow analysis will operate. It uses whatever algorithm is implemented in Rose::BinaryAnalysis::DataFlow::buildGraphPerVertex.
Definition at line 211 of file BinaryTaintedFlow.h.
References Rose::BinaryAnalysis::DataFlow::buildGraphPerVertex(), Rose::BinaryAnalysis::DataFlow::getUniqueVariables(), and Rose::StringUtility::plural().

inline 
Property: data flow graphs.
The taint analysis stores data flow graph for each CFG vertex. This information is used by the data flow engine's transfer function whenever it processes a CFG vertex. The user can provide his own information by setting this property, or have the property's value calculated by calling computeFlowGraphs.
Definition at line 234 of file BinaryTaintedFlow.h.

inline 
Property: data flow graphs.
The taint analysis stores data flow graph for each CFG vertex. This information is used by the data flow engine's transfer function whenever it processes a CFG vertex. The user can provide his own information by setting this property, or have the property's value calculated by calling computeFlowGraphs.
Definition at line 238 of file BinaryTaintedFlow.h.
References Rose::BinaryAnalysis::DataFlow::getUniqueVariables(), and Rose::StringUtility::plural().

inline 
List of variables.
Returns the list of variables over which tainted flow analysis is operating. The variables are in no particular order. The vertexFlowGraphs property must have already been set or calculated.
Definition at line 253 of file BinaryTaintedFlow.h.

inline 
Creates a new state.
Creates a new state with all variables initialized to the specified taintedness value. The vertexFlowGraphs property must have alraeady been set or calculated.
Definition at line 263 of file BinaryTaintedFlow.h.
References Rose::BinaryAnalysis::TaintedFlow::State::instance().

inline 
Run data flow.
Runs the tainted data flow analysis until it converges to a fixed point.
Definition at line 273 of file BinaryTaintedFlow.h.
References Rose::BinaryAnalysis::DataFlow::Engine< CFG, State, TransferFunction, MergeFunction, PathFeasibility >::getFinalStates(), merge(), Rose::StringUtility::plural(), and Rose::BinaryAnalysis::DataFlow::Engine< CFG, State, TransferFunction, MergeFunction, PathFeasibility >::runToFixedPoint().

inline 
Query results.
Returns a the taint state at the specified control flow graph vertex. The state is that which exists at the end of the specified vertex.
Definition at line 292 of file BinaryTaintedFlow.h.