ROSE  0.9.10.89
Classes | Public Types | Public Member Functions | Static Public Member Functions | List of all members
Rose::BinaryAnalysis::TaintedFlow Class Reference

Description

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, TaintednessVariableTaint
 Variable-Taintedness 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::VariableListvariables () 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::VertexFlowGraphsvertexFlowGraphs () 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...
 

Member Typedef Documentation

Variable-Taintedness 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.

Member Enumeration Documentation

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 over-approximate tainted flow. The only difference between the two modes are whether variable searching uses DataFlow::Variable::mustAlias (under-approximated) or DataFlow::Variable::mayAlias (over-appoximated).

Definition at line 30 of file BinaryTaintedFlow.h.

Constructor & Destructor Documentation

Rose::BinaryAnalysis::TaintedFlow::TaintedFlow ( const InstructionSemantics2::BaseSemantics::DispatcherPtr userDispatcher)
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.

Member Function Documentation

static Taintedness Rose::BinaryAnalysis::TaintedFlow::merge ( Taintedness  ,
Taintedness   
)
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 void Rose::BinaryAnalysis::TaintedFlow::initDiagnostics ( )
static

Initialize diagnostics.

This is called by Rose::Diagnostics::initialize.

Approximation Rose::BinaryAnalysis::TaintedFlow::approximation ( ) const
inline

Property: approximation.

The approximation property determines whether taintedness is under or over approximated. Under-approximating 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 over-approximating 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.

void Rose::BinaryAnalysis::TaintedFlow::approximation ( Approximation  a)
inline

Property: approximation.

The approximation property determines whether taintedness is under or over approximated. Under-approximating 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 over-approximating 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.

SmtSolverPtr Rose::BinaryAnalysis::TaintedFlow::smtSolver ( ) const
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.

void Rose::BinaryAnalysis::TaintedFlow::smtSolver ( const SmtSolverPtr solver)
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.

template<class CFG >
void Rose::BinaryAnalysis::TaintedFlow::computeFlowGraphs ( const CFG &  cfg,
size_t  cfgStartVertex 
)
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().

const DataFlow::VertexFlowGraphs& Rose::BinaryAnalysis::TaintedFlow::vertexFlowGraphs ( ) const
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.

void Rose::BinaryAnalysis::TaintedFlow::vertexFlowGraphs ( const DataFlow::VertexFlowGraphs graphMap)
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().

const DataFlow::VariableList& Rose::BinaryAnalysis::TaintedFlow::variables ( ) const
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.

StatePtr Rose::BinaryAnalysis::TaintedFlow::stateInstance ( Taintedness  taint) const
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().

template<class CFG >
void Rose::BinaryAnalysis::TaintedFlow::runToFixedPoint ( const CFG &  cfg,
size_t  cfgStartVertex,
const StatePtr initialState 
)
inline
StatePtr Rose::BinaryAnalysis::TaintedFlow::getFinalState ( size_t  cfgVertexId) const
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.


The documentation for this class was generated from the following file: