mate_common.models.integration module¶

class mate_common.models.integration.Addr(va: pydantic.types.PositiveInt)¶

Bases: object

A binary address.

Parameters: va (pydantic.types.PositiveInt) –
Return type: None

va: pydantic.types.PositiveInt¶

class mate_common.models.integration.Assertion(location: mate_common.models.integration.Addr, constraint: List[mate_common.models.integration.Constraint] = <factory>)¶

Bases: object

Assertions are used to add constraints during the execution of a program.

These constraints only apply to symbolic values and must be true _after_ the execution of the location.

Parameters

location (mate_common.models.integration.Addr) –
constraint (List[mate_common.models.integration.Constraint]) –

Return type

None

constraint: List[mate_common.models.integration.Constraint]¶

location: mate_common.models.integration.Addr¶

class mate_common.models.integration.ConcreteHeapOOBOptions(fast: bool = True, detector: Literal[<Detector.ConcreteHeapOOB: 'ConcreteHeapOOB'>] = Detector.ConcreteHeapOOB)¶

Bases: mate_common.models.integration.DetectorOptionsBase

A testing detector that creates a case for every OOB access in the heap.

Parameters

fast (bool) –
detector (Literal[<Detector.ConcreteHeapOOB: 'ConcreteHeapOOB'>]) –

Return type

None

detector: Literal[<Detector.ConcreteHeapOOB: 'ConcreteHeapOOB'>] = 'ConcreteHeapOOB'¶

class mate_common.models.integration.Constraint(expr: str, id: List[mate_common.models.integration.SMTIdentifier] = <factory>)¶

Bases: object

Constraint to apply to identifier.

Parameters

expr (str) –
id (List[mate_common.models.integration.SMTIdentifier]) –

Return type

None

expr: str¶

id: List[mate_common.models.integration.SMTIdentifier]¶

class mate_common.models.integration.Decl(name: str, value: str, expr: str)¶

Bases: object

An initial declaration for symbolic variables.

Parameters

name (str) –
value (str) –
expr (str) –

Return type

None

expr: str¶

name: str¶

value: str¶

class mate_common.models.integration.DetectAllPathsOptions(fast: bool = True, detector: Literal[<Detector.DetectAllPaths: 'DetectAllPaths'>] = Detector.DetectAllPaths)¶

Bases: mate_common.models.integration.DetectorOptionsBase

A testing detector that fires when each state terminates.

Parameters

fast (bool) –
detector (Literal[<Detector.DetectAllPaths: 'DetectAllPaths'>]) –

Return type

None

detector: Literal[<Detector.DetectAllPaths: 'DetectAllPaths'>] = 'DetectAllPaths'¶

class mate_common.models.integration.Detector(value)¶

Bases: str, enum.Enum

Supported detectors for Manticore.

See the dwarfcore module for more info.

ConcreteHeapOOB = 'ConcreteHeapOOB'¶

DetectAllPaths = 'DetectAllPaths'¶

UnderconstrainedOOB = 'UnderconstrainedOOB'¶

UninitializedVar = 'UninitializedVariable'¶

UseAfterFree = 'UseAfterFree'¶

VariableBoundsAccess = 'VariableBoundsAccess'¶

class mate_common.models.integration.DetectorOptionsBase(fast: bool = True)¶

Bases: object

Common fields for detector options.

Parameters: fast (bool) –
Return type: None

fast: bool = True¶

class mate_common.models.integration.ExplorationTree(state_id: int, cases: List[mate_common.models.integration.ReachingTestCase] = <factory>, choices: List[Tuple[str, int]] = <factory>, children: List[mate_common.models.integration.ExplorationTree] = <factory>, error_msg: Optional[str] = None)¶

Bases: object

A tree representing exploration choices and containing potential errors detected during program exploration.

Parameters

state_id (int) –
cases (List[mate_common.models.integration.ReachingTestCase]) –
choices (List[Tuple[str, int]]) –
children (List[mate_common.models.integration.ExplorationTree]) –
error_msg (Optional[str]) –

Return type

None

add_state(parent_id: int, state_id: int, choice: Tuple[str, int]) → bool¶

Add a state to the exploration tree.

Return true on success

Parameters

parent_id (int) –
state_id (int) –
choice (Tuple[str, int]) –

Return type

bool

cases: List[mate_common.models.integration.ReachingTestCase]¶

children: List[mate_common.models.integration.ExplorationTree]¶

choices: List[Tuple[str, int]]¶

error_msg: Optional[str] = None¶

get_state(state_id: int) → Optional[mate_common.models.integration.ExplorationTree]¶

Get a state in the exploration tree.

Parameters: state_id (int) –
Return type: Optional[mate_common.models.integration.ExplorationTree]

iter_cases() → Iterable[mate_common.models.integration.ReachingTestCase]¶

Return type: Iterable[mate_common.models.integration.ReachingTestCase]

state_id: int¶

class mate_common.models.integration.Explore(command_line_flags: List[str] = <factory>, concrete_start: str = '', stdin_size: Optional[int] = 256, env: Dict[str, str] = <factory>, detector_options: List[Union[mate_common.models.integration.DetectAllPathsOptions, mate_common.models.integration.VariableBoundsAccessOptions, mate_common.models.integration.UninitializedVarOptions, mate_common.models.integration.UseAfterFreeOptions, mate_common.models.integration.UnderconstrainedOOBOptions, mate_common.models.integration.ConcreteHeapOOBOptions]] = <factory>, timeout: Optional[int] = None)¶

Bases: object

A message that will configure Manticore to explore with an optionally enabled detector without much direction.

Parameters

command_line_flags (List[str]) –
concrete_start (str) –
stdin_size (Optional[int]) –
env (Dict[str, str]) –
detector_options (List[Union[mate_common.models.integration.DetectAllPathsOptions, mate_common.models.integration.VariableBoundsAccessOptions, mate_common.models.integration.UninitializedVarOptions, mate_common.models.integration.UseAfterFreeOptions, mate_common.models.integration.UnderconstrainedOOBOptions, mate_common.models.integration.ConcreteHeapOOBOptions]]) –
timeout (Optional[int]) –

Return type

None

command_line_flags: List[str]¶

concrete_start: str = ''¶

detector_options: List[Union[mate_common.models.integration.DetectAllPathsOptions, mate_common.models.integration.VariableBoundsAccessOptions, mate_common.models.integration.UninitializedVarOptions, mate_common.models.integration.UseAfterFreeOptions, mate_common.models.integration.UnderconstrainedOOBOptions, mate_common.models.integration.ConcreteHeapOOBOptions]]¶

env: Dict[str, str]¶

stdin_size: Optional[int] = 256¶

timeout: Optional[int] = None¶

class mate_common.models.integration.ExploreFunction(command_line_flags: List[str] = <factory>, concrete_start: str = '', stdin_size: Optional[int] = 256, env: Dict[str, str] = <factory>, detector_options: List[Union[mate_common.models.integration.DetectAllPathsOptions, mate_common.models.integration.VariableBoundsAccessOptions, mate_common.models.integration.UninitializedVarOptions, mate_common.models.integration.UseAfterFreeOptions, mate_common.models.integration.UnderconstrainedOOBOptions, mate_common.models.integration.ConcreteHeapOOBOptions]] = <factory>, timeout: Optional[int] = None, target_function: Optional[str] = None, input_constraints: Optional[List[str]] = None, primitive_ptr_policy: Optional[mate_common.models.integration.UnboundedPtrPolicy] = UnboundedPtrPolicy(policy_type=<UnboundedPtrPolicyType.DEFAULT: 'default'>, max_alternatives=3, custom_values=None), complex_ptr_policy: Optional[mate_common.models.integration.UnboundedPtrPolicy] = UnboundedPtrPolicy(policy_type=<UnboundedPtrPolicyType.DEFAULT: 'default'>, max_alternatives=3, custom_values=None))¶

Bases: mate_common.models.integration.Explore

A message that configures Manticore to explore a single function using underconstrained symbolic execution.

Parameters

command_line_flags (List[str]) –
concrete_start (str) –
stdin_size (Optional[int]) –
env (Dict[str, str]) –
detector_options (List[Union[mate_common.models.integration.DetectAllPathsOptions, mate_common.models.integration.VariableBoundsAccessOptions, mate_common.models.integration.UninitializedVarOptions, mate_common.models.integration.UseAfterFreeOptions, mate_common.models.integration.UnderconstrainedOOBOptions, mate_common.models.integration.ConcreteHeapOOBOptions]]) –
timeout (Optional[int]) –
target_function (Optional[str]) –
input_constraints (Optional[List[str]]) –
primitive_ptr_policy (Optional[mate_common.models.integration.UnboundedPtrPolicy]) –
complex_ptr_policy (Optional[mate_common.models.integration.UnboundedPtrPolicy]) –

Return type

None

complex_ptr_policy: Optional[mate_common.models.integration.UnboundedPtrPolicy] = UnboundedPtrPolicy(policy_type=<UnboundedPtrPolicyType.DEFAULT: 'default'>, max_alternatives=3, custom_values=None)¶

input_constraints: Optional[List[str]] = None¶

primitive_ptr_policy: Optional[mate_common.models.integration.UnboundedPtrPolicy] = UnboundedPtrPolicy(policy_type=<UnboundedPtrPolicyType.DEFAULT: 'default'>, max_alternatives=3, custom_values=None)¶

target_function: Optional[str] = None¶

class mate_common.models.integration.ExploreRet(path: str, exploration_tree: Optional[mate_common.models.integration.ExplorationTree] = None, cases: List[mate_common.models.integration.ReachingTestCase] = <factory>, warnings: List[str] = <factory>)¶

Bases: object

Results message after processing of an Explore message.

Parameters

path (str) –
exploration_tree (Optional[mate_common.models.integration.ExplorationTree]) –
cases (List[mate_common.models.integration.ReachingTestCase]) –
warnings (List[str]) –

Return type

None

cases: List[mate_common.models.integration.ReachingTestCase]¶

exploration_tree: Optional[mate_common.models.integration.ExplorationTree] = None¶

path: str¶

warnings: List[str]¶

class mate_common.models.integration.FreeUseInfo(use_file: str, use_line: int, free_file: str, free_line: int)¶

Bases: object

Use and free filename(s) and line numbers for input into use after free detection.

Parameters

use_file (str) –
use_line (int) –
free_file (str) –
free_line (int) –

Return type

None

free_file: str¶

free_line: int¶

use_file: str¶

use_line: int¶

class mate_common.models.integration.FunctionVariableInfo(function_name: str, variable_name: str)¶

Bases: object

Targeted function and variable name for input to uninitialized stack-variable use detection.

Parameters

function_name (str) –
variable_name (str) –

Return type

None

function_name: str¶

variable_name: str¶

class mate_common.models.integration.Model(python_code: str)¶

Bases: object

Replacement Model for a piece of native code, like a function.

Parameters: python_code (str) –
Return type: None

python_code: str¶

class mate_common.models.integration.ORMConfig¶

Bases: object

orm_mode = True¶

class mate_common.models.integration.Reachability(command_line_flags: List[str] = <factory>, concrete_start: str = '', stdin_size: Optional[int] = 256, env: Dict[str, str] = <factory>, detector_options: List[Union[mate_common.models.integration.DetectAllPathsOptions, mate_common.models.integration.VariableBoundsAccessOptions, mate_common.models.integration.UninitializedVarOptions, mate_common.models.integration.UseAfterFreeOptions, mate_common.models.integration.UnderconstrainedOOBOptions, mate_common.models.integration.ConcreteHeapOOBOptions]] = <factory>, timeout: Optional[int] = None, waypoints: List[mate_common.models.integration.Waypoint] = <factory>, constraint_vars: List[mate_common.models.integration.Decl] = <factory>)¶

Bases: mate_common.models.integration.Explore

Reachability message is the top-level message that represents constraints for POIs.

Parameters

command_line_flags (List[str]) –
concrete_start (str) –
stdin_size (Optional[int]) –
env (Dict[str, str]) –
detector_options (List[Union[mate_common.models.integration.DetectAllPathsOptions, mate_common.models.integration.VariableBoundsAccessOptions, mate_common.models.integration.UninitializedVarOptions, mate_common.models.integration.UseAfterFreeOptions, mate_common.models.integration.UnderconstrainedOOBOptions, mate_common.models.integration.ConcreteHeapOOBOptions]]) –
timeout (Optional[int]) –
waypoints (List[mate_common.models.integration.Waypoint]) –
constraint_vars (List[mate_common.models.integration.Decl]) –

Return type

None

constraint_vars: List[mate_common.models.integration.Decl]¶

waypoints: List[mate_common.models.integration.Waypoint]¶

class mate_common.models.integration.ReachabilityRet(path: str, exploration_tree: Optional[mate_common.models.integration.ExplorationTree] = None, cases: List[mate_common.models.integration.ReachingTestCase] = <factory>, warnings: List[str] = <factory>, success: bool = False)¶

Bases: mate_common.models.integration.ExploreRet

Results message after processing of the Reachability message.

Parameters

path (str) –
exploration_tree (Optional[mate_common.models.integration.ExplorationTree]) –
cases (List[mate_common.models.integration.ReachingTestCase]) –
warnings (List[str]) –
success (bool) –

Return type

None

success: bool = False¶

class mate_common.models.integration.ReachingInput(name: str, symbolic_values: List[mate_common.models.integration.ReachingValue] = <factory>)¶

Bases: object

Information about symbolic input that has reached a destination of importance within the program during execution.

Each input has an associated name in Manticore that gives some insight on its origin.

Parameters

name (str) –
symbolic_values (List[mate_common.models.integration.ReachingValue]) –

Return type

None

name: str¶

symbolic_values: List[mate_common.models.integration.ReachingValue]¶

class mate_common.models.integration.ReachingTestCase(description: str, detector_triggered: Optional[mate_common.models.integration.Detector] = None, symbolic_inputs: List[mate_common.models.integration.ReachingInput] = <factory>)¶

Bases: object

A summary of a set of inputs and description that have been saved for replay on a binary.

description is human-readable free-form text that gives insight on what Manticore detected.

Parameters

description (str) –
detector_triggered (Optional[mate_common.models.integration.Detector]) –
symbolic_inputs (List[mate_common.models.integration.ReachingInput]) –

Return type

None

description: str¶

detector_triggered: Optional[mate_common.models.integration.Detector] = None¶

symbolic_inputs: List[mate_common.models.integration.ReachingInput]¶

class mate_common.models.integration.ReachingValue(symbolic_value: str, concrete_value_base64: str)¶

Bases: object

A symbolic representation of the reaching input and a single, concrete, base64-encoded value.

Parameters

symbolic_value (str) –
concrete_value_base64 (str) –

Return type

None

concrete_value_base64: str¶

symbolic_value: str¶

class mate_common.models.integration.Register(value)¶

Bases: str, enum.Enum

Registers for machine-code. Must match up with what appears in the binary.

NOTE: If there is a better way of normalizing the register names, we might not need this.

RIP = 'RIP'¶

class mate_common.models.integration.Replacement(location: mate_common.models.integration.Addr, model: mate_common.models.integration.Model)¶

Bases: object

A replacement for a function call. A “replacement” will intercept control-flow to replace the logic at the specified location. If it will replace a function call, then the location should appear at the very first instruction within the function that is being replaced (to catch all calls). The model will then need to return control-flow back to the caller using standard calling convention rules.

NOTE: This has yet to be implemented or tested.

These are added _before_ the execution of location

Parameters

location (mate_common.models.integration.Addr) –
model (mate_common.models.integration.Model) –

Return type

None

location: mate_common.models.integration.Addr¶

model: mate_common.models.integration.Model¶

class mate_common.models.integration.SMTIdentifier(identifier: Union[mate_common.models.integration.Register, str])¶

Bases: object

Identifier for SMT expressions.

Parameters: identifier (Union[mate_common.models.integration.Register, str]) –
Return type: None

identifier: Union[mate_common.models.integration.Register, str]¶

class mate_common.models.integration.Target(event: str, id: str, type: str = 'target')¶

Bases: object

Parameters

event (str) –
id (str) –
type (str) –

Return type

None

event: str¶

id: str¶

type: str = 'target'¶

class mate_common.models.integration.UnboundedPtrPolicy(policy_type: mate_common.models.integration.UnboundedPtrPolicyType = UnboundedPtrPolicyType.DEFAULT, max_alternatives: int = 3, custom_values: Optional[List[int]] = None)¶

Bases: object

Policy for handling unbounded pointers in under-constrained Manticore.

Parameters

policy_type (mate_common.models.integration.UnboundedPtrPolicyType) –
max_alternatives (int) –
custom_values (Optional[List[int]]) –

Return type

None

custom_values: Optional[List[int]] = None¶

max_alternatives: int = 3¶

policy_type: mate_common.models.integration.UnboundedPtrPolicyType = 'default'¶

class mate_common.models.integration.UnboundedPtrPolicyType(value)¶

Bases: str, enum.Enum

Strategy for handling unbounded pointers.

CUSTOM = 'custom'¶

DEFAULT = 'default'¶

class mate_common.models.integration.UnderconstrainedOOBOptions(fast: bool = True, detector: Literal[<Detector.UnderconstrainedOOB: 'UnderconstrainedOOB'>] = Detector.UnderconstrainedOOB)¶

Bases: mate_common.models.integration.DetectorOptionsBase

A testing detector that creates a case for every OOB access in underconstrained symex.

Parameters

fast (bool) –
detector (Literal[<Detector.UnderconstrainedOOB: 'UnderconstrainedOOB'>]) –

Return type

None

detector: Literal[<Detector.UnderconstrainedOOB: 'UnderconstrainedOOB'>] = 'UnderconstrainedOOB'¶

class mate_common.models.integration.UnderconstrainedTestCase(description: str, detector_triggered: Optional[mate_common.models.integration.Detector] = None, symbolic_inputs: List[mate_common.models.integration.ReachingInput] = <factory>, uid: int = -1, va: int = -1, va_mapping: Optional[str] = None, condition: Optional[str] = None, constraints: List[str] = <factory>)¶

Bases: mate_common.models.integration.ReachingTestCase

A test case generated by under-constrained Manticore.

Parameters

description (str) –
detector_triggered (Optional[mate_common.models.integration.Detector]) –
symbolic_inputs (List[mate_common.models.integration.ReachingInput]) –
uid (int) –
va (int) –
va_mapping (Optional[str]) –
condition (Optional[str]) –
constraints (List[str]) –

Return type

None

condition: Optional[str] = None¶

constraints: List[str]¶

uid: int = -1¶

va: int = -1¶

va_mapping: Optional[str] = None¶

class mate_common.models.integration.UninitializedVarOptions(fast: bool = True, detector: Literal[<Detector.UninitializedVar: 'UninitializedVariable'>] = <Detector.UninitializedVar: 'UninitializedVariable'>, poi_info: List[mate_common.models.integration.FunctionVariableInfo] = <factory>)¶

Bases: mate_common.models.integration.DetectorOptionsBase

Parameters

fast (bool) –
detector (Literal[<Detector.UninitializedVar: 'UninitializedVariable'>]) –
poi_info (List[mate_common.models.integration.FunctionVariableInfo]) –

Return type

None

detector: Literal[<Detector.UninitializedVar: 'UninitializedVariable'>] = 'UninitializedVariable'¶

poi_info: List[mate_common.models.integration.FunctionVariableInfo]¶

class mate_common.models.integration.UseAfterFreeOptions(fast: bool = True, detector: Literal[<Detector.UseAfterFree: 'UseAfterFree'>] = <Detector.UseAfterFree: 'UseAfterFree'>, poi_info: List[mate_common.models.integration.FreeUseInfo] = <factory>)¶

Bases: mate_common.models.integration.DetectorOptionsBase

Parameters

fast (bool) –
detector (Literal[<Detector.UseAfterFree: 'UseAfterFree'>]) –
poi_info (List[mate_common.models.integration.FreeUseInfo]) –

Return type

None

detector: Literal[<Detector.UseAfterFree: 'UseAfterFree'>] = 'UseAfterFree'¶

poi_info: List[mate_common.models.integration.FreeUseInfo]¶

class mate_common.models.integration.VariableBoundsAccessOptions(fast: bool = True, detector: Literal[<Detector.VariableBoundsAccess: 'VariableBoundsAccess'>] = <Detector.VariableBoundsAccess: 'VariableBoundsAccess'>, poi_info: List[str] = <factory>)¶

Bases: mate_common.models.integration.DetectorOptionsBase

Parameters

fast (bool) –
detector (Literal[<Detector.VariableBoundsAccess: 'VariableBoundsAccess'>]) –
poi_info (List[str]) –

Return type

None

detector: Literal[<Detector.VariableBoundsAccess: 'VariableBoundsAccess'>] = 'VariableBoundsAccess'¶

poi_info: List[str]¶

class mate_common.models.integration.Waypoint(start: mate_common.models.integration.Addr, end: mate_common.models.integration.Addr, asserts: List[mate_common.models.integration.Assertion] = <factory>, replacements: List[mate_common.models.integration.Replacement] = <factory>)¶

Bases: object

Waypoint message relates to a specific area of code and contains relevant information for that area.

Parameters

start (mate_common.models.integration.Addr) –
end (mate_common.models.integration.Addr) –
asserts (List[mate_common.models.integration.Assertion]) –
replacements (List[mate_common.models.integration.Replacement]) –

Return type

None

asserts: List[mate_common.models.integration.Assertion]¶

end: mate_common.models.integration.Addr¶

replacements: List[mate_common.models.integration.Replacement]¶

start: mate_common.models.integration.Addr¶