mantiserve.mantireach module

This module contains all of the handling for orchestrating the contents of a Reachability message into a symbolic execution plan for Manticore to execute.

class mantiserve.mantireach.ConstraintValidationErrorInfo(err_msg: Union[str, List[str]], expr: str)

Bases: mantiserve.mantireach.ValidationErrorInfo

Validation error information for constraints.

Parameters

  • err_msg (Union[str, List[str]]) –

  • expr (str) –

Return type

None

expr: str
class mantiserve.mantireach.HookInfo(pc: int, callback: Callable[[manticore.native.state.State], None], after: bool)

Bases: object

Information required to keep track of hooks added.

These are also the order in which the arguments appear to add_hook and remove_hook

Parameters

  • pc (int) –

  • callback (Callable[[manticore.native.state.State], None]) –

  • after (bool) –

Return type

None

after: bool
callback: Callable[[manticore.native.state.State], None]
pc: int
class mantiserve.mantireach.ValidationErrorInfo(err_msg: Union[str, List[str]])

Bases: object

General validation error information.

Parameters

err_msg (Union[str, List[str]]) –

Return type

None

err_msg: Union[str, List[str]]
class mantiserve.mantireach.WaypointInfo(va_start: int, va_end: int, init_hook: mantiserve.mantireach.HookInfo, hooks: FrozenSet[mantiserve.mantireach.HookInfo], deinit_hook: mantiserve.mantireach.HookInfo)

Bases: object

Information that Manticore should know about Waypoints to add and remove assertion hooks as they are encountered.

Parameters
Return type

None

property all_hooks: FrozenSet[mantiserve.mantireach.HookInfo]
deinit_hook: mantiserve.mantireach.HookInfo
hooks: FrozenSet[mantiserve.mantireach.HookInfo]
init_hook: mantiserve.mantireach.HookInfo
va_end: int
va_start: int
mantiserve.mantireach.add_assertion(assertions: List[Callable[[manticore.native.state.State], manticore.core.smtlib.expression.Bool]], state: manticore.native.state.State) → None

Add all assertions in the list to the Manticore State.

Parameters

  • assertions – Assertions to be added to the State

  • state – The Manticore State that will take the assertions

  • assertions (List[Callable[[manticore.native.state.State], manticore.core.smtlib.expression.Bool]]) –

  • state (manticore.native.state.State) –

Return type

None

mantiserve.mantireach.assertion_hook_callback_factory(assertions: List[Callable[[manticore.native.state.State], manticore.core.smtlib.expression.Bool]]) → Callable[[manticore.native.state.State], None]

Given a stateful assertion, create a callback that will add that assertion to Manticore’s state.

Parameters

  • assertions – Assertions to be added to a Manticore State

  • assertions (List[Callable[[manticore.native.state.State], manticore.core.smtlib.expression.Bool]]) –

Returns

A function that can be used with a Manticore state to add the assertions

Return type

Callable[[manticore.native.state.State], None]

mantiserve.mantireach.build_assertion_expr(constraint_msg: mate_common.models.integration.Constraint) → Callable[[manticore.native.state.State], manticore.core.smtlib.expression.Bool]

Build a Manticore-compatible StatefulAssertion.

Parameters
Returns

An assertion expression that can be used with a Manticore state

Return type

Callable[[manticore.native.state.State], manticore.core.smtlib.expression.Bool]

mantiserve.mantireach.call_funcs(arg: mantiserve.mantireach.T, funcs: List[Callable[[mantiserve.mantireach.T], None]]) → None

Call all functions given and pass arg to each one. Ignores output of functions.

Parameters

  • arg – Argument to pass to functions

  • funcs – List of functions to call

  • arg (mantiserve.mantireach.T) –

  • funcs (List[Callable[[mantiserve.mantireach.T], None]]) –

Return type

None

mantiserve.mantireach.combine_hooks(hooks: Iterable[Callable[[manticore.native.state.State], None]]) → Callable[[manticore.native.state.State], None]

Combine hooks by calling them one after another in the order provided.

Parameters

  • hooks – The hooks to combine

  • hooks (Iterable[Callable[[manticore.native.state.State], None]]) –

Returns

A function that will call all hooks

Return type

Callable[[manticore.native.state.State], None]

mantiserve.mantireach.convert_identifier(identifier_p: mate_common.models.integration.SMTIdentifier) → Callable[[manticore.native.state.State], Tuple[str, manticore.core.smtlib.expression.Expression]]

Build a function that will obtain an identifier’s value using a Manticore State.

Parameters
Returns

Partial function that can be used to get the run-time value of the identifier given a Manticore state

Return type

Callable[[manticore.native.state.State], Tuple[str, manticore.core.smtlib.expression.Expression]]

mantiserve.mantireach.deinit_hook(state: manticore.native.state.State) → None

Hook at the end address of the waypoint. Removes all hooks from this waypoint.

Parameters

  • state – The state we want to deinitialize the hook

  • state (manticore.native.state.State) –

Return type

None

mantiserve.mantireach.do_expr_replace(smt_replacements, constraint_msg: mate_common.models.integration.Constraint, state: manticore.native.state.State) → manticore.core.smtlib.expression.Bool

Match up our replacement identifiers $replace#0, $replace#1, … with our actual replacements, and form a Python expression, which we can then return.

Parameters

  • smt_replacements – The values we want to insert the constraint

  • constraint_msg_p – The constraint to place on the Manticore state

  • state – The Manticore State this replacement relates to

  • constraint_msg (mate_common.models.integration.Constraint) –

  • state (manticore.native.state.State) –

Returns

An assertion expression placed on the Manticore state with replacements

Return type

manticore.core.smtlib.expression.Bool

mantiserve.mantireach.generate_hook_waypoint_assertions(waypoint: mate_common.models.integration.Waypoint) → mantiserve.mantireach.WaypointInfo

Given a list of assertions, create a hook for manticore that will apply the constraints _after_ the instruction has executed.

Parameters
Returns

Information about the waypoint and hooks to add to Manticore

Return type

mantiserve.mantireach.WaypointInfo

mantiserve.mantireach.init_hook(state: manticore.native.state.State) → None

Hook at the beginning address of the waypoint. Initializes all other hooks in the waypoint.

Parameters

  • state – The state we want to initialize the hook

  • state (manticore.native.state.State) –

Return type

None

mantiserve.mantireach.last_block_solve(state: manticore.native.state.State) → None

Hook for the last basic block/Waypoint on the list used to generate ReachingInput message that is saved in Manticore context.

Parameters

  • state – Manticore state for context

  • state (manticore.native.state.State) –

Return type

None

mantiserve.mantireach.manticore_reach(bin_path: pathlib.Path, session: mate_query.db.Session, graph: mate_query.db.Graph, ctxt: argparse.Namespace, msg: mate_common.models.integration.Reachability, *, manticore_workspace: Optional[str] = None) → mate_common.models.integration.ReachabilityRet

Determine whether Manticore can follow the given Reachability message.

Parameters
Returns

Reachability Return message with details of Manticore run

Return type

mate_common.models.integration.ReachabilityRet

mantiserve.mantireach.natural_sort_key(s, _nsre=re.compile('([0-9]+)'))

String natural sort for strings that include numbers.

https://stackoverflow.com/a/16090640

mantiserve.mantireach.setup_next_waypoint(state: manticore.native.state.State) → None

Grab the next waypoint and setup a hook to initialize it when the start address is hit.

Parameters

  • state – The state we want to setup the next waypoint on

  • state (manticore.native.state.State) –

Return type

None

mantiserve.mantireach.stateful_id_expr(identifier: mate_common.models.integration.SMTIdentifier, state: manticore.native.state.State) → Tuple[str, manticore.core.smtlib.expression.Expression]

Use run-time information from Manticore state to retrieve value of the SMT identifier.

Parameters
Returns

The identifier and its value

Return type

Tuple[str, manticore.core.smtlib.expression.Expression]

mantiserve.mantireach.validate_reachability_msg(reach_msg: mate_common.models.integration.Reachability) → List[mantiserve.mantireach.ValidationErrorInfo]

Validate the well-formed-ness of the Reachability message before Manticore processes it.

Parameters
Returns

a list of errors if there are any.

Return type

List[mantiserve.mantireach.ValidationErrorInfo]