Description

Various tools for performing tainted flow analysis.

Example usage can be found in tests/nonsmoke/functional/roseTests/binaryTests/taintedFlow.C

Definition at line 18 of file TaintedFlow.h.

#include <Rose/BinaryAnalysis/TaintedFlow.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
	Variable-Taintedness pair.

typedef State::Ptr	StatePtr
	Reference counting pointer to State.

Public Member Functions
	TaintedFlow (const InstructionSemantics::BaseSemantics::DispatcherPtr &userDispatcher)
	Constructs a tainted flow analysis.

template<class CFG >
void	computeFlowGraphs (const CFG &cfg, size_t cfgStartVertex)
	Compute data flow graphs.

const DataFlow::VariableList &	variables () const
	List of variables.

StatePtr	stateInstance (Taintedness taint) const
	Creates a new state.

template<class CFG >
void	runToFixedPoint (const CFG &cfg, size_t cfgStartVertex, const StatePtr &initialState)
	Run data flow.

StatePtr	getFinalState (size_t cfgVertexId) const
	Query results.


Approximation	approximation () const
	Property: approximation.

void	approximation (Approximation a)
	Property: approximation.


SmtSolverPtr	smtSolver () const
	Property: SMT solver.

void	smtSolver (const SmtSolverPtr &solver)
	Property: SMT solver.


const DataFlow::VertexFlowGraphs &	vertexFlowGraphs () const
	Property: data flow graphs.

void	vertexFlowGraphs (const DataFlow::VertexFlowGraphs &graphMap)
	Property: data flow graphs.

Static Public Member Functions
static Taintedness	merge (Taintedness, Taintedness)
	Merges two taint values.

static void	initDiagnostics ()
	Initialize diagnostics.

Member Typedef Documentation

◆ VariableTaint

typedef std::pair<DataFlow::Variable, Taintedness> Rose::BinaryAnalysis::TaintedFlow::VariableTaint

Variable-Taintedness pair.

Definition at line 39 of file TaintedFlow.h.

◆ StatePtr

typedef State::Ptr Rose::BinaryAnalysis::TaintedFlow::StatePtr

Reference counting pointer to State.

State objects are reference counted and should not be deleted explicitly.

Definition at line 114 of file TaintedFlow.h.

Member Enumeration Documentation

◆ Taintedness

enum Rose::BinaryAnalysis::TaintedFlow::Taintedness

Taint values.

These values form a lattice where NOT_TAINTED and TAINTED are children of TOP and parents of BOTTOM.

Definition at line 24 of file TaintedFlow.h.

◆ Approximation

enum Rose::BinaryAnalysis::TaintedFlow::Approximation

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 31 of file TaintedFlow.h.

Constructor & Destructor Documentation

◆ TaintedFlow()

Rose::BinaryAnalysis::TaintedFlow::TaintedFlow ( const InstructionSemantics::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 176 of file TaintedFlow.h.

Member Function Documentation

◆ merge()

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().

◆ initDiagnostics()

static void Rose::BinaryAnalysis::TaintedFlow::initDiagnostics ( )

static

Initialize diagnostics.

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

◆ approximation() [1/2]

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 192 of file TaintedFlow.h.

◆ approximation() [2/2]

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 193 of file TaintedFlow.h.

◆ smtSolver() [1/2]

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 202 of file TaintedFlow.h.

◆ smtSolver() [2/2]

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 203 of file TaintedFlow.h.

◆ computeFlowGraphs()

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 212 of file TaintedFlow.h.

References Rose::BinaryAnalysis::DataFlow::buildGraphPerVertex(), Rose::BinaryAnalysis::DataFlow::getUniqueVariables(), and Rose::StringUtility::plural().

◆ vertexFlowGraphs() [1/2]

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 235 of file TaintedFlow.h.

◆ vertexFlowGraphs() [2/2]

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 239 of file TaintedFlow.h.

References Rose::BinaryAnalysis::DataFlow::getUniqueVariables(), and Rose::StringUtility::plural().

◆ variables()

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 254 of file TaintedFlow.h.

◆ stateInstance()

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 264 of file TaintedFlow.h.

References Rose::BinaryAnalysis::TaintedFlow::State::instance().

◆ runToFixedPoint()

template<class CFG >

void Rose::BinaryAnalysis::TaintedFlow::runToFixedPoint	(	const CFG &	cfg,
		size_t	cfgStartVertex,
		const StatePtr &	initialState
	)

inline

Run data flow.

Runs the tainted data flow analysis until it converges to a fixed point.

Definition at line 274 of file TaintedFlow.h.

References Rose::BinaryAnalysis::DataFlow::Engine< Cfg_, State_, TransferFunction_, MergeFunction_, PathFeasibility_ >::getFinalStates(), merge(), Rose::BinaryAnalysis::DataFlow::Engine< Cfg_, State_, TransferFunction_, MergeFunction_, PathFeasibility_ >::name(), Rose::StringUtility::plural(), and Rose::BinaryAnalysis::DataFlow::Engine< Cfg_, State_, TransferFunction_, MergeFunction_, PathFeasibility_ >::runToFixedPoint().

◆ getFinalState()

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 294 of file TaintedFlow.h.

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

TaintedFlow.h

Description

Classes

Public Types

Public Member Functions

Static Public Member Functions

Member Typedef Documentation

◆ VariableTaint

◆ StatePtr

Member Enumeration Documentation

◆ Taintedness

◆ Approximation

Constructor & Destructor Documentation

◆ TaintedFlow()

Member Function Documentation

◆ merge()

◆ initDiagnostics()

◆ approximation() [1/2]

◆ approximation() [2/2]

◆ smtSolver() [1/2]

◆ smtSolver() [2/2]

◆ computeFlowGraphs()

◆ vertexFlowGraphs() [1/2]

◆ vertexFlowGraphs() [2/2]

◆ variables()

◆ stateInstance()

◆ runToFixedPoint()

◆ getFinalState()