angr.analyses.veritesting

exception angr.analyses.veritesting.VeritestingError

Bases: Exception

class angr.analyses.veritesting.CallTracingFilter

Bases: object

Filter to apply during CFG creation on a given state and jumpkind to determine if it should be skipped at a certain depth

whitelist = {<class 'angr.procedures.cgc.receive.receive'>, <class 'angr.procedures.cgc.transmit.transmit'>, <class 'angr.procedures.glibc.__ctype_b_loc.__ctype_b_loc'>, <class 'angr.procedures.libc.atoi.atoi'>, <class 'angr.procedures.libc.fgetc.fgetc'>, <class 'angr.procedures.libc.strcmp.strcmp'>, <class 'angr.procedures.libc.strlen.strlen'>, <class 'angr.procedures.posix.read.read'>}
cfg_cache = {}
__init__(project, depth, blacklist=None)
filter(call_target_state, jumpkind)

The call will be skipped if it returns True.

Parameters:

  • call_target_state – The new state of the call target.

  • jumpkind – The Jumpkind of this call.

Returns:

True if we want to skip this call, False otherwise.

class angr.analyses.veritesting.Veritesting

Bases: Analysis

An exploration technique made for condensing chunks of code to single (nested) if-then-else constraints via CFG accurate to conduct Static Symbolic Execution SSE (conversion to single constraint)

cfg_cache = {}
all_stashes = ('successful', 'errored', 'deadended', 'deviated', 'unconstrained')
__init__(input_state, boundaries=None, loop_unrolling_limit=10, enable_function_inlining=False, terminator=None, deviation_filter=None)

SSE stands for Static Symbolic Execution, and we also implemented an extended version of Veritesting (Avgerinos, Thanassis, et al, ICSE 2014).

Parameters:

  • input_state – The initial state to begin the execution with.

  • boundaries – Addresses where execution should stop.

  • loop_unrolling_limit – The maximum times that Veritesting should unroll a loop for.

  • enable_function_inlining – Whether we should enable function inlining and syscall inlining.

  • terminator – A callback function that takes a state as parameter. Veritesting will terminate if this function returns True.

  • deviation_filter – A callback function that takes a state as parameter. Veritesting will put the state into “deviated” stash if this function returns True.

is_not_in_cfg(s)

Returns if s.addr is not a proper node in our CFG.

Parameters:

s (SimState) – The SimState instance to test.

Returns bool:

False if our CFG contains p.addr, True otherwise.

is_overbound(state)

Filter out all states that run out of boundaries or loop too many times.

param SimState state: SimState instance to check returns bool: True if outside of mem/loop_ctr boundary