' + + '' + + _("Hide Search Matches") + + "
" + ) + ); + }, + + /** + * helper function to hide the search marks again + */ + hideSearchWords: () => { + document + .querySelectorAll("#searchbox .highlight-link") + .forEach((el) => el.remove()); + document + .querySelectorAll("span.highlighted") + .forEach((el) => el.classList.remove("highlighted")); + localStorage.removeItem("sphinx_highlight_terms") + }, + + initEscapeListener: () => { + // only install a listener if it is really needed + if (!DOCUMENTATION_OPTIONS.ENABLE_SEARCH_SHORTCUTS) return; + + document.addEventListener("keydown", (event) => { + // bail for input elements + if (BLACKLISTED_KEY_CONTROL_ELEMENTS.has(document.activeElement.tagName)) return; + // bail with special keys + if (event.shiftKey || event.altKey || event.ctrlKey || event.metaKey) return; + if (DOCUMENTATION_OPTIONS.ENABLE_SEARCH_SHORTCUTS && (event.key === "Escape")) { + SphinxHighlight.hideSearchWords(); + event.preventDefault(); + } + }); + }, +}; + +_ready(() => { + /* Do not call highlightSearchWords() when we are on the search page. + * It will highlight words from the *previous* search query. + */ + if (typeof Search === "undefined") SphinxHighlight.highlightSearchWords(); + SphinxHighlight.initEscapeListener(); +}); diff --git a/autoapi/cozy/__main__/index.html b/autoapi/cozy/__main__/index.html new file mode 100644 index 0000000..522561b --- /dev/null +++ b/autoapi/cozy/__main__/index.html @@ -0,0 +1,459 @@ + + + + + + + +| + | + |
| + | Generic enumeration. |
+
| + | + |
Bases: enum.Enum
Generic enumeration.
+Derive from this class to define new enumerations.
+Bases: textual.app.App
"""
+ Screen {
+ padding:1
+ }
+ """
+| + | + |
| + | For a field to be equal, all subcomponents of the body must be equal. In this case, left_body and right_body |
+
| + | A not equal leaf is a field that cannot be further unpacked/traversed. |
+
| + | For a field to be not equal, there must be at least one subcomponent of the body that was not equal. In this case, |
+
| + | + |
| + | StateDiff encapsulates the memoized state used by the difference method. This class is used internally by Comparison and is typically not for external use. |
+
| + | Stores information about comparing two compatible states. |
+
| + | This class stores all compatible pairs and orphaned states. An orphan state is one in which there is no compatible state in the other execution tree. In most scenarios there will be no orphaned states. |
+
|
++ |
|
++ |
|
++ |
|
+This function attempts to create a human understandable name for an address, or returns None if it can't figure |
+
|
++ |
|
+Recursively transforms all integers in a Python datastructure (that is mappable with functools_ext.fmap) to hex strings. |
+
This function attempts to create a human understandable name for an address, or returns None if it can’t figure +one out.
+Bases: FieldDiff
For a field to be equal, all subcomponents of the body must be equal. In this case, left_body and right_body +should not hold any further FieldDiffs within themselves. Rather left_body and right_body should be the entire +fields for which differencing was checked (and it was determined that all subfields are equal).
+Bases: FieldDiff
A not equal leaf is a field that cannot be further unpacked/traversed.
+Bases: FieldDiff
For a field to be not equal, there must be at least one subcomponent of the body that was not equal. In this case, +body_diff will hold further FieldDiffs within itself. Equal subfields of the bodies will be +represented by EqFieldDiff, whereas unequal subfields will be represented by further nested NotEqFieldDiff.
+StateDiff encapsulates the memoized state used by the difference method. This class is used internally by Comparison and is typically not for external use.
+Compares two states to find differences in memory. This function will return None if the two states have non-intersecting inputs. Otherwise, it will return a dict of addresses and a dict of registers which are different between the two. This function is based off of angr.analyses.congruency_check.CongruencyCheck().compare_states, but has been customized for our purposes. Note that this function may use memoization to enhance performance.
+sl (SimState) – The first state to compare
sr (SimState) – The second state to compare
ignore_addrs (collections.abc.Iterable[range] | None) – Memory addresses to ignore when doing the memory diffing. This representation is more efficient than a set of integers since the ranges involved can be quite large.
compute_mem_diff (bool) – If this flag is True, then we will diff the memory. If this is false, then the first element of the return tuple will be None.
compute_reg_diff (bool) – If this flag is True, then we will diff the registers. If this is false, then the second element of the return tuple will be None.
use_unsat_core (bool) – If this flag is True, then we will use unsat core optimization to speed up comparison of pairs of states. This option may cause errors in Z3, so disable if this occurs.
None if the two states are not compatible, otherwise returns an object containing the memory, register differences, and side effect differences.
+DiffResult | None
+Recursively transforms all integers in a Python datastructure (that is mappable with functools_ext.fmap) to hex strings.
+val0 – The datastructure to traverse.
+A deep copy of the datastructure, with all integers converted to hex strings.
+Stores information about comparing two compatible states.
+state_left (TerminalState) – Information pertaining specifically to the pre-patched state being compared.
state_right (TerminalState) – Information pertaining specifically to the post-patched state being compared.
mem_diff (dict[range, tuple[claripy.ast.Base, claripy.ast.Base]]) – Maps memory addresses to pairs of claripy ASTs, where the left element of the tuple is the data in memory for state_left, and the right element of the tuple is what was found in memory for state_right. Only memory locations that are different are saved in this dict.
reg_diff (dict[str, tuple[claripy.ast.Base, claripy.ast.Base]]) – Similar to mem_diff, except that the dict is keyed by register names. Note that some registers may be subparts of another. For example in x64, EAX is a subregister of RAX.
side_effect_diff (dict[str, list[tuple[PerformedSideEffect | None, PerformedSideEffect | None, FieldDiff]]]) – Maps side effect channels to a list of 3 element tuples, where the first element is the performed side effect from the left binary, the second element is the performed side effect from the right binary, and the third element is the diff between the body of the side effects.
mem_diff_ip (dict[int, tuple[frozenset[claripy.ast.Base]], frozenset[claripy.ast.Base]]) – Maps memory addresses to a set of instruction pointers that the program was at when it wrote that byte in memory. In most cases the frozensets will have a single element, but this may not be the case in the scenario where a symbolic value determined the write address.
compare_std_out (bool) – If True then we should consider stdout when checking if the two input states are equal.
compare_std_err (bool) – If True then we should consider stderr when checking if the two input states are equal.
Determines if the two compatible states are observationally equal. That is, they contain the same memory contents, registers, stdout, and stderr after execution.
+True if the two compatible states are observationally equal, and False otherwise.
+bool
+Concretizes the arguments used to put the program in these states by jointly using the constraints attached to the compatible states.
+args (any) – The input arguments to concretize. This argument may be a Python datastructure, the concretizer will make a deep copy with claripy symbolic variables replaced with concrete values.
num_examples (int) – The maximum number of concrete examples to generate for this particular pair.
A list of concrete inputs that satisfy both constraints attached to the states.
+list[CompatiblePairInput]
+This class stores all compatible pairs and orphaned states. An orphan state is one in which there is no compatible state in the other execution tree. In most scenarios there will be no orphaned states.
+pairs (dict[tuple[SimState, SimState], CompatiblePair]) – pairs stores a dictionary that maps a pair of (pre_patch_state, post_patch_state) compatible states to their comparison information
orphans_left (set[TerminalState]) – Pre-patched states for which there are 0 corresponding compatible states in the post-patch
orphans_right (set[TerminalState]) – Post-patched states for which there are 0 corresponding compatible states in the pre-patch
Compares a bundle of pre-patched states with a bundle of post-patched states.
+pre_patched (project.RunResult) – The pre-patched state bundle
post_patched (project.RunResult) – The post-patched state bundle
ignore_addrs (list[range] | None) – A list of addresses ranges to ignore when comparing memory.
ignore_invalid_stack (bool) – If this flag is True, then memory differences in locations previously occupied by the stack are ignored.
compare_memory (bool) – If True, then the analysis will compare locations in the program memory.
compare_registers (bool) – If True, then the analysis will compare registers used by the program.
compare_side_effects (bool) – If True, then the analysis will compare side effects outputted by the program.
compare_std_out (bool) – If True, then the analysis will save stdout written by the program in the results. Note that angr currently concretizes values written to stdout, so these values will be binary strings.
compare_std_err (bool) – If True, then the analysis will save stderr written by the program in the results.
use_unsat_core (bool) – If this flag is True, then we will use unsat core optimization to speed up comparison of pairs of states. This option may cause errors in Z3, so disable if this occurs.
simplify (bool) – If this flag is True, then symbolic memory and register differences will be simplified as much as possible. This flag is typically only necessary if you want to do some deep inspection of symbolic contents. simplify can speed things down a lot, and symbolic expressions are usually very complex to the point where they are not easily understandable. This is why in most scenarios the flag should be left as False.
Retrieves a CompatiblePair given two compatible input states.
+state_left (SimState) – The pre-patched state
state_right (SimState) – The post-patched state
The CompatiblePair object corresponding to this compatible state pair.
+Returns True when the two input states are compatible based on the pairs stored in this object, and False otherwise.
+state_left (SimState) – The pre-patched state
state_right (SimState) – The post-patched state
True if the input states are compatible, and False otherwise
+bool
+Iterates over compatible pairs stored in the comparison.
+An iterator over compatible pairs.
+Iterator[CompatiblePair]
+Determines what compatible state pairs are valid with respect to a verification assertion. Note that the comparison results are verified with respect to the verification_assertion if the returned list is empty (has length 0).
+verification_assertion (Callable[[CompatiblePair], claripy.ast.Base | bool]) – A function which takes in a compatible pair and returns a claripy expression which must be satisfiable for all inputs while under the joint constraints of the state pair. Alternatively the function can return a bool. If the return value is False, this will be considered a verification failure. If the return value is True, this will be considered a verification success.
+A list of all compatible pairs for which there was a concrete input that caused the verification assertion to fail.
+list[CompatiblePair]
+Generates a human-readable report of the result object, saved as a string. This string is suitable for printing.
+args (any) – The symbolic/concolic arguments used during exeuction, here these args are concretized so that we can give examples of concrete input.
concrete_post_processor (Callable[[any], any] | None) – This function is used to post-process concretized versions of args before they are added to the return string. Some examples of this function include converting an integer to a negative number due to use of two’s complement, or slicing off parts of the argument based on another part of the input arguments.
num_examples (int) – The number of concrete examples to show the user.
A human-readable summary of the comparison.
+str
+
|
+Simplifies a claripy AST expression, given some knowledge base (kb) of information |
+
|
++ |
|
++ |
Simplifies a claripy AST expression, given some knowledge base (kb) of information
+expr (claripy.ast.bits) – The expression to simplify
kb (claripy.ast.Bool) – The knowledge base which is used to simplify the expr. This is typically a series of equalities conjoined together.
A simplified version of the input expression, or the original expression if no simplification occurred.
+claripy.ast.bits
+| + | This class implements concolic execution without using an external emulator |
+
| + | Generic enumeration. |
+
| + | Jointly runs two SimulationManager objects by concretizing symbols, then running the left and right simulations |
+
Bases: angr.ExplorationTechnique
This class implements concolic execution without using an external emulator
+like QEMU or Unicorn. This class functions by storing a concrete assignment
+for each symbolic variable. When the state branches, the assignment is
+substituted into both children’s constraints. If the substitution results
+in the constraints evaluating to false, that child is placed in the deferred
+stash. By querying the simulation manager’s active stash length, we can
+tell when the concrete execution ends. When concrete execution ends, we
+can either choose a new concrete substitution ourselves and set it with
+the ConcolicDeferred.set_concrete() method. Alternatively we
+can take one of the deferred states and generate and autogenerate a new
+concrete substitution by finding a satisfying assignment for that state’s
+constraints.
ConcolicSim constructor
+concrete_init (dict[claripy.BVS, claripy.BVV] | set[claripy.BVS] | frozenset[claripy.BVS]) – Used to initialize the concrete value. If this value is a substitution dictionary, then that dictionary is used as our concrete input. If this value is a set or frozenset, then a substituting dictionary is autogenerated, subject to the initial state’s constraints.
deferred_stash (string) – The name of the deferred stash
check_only_recent_constraints (bool) – If this value is true, then whenever child states are created, only the new constraints are checked with respect to the concrete substitution. Here we assume that the parent of the child already satisfied the concrete input on a previous iteration, so it’s safe to only check with respect to the new constraints.
Substitutes the current concrete input into the constraints, and returns True if the constraints are True after +the substitution is made.
+constraints (list[claripy.ast.bool]) – The constraints in which the concrete solution will be substituted.
+bool
+If the constraints are True after substitution, then True is returned. Otherwise returns False.
+Sets the concrete input via a substitution dictionary. All the symbols used by the program should have concrete +values provided for them. The active and deferred stash will be mutated to ensure that only states which +are satisfied by the concrete substitution are active.
+concrete (dict[claripy.BVS, claripy.BVV]) – A dictionary mapping each symbol to its concrete value.
+Autogenerates a new concrete input by choosing a deferred state and finding a satisfying assignment +with respect to that state’s constraints. The symbols provided will be used to internally generate +a substitution dictionary. The candidate_heuristic is used to choose a state from the current stash +of deferred states. If no heuristic is provided, the last state in the deferred stash will be chosen next. +If there are any active states in the simulation manager, a ValueError will be thrown.
+simgr (angr.SimulationManager) – The simulation manager
symbols (set[claripy.BVS] | frozenset[claripy.BVS]) – The symbols that we will generate a substitution for.
candidate_heuristic (Callable[[list[angr.SimState]], angr.SimState] | None) – The heuristic that should be used to choose the deferred state that should be explored further. Note that this function should mutate its input list (ie, remove the desired state), and return that desired state.
Bases: enum.Enum
Generic enumeration.
+Derive from this class to define new enumerations.
+Jointly runs two SimulationManager objects by concretizing symbols, then running the left and right simulations +with the same concrete input. This joint simulator alternates between the left and right simulations +when generating new concrete inputs.
+simgr_left (SimulationManager) – The first simulation manager to run in concolic execution
simgr_right (SimulationManager) – The second simulation manager to run in concolic execution.
left_explorer (ConcolicSim) – The first exploration method to use for concolic execution. Note that this exploration technique will be attached to the left simulation manager.
right_explorer (ConcolicSim) – The second exploration method to use for concolic execution. Note that this exploration technique will be attached to the right simulation manager.
candidate_heuristic_left (Callable[[list[angr.SimState]], angr.SimState] | None) – The heuristic that should be used to choose the deferred state that should be explored further. Note that this function should mutate its input list (ie, remove the desired state), and return that desired state. Note that some pre-made candidate heuristic techniques can be found in the cozy.concolic.heuristics module.
candidate_heuristic_right (Callable[[list[angr.SimState]], angr.SimState] | None) – The heuristic that should be used to choose the deferred state that should be explored further. Note that this function should mutate its input list (ie, remove the desired state), and return that desired state. Note that some pre-made candidate heuristic techniques can be found in the cozy.concolic.heuristics module.
Explores the simulations given in the left and right simulation manager.
+explore_fun_left (Callable[[SimulationManager], None] | None) – If this parameter is not None, then instead of SimulationManager.explore() being called to do the exploration, we call explore_fun_left instead.
explore_fun_right (Callable[[SimulationManager], None] | None) – If this parameter is not None, then instead of SimulationManager.explore() being called to do the exploration, we call explore_fun_right instead.
termination_fun_left (Callable[[SimulationManager], bool] | None) – Every time we finish exploring one concrete input, this function is called to determine if the exploration should terminate. If both termination functions return True, then exploration is halted and this function returns. If this parameter is None, then the left simulation manager will terminate only when no further exploration is possible (ie, execution is complete). Pre-made termination functions can be found in the cozy.concolic.heuristics module.
termination_fun_right (Callable[[SimulationManager], bool] | None) – Every time we finish exploring one concrete input, this function is called to determine if the exploration should terminate. If both termination functions return True, then exploration is halted and this function returns. If this parameter is None, then the right simulation manager will terminate only when no further exploration is possible (ie, execution is complete). Pre-made termination functions can be found in the cozy.concolic.heuristics module.
loop_bound_left (int | None) – Sets an upper bound on loop iteration count for the left session. Useful for programs with non-terminating loops.
loop_bound_right (int | None) – Sets an upper bound on loop iteration count for the right session. Useful for programs with non-terminating loops.
None
+None
+| + | For use as the candidate heuristic in |
+
| + | For use as the candidate heuristic in |
+
| + | This termination heuristic tells the concolic execution to explore until all states are deadended. |
+
| + | This termination heuristic tells the concolic execution to explore until a certain fraction of a |
+
| + | This termination heuristic tells the concolic execution to explore until a certain number of terminated |
+
For use as the candidate heuristic in cozy.exploration.ConcolicSim.generate_concrete()
+This heuristic will choose the next exploration candidate by popping the last element off the candidate’s list.
For use as the candidate heuristic in cozy.exploration.ConcolicSim.generate_concrete()
+This heuristic will select a candidate whose basic block history has been seen least frequently in the past. This
+class keeps an internal record of candidates it chose in the past to compute this metric.
lookback (int) – The number of basic blocks we should look back to when computing a candidate’s transition history. This should be a small integer, somewhere in the range 1 to 6. This number should in general only be increased if the total number of states we search goes up. The candidate state with the most unique transition history will be chosen by this heuristic.
+This termination heuristic tells the concolic execution to explore until all states are deadended.
+This termination heuristic tells the concolic execution to explore until a certain fraction of a +function’s basic blocks have been visited at least once.
+fun (Function) – The function that we are seeking a specific coverage over.
coverage_fraction (float) – A number in the range [0, 1] that determines what fraction of basic blocks need to be visited before termination is reached.
Constructs a CoverageTermination object from an unrun session.
+sess (Session) – The session which is set to call some specific function, but has not yet been run.
coverage_fraction (float) – A number in the range [0, 1] that determines what fraction of basic blocks need to be visited before termination is reached.
This termination heuristic tells the concolic execution to explore until a certain number of terminated +states are reached. If add_callees is False, then this value is equal to the cyclomatic complexity of the function. +Otherwise, it is equal to the cyclomatic complexity of the function plus the cyclomatic complexity of all callees +of the function (recursively).
+add_callees (bool) – If this parameter is True, the cyclomatic complexity of all functions deeper in the call graph will be summed to determine the maximum number of states to explore. If False, the upper bound will be the cyclomatic complexity of the session.
multiplier (int | float) – The computed cyclomatic complexity sum will be multiplied by this value to determine the number of states to explore
Constructs an object from a session. The session must be started from a specific function.
+add_callees (bool) – If this parameter is True, the cyclomatic complexity of all functions deeper in the call graph will be summed to determine the maximum number of states to explore. If False, the upper bound will be the cyclomatic complexity of the session.
multiplier (int | float) – The computed cyclomatic complexity sum will be multiplied by this value to determine the number of states to explore
| + | This class is used for jointly running two sessions using concolic execution. The sessions need to be run |
+
This class is used for jointly running two sessions using concolic execution. The sessions need to be run +jointly because the concrete values generated during concolic execution need to be fed to both programs.
+Jointly run two sessions.
+args_left (list[claripy.ast.bits]) – The arguments to pass to the left session.
args_right (list[claripy.ast.bits]) – The arguments to pass to the right session.
symbols (set[claripy.BVS] | frozenset[claripy.BVS]) – All symbolic values used in the two sessions. These symbols may be passed as arguments, or may have been pre-stored in the memory of the session before this method was called. This set is required during the concretization step where we need to generate concrete values for all symbolic values in the program.
cache_intermediate_info (bool) – If this flag is True, then information about intermediate states will be
cached. This is required for dumping the execution graph which is used in visualization. +:param int | None ret_addr_left: What address to return to if calling as a function +:param int | None ret_addr_right: What address to return to if calling as a function +:param int | None loop_bound_left: Sets an upper bound on loop iteration count for the left session. Useful for programs with non-terminating loops. +:param int | None loop_bound_right: Sets an upper bound on loop iteration count for the right session. Useful for programs with non-terminating loops.
+ +| + | Stores information about the concretization of a compatible state pair. |
+
| + | Stores information about the concretization of a TerminalState. |
+
|
++ |
Stores information about the concretization of a compatible state pair.
+args (any) – The same Python datastructures as the arguments passed to concrete_examples, except that all claripy symbolic variables are replaced with concrete values.
mem_diff (dict[range, tuple[int, int]]) – Concretized version of memory difference. Each key is a memory address range, and each value is a concretized version of the data stored at that location for the prepatched, postpatched runs.
reg_diff (dict[str, tuple[int, int]]) – Concretized version of register difference. Each key is a register name, and each value is a concretized version of the data stored at that register for the prepatched, postpatched runs.
left_side_effects (dict[str, list[ConcretePerformedSideEffect]]) – Concretized versions of side effects made by the prepatched state.
right_side_effects (dict[str, list[ConcretePerformedSideEffect]]) – Concretized versions of side_effects made by the postpatched state.
Stores information about the concretization of a TerminalState.
+args (any) – The same Python datastructures as the arguments passed to concrete_examples, except that all claripy symbolic variables are replaced with concrete values.
side_effects (dict[str, list[PerformedSideEffect]]) – Concretized side effects outputted by the singleton state.
| + | Abstract base class for all directives. |
+
| + | An enum to determine the type of assertion. |
+
| + | An assert directive sets a breakpoint at a certain address. |
+
| + | An assume directive sets a breakpoint at a certain address. An assume simply adds an extra constraint to the state's accumulated constraints before resuming execution. An assume is useful for adding a precondition. |
+
| + | This directive is used to log some piece of information about the program in a list attached to the state. When execution reaches the desired address, the log function will be called, and the result will be saved inside the state's globals dictionary. |
+
| + | If the program execution reaches the desired address, the state will be considered to be in an errored state and will be moved to the errored cache. This state will have no further execution. |
+
| + | This directive is used to halt execution at some particular address, and pass the current state to the provided |
+
| + | A Postcondition is a special type of assertion that is executed on terminal states for which execution has been |
+
Abstract base class for all directives.
+Bases: enum.Enum
An enum to determine the type of assertion.
+This type of assert will be triggered if the assertion condition can be falsified. This assertion type replicates +the behaviour of assertions as used in a typical testing environment. More precisely, this assertion uses +universal quantification. The assertion fails if the following condition does not hold: forall x . P(x), where +x is the program input, and P is the assertion condition.
+This type of assert will be triggered if the assertion condition cannot be satisfied, under the constraints of +the local state. This assertion type is a dual to ASSERT_MUST, and an exact analogue does not exist from +typical testing environments. More precisely, this assertion uses existential quantification. The assertion +fails if the following condition does not hold: exists x . P(x), where x is the program input, P is the +assertion condition, and C is the state’s constraints.
+This is type of assert is like ASSERT_CAN, but is computed under a global setting. If on any path the local +assertion exists x . P(x) holds, then all cases where the assertion failed will be scrubbed from the output. +This is much the same E from computation tree logic, which is also a global property. Note that this assertion +type should only be used in cases where the exploration is complete - ie all states can be explored.
+Bases: Directive
An assert directive sets a breakpoint at a certain address.
+addr (int) – The program address this assert is attached to.
condition_fun (Callable[[SimState], claripy.ast.bool]) – When the program reaches the desired address, the SimState will be passed to this function, and an assertion condition should be returned. This is then used internally by the SAT solver, along with the state’s accumulated constraints.
info_str (str | None) – Human readable label for this assertion, printed to the user if the assert is triggered.
assert_type (AssertType) – The type of assert.
Constructor for an Assert object.
+addr (int) – The address at which the assert will be triggered.
condition_fun (Callable[[SimState], claripy.ast.bool]) – When the program reaches the desired address, the SimState will be passed to this function, and an assertion condition should be returned. This is then used internally by the SAT solver, along with the state’s accumulated constraints.
info_str (str | None) – Human readable label for this assertion, printed to the user if the assert is triggered.
assert_type (AssertType) – The type of assert to construct.
Factory for an Assert object set at a certain offset from a function start.
+project (cozy.project.Project) – The project which this assert is attached to. The project is used to compute the address of the assert.
str (fun_name) – The name of the function in which this assert will be located.
int (offset) – The offset into the function in which this assert will be located.
condition_fun (Callable[[SimState], claripy.ast.bool]) – When the program reaches the desired address, the SimState will be passed to this function, and an assertion condition should be returned. This is then used internally by the SAT solver, along with the state’s accumulated constraints.
info_str (str | None) – Human readable label for this assertion, printed to the user if the assert is triggered.
assert_type (AssertType) – The type of assert to construct.
Bases: Directive
An assume directive sets a breakpoint at a certain address. An assume simply adds an extra constraint to the state’s accumulated constraints before resuming execution. An assume is useful for adding a precondition.
+addr (int) – The program address this assume is attached to.
condition_fun (Callable[[SimState], claripy.ast.bool]) – When the program reaches the desired address, the SimState will be passed to this function, and a condition should be returned. This condition is then attached to the state’s set of constraints.
info_str (str | None) – Human readable label for this assume.
Constructor for an Assume object.
+addr (int) – The address at which the assume will be triggered.
condition_fun (Callable[[SimState], claripy.ast.bool]) – When the program reaches the desired address, the SimState will be passed to this function, and an assumption should be returned. This assumption is attached to the state’s constraints for future execution.
info_str (str | None) – Human readable label for this assume.
Factory for an Assume object set at a certain offset from a function start.
+project (cozy.project.Project) – The project this assume is attached to.
str (fun_name) – The name of the function in which this assume will be located.
int (offset) – The offset into the function in which this assume will be located.
condition_fun (Callable[[SimState], claripy.ast.bool]) – When the program reaches the desired address, the SimState will be passed to this function, and an assumption should be returned. This assumption is attached to the state’s constraints for future execution.
info_str (str | None) – Human readable label for this assume.
A new Assume object at the desired function offset.
+Bases: Directive
This directive is used to log some piece of information about the program in a list attached to the state. When execution reaches the desired address, the log function will be called, and the result will be saved inside the state’s globals dictionary.
+addr (int) – The program address this virutal print is attached to.
log_fun (Callable[[SimState], claripy.ast.Base]) – This function takes in the current state and returns a claripy AST which should be logged. This value may be symbolic.
info_str (str) – Human readable label for this virtual print.
label (str) – Internal label used for side effect alignment. Side effects (including virtual prints) are diffed if they have the same label.
concrete_post_processor (Callable[[claripy.ast.Base], any] | None) – concrete_post_processor takes as input a concretized version of the output from log_fun and returns a result which is printed to the screen. For example, a log fun may return state.regs.eax to log the value of eax. But if eax represents a 32 bit signed value, we want to pretty print to negative number. This is where concrete_post_processor is useful. In this example concrete_post_processor would take a concrete bit vector representing a possible value of EAX and return a Python integer (which can be negative). This is what is shown to the user.
Constructor for a VirtualPrint object.
+addr (int) – The program address this virutal print is attached to.
log_fun (Callable[[SimState], claripy.ast.Base]) – This function takes in the current state and returns a claripy AST which should be logged. This value may be symbolic.
concrete_post_processor (Callable[[claripy.ast.Base], any] | None) – concrete_post_processor takes as input a concretized version of the output from log_fun and returns a result which is printed to the screen. For example, a log fun may return state.regs.eax to log the value of eax. But if eax represents a 32 bit signed value, we want to pretty print to negative number. This is where concrete_post_processor is useful. In this example concrete_post_processor would take a concrete bit vector representing a possible value of EAX and return a Python integer (which can be negative). This is what is shown to the user.
info_str (str) – Human readable label for this virtual print.
label (str) – Internal label used for side effect alignment. Side effects (including virtual prints) are diffed if they have the same label.
Factory for VirtualPrint object set at a certain offset from a function start.
+project (cozy.project.Project) – The project which this virtual print is attached to. The project is used to compute the address of the virtual print.
fun_name (str) – The name of the function in which this virtual print will be located.
offset (int) – The offset into the function in which this virtual print will be located.
log_fun (Callable[[SimState], claripy.ast.Base]) – This function takes in the current state and returns a claripy AST which should be logged. The return value may be symbolic.
concrete_post_processor (Callable[[claripy.ast.Base], any] | None) – concrete_post_processor takes as input a concretized version of the output from log_fun and returns a result which is printed to the screen. For example, a log fun may return state.regs.eax to log the value of eax. But if eax represents a 32 bit signed value, we want to pretty print to negative number. This is where concrete_post_processor is useful. In this example concrete_post_processor would take a concrete bit vector representing a possible value of EAX and return a Python integer (which can be negative). This is what is shown to the user.
info_str (str) – Human readable label for this virtual print.
label (str) – Internal label used for side effect alignment. Side effects (including virtual prints) are diffed if they have the same label.
A new VirtualPrint object at the desired function offset.
+Bases: Directive
If the program execution reaches the desired address, the state will be considered to be in an errored state and will be moved to the errored cache. This state will have no further execution.
+addr (int) – The program address this error directive is attached to.
str – Human readable information for this error directive.
Constructor for an ErrorDirective object.
+addr (int) – The program address this error directive is attached to.
info_str (str) – Human readable information for this error directive.
Factory for ErrorDirective object set at a certain offset from a function start.
+project (cozy.project.Project) – The project this error directive should be attached to.
fun_name (str) – The name of the function in which this error directive will be located.
offset (int) – The offset into the function in which this error directive will be located.
info_str (str | None) – Human readable information for this error directive.
A new ErrorDirective object at the desired function offset.
+Bases: Directive
This directive is used to halt execution at some particular address, and pass the current state to the provided +breakpoint function, which can then either modify the state or do some other side effect (like executing a Python +print() call).
+addr (int) – The program address this breakpoint is attached to.
breakpoint_fun (Callable[[SimState], None]) – This function takes in the state reached by the program at the attachment point.
Constructor for a VirtualPrint object.
+addr (int) – The program address this breakpoint is attached to.
breakpoint_fun (Callable[[SimState], None]) – This function takes in the state reached by the program at the attachment point.
Factory for VirtualPrint object set at a certain offset from a function start.
+project (cozy.project.Project) – The project which this virtual print is attached to. The project is used to compute the address of the virtual print.
fun_name (str) – The name of the function in which this virtual print will be located.
offset (int) – The offset into the function in which this virtual print will be located.
breakpoint_fun (Callable[[SimState], None]) – This function takes in the state reached by the program at the attachment point.
A new Breakpoint object at the desired function offset.
+Bases: Directive
A Postcondition is a special type of assertion that is executed on terminal states for which execution has been
+completed. This is identical to attaching an ASSERT_MUST assertion to all return points. This type of property
+is useful for verifying that a property holds in all terminal states. Note that if you are looking to add a
+precondition, you can add your proposition to the session before the run via
+cozy.Session.add_constraints().
condition_fun (Callable[[SimState], claripy.ast.bool]) – When the program reaches a terminal state, the SimState will be passed to this function, and an assertion condition should be returned. This is then used internally by the SAT solver, along with the state’s accumulated constraints.
info_str (str | None) – Human readable label for this postcondition assertion, printed to the user if the assert is triggered.
assert_type (AssertType) – The type of assert to construct.
| + | This class is used to store a networkx.DiGraph, decorated with SimStates, representing the full history of a symbolic program execution. |
+
|
++ |
|
++ |
|
+Generates and saves JSON data for Cozy-Viz. |
+
|
+Generates and visualizes JSON data for Cozy-Viz. |
+
|
+Generates JSON data for Cozy-Viz. |
+
Generates and saves JSON data for Cozy-Viz.
+Generates JSON data for Cozy-Viz from the results of two symbolic +executions, and saves the result to two files, one for pre and one for post.
+proj_a (Project) – The project associated with the first execuction.
proj_b (Project) – The project associated with the second execuction.
rslt_a (RunResult) – The result of the first execution.
rslt_b (RunResult) – The result of the second execution.
comparison_results (analysis.Comparison) – The comparison we wish to dump.
file_name_a (str, optional) – A name for the prepatch binary, displayed in visualization. +Default “prepatch”.
file_name_b (str, optional) – A name for the postpatch binary, displayed in visualization. +Default “postpatch”
output_file (str, optional) – A name for generated JSON file. Default “cozy-result.json”.
concrete_post_processor (Callable [[any],any] | None, optional) – This function is used to +post-process concretized versions of args before they are added to the +return string. Some examples of this function include converting an integer +to a negative number due to use of two’s complement, or slicing off parts of +the argument based on another part of the input arguments. Default None.
include_vex (bool, optional) – whether to, for each SimState, generate the +corresponding VEX IR and include the result in the JSON. Default False.
include_simprocs (bool, optional) – whether to, for each SimState, flag any +SimProcedure locations occurring in the corrsponding basic block. Default False.
include_simprocs – whether to include a listing of +SimProcedures called in each basic block. Default False.
include_actions (bool, optional) – whether to include logging of +read/write operations on memory and registers. Default False.
include_debug (bool, optional) – whether to include debugging information +recovered from DWARF metadata. Default False.
include_side_effects (bool, optional) – whether to include cozy side effects, +like virtual prints, if present. Default True.
args (any, optional) – The input arguments to concretize. This argument
+may be a Python datastructure, the concretizer will make a deep copy with
+claripy symbolic variables replaced with concrete values. See
+cozy.analysis.CompatiblePair. Default = [].
num_examples (int, optional) – The number of concrete examples to +generate and incorporate into the JSON, for each dead-end state. Default 0.
Generates and visualizes JSON data for Cozy-Viz.
+Generates JSON data suitable for visual comparison using Cozy-Viz from the results of two symbolic executions, and launches a server to view the data.
+proj_a (Project) – The project associated with the first execuction.
proj_b (Project) – The project associated with the second execuction.
rslt_a (RunResult) – The result of the first execution.
rslt_b (RunResult) – The result of the second execution.
comparison_results (analysis.Comparison) – The comparison we wish to dump.
concrete_post_processor (Callable [[any],any] | None, optional) – This function is used to +post-process concretized versions of args before they are added to the +return string. Some examples of this function include converting an integer +to a negative number due to use of two’s complement, or slicing off parts of +the argument based on another part of the input arguments. Default None.
include_vex (bool, optional) – whether to, for each SimState, generate the +corresponding VEX IR and include the result in the JSON. Default False.
include_simprocs (bool, optional) – whether to include a listing of +SimProcedures called in each basic block. Default False.
include_actions (bool, optional) – whether to include logging of +read/write operations on memory and registers. Default False.
include_debug (bool, optional) – whether to include debugging information +recovered from DWARF metadata. Default False.
include_side_effects (bool, optional) – whether to include cozy side effects, +like virtual prints, if present. Default True.
args (any, optional) – The input arguments to concretize. This argument
+may be a Python datastructure, the concretizer will make a deep copy with
+claripy symbolic variables replaced with concrete values. See
+cozy.analysis.CompatiblePair. Default [].
num_examples (int, optional) – The number of concrete examples to +generate and incorporate into the JSON, for each dead-end state. Default 0.
open_browser (bool, optional) – Automatically open cozy-viz with the +comparison data loaded. Default False.
port (int, optional) – The port to serve cozy-viz on. Default 8080.
Generates JSON data for Cozy-Viz.
+Generates JSON data suitable for visual comparison using Cozy-Viz from the results of two symbolic executions.
+proj_a (Project) – The project associated with the first execuction.
proj_b (Project) – The project associated with the second execuction.
rslt_a (RunResult) – The result of the first execution.
rslt_b (RunResult) – The result of the second execution.
concrete_post_processor (Callable [[any],any] | None, optional) – This function is used to +post-process concretized versions of args before they are added to the +return string. Some examples of this function include converting an integer +to a negative number due to use of two’s complement, or slicing off parts of +the argument based on another part of the input arguments. Default None.
include_vex (bool, optional) – whether to, for each SimState, generate the +corresponding VEX IR and include the result in the JSON. Default False.
include_simprocs (bool, optional) – whether to include a listing of +SimProcedures called in each basic block. Default False.
include_actions (bool, optional) – whether to include logging of +read/write operations on memory and registers. Default False.
include_debug (bool, optional) – whether to include debugging information +recovered from DWARF metadata. Default False.
include_side_effects (bool, optional) – whether to include cozy side effects, +like virtual prints, if present. Default True.
args (any, optional) – The input arguments to concretize. This argument
+may be a Python datastructure, the concretizer will make a deep copy with
+claripy symbolic variables replaced with concrete values. See
+cozy.analysis.CompatiblePair. Default = [].
num_examples (int, optional) – The number of concrete examples to +generate and incorporate into the JSON, for each dead-end state. Default 0.
A pair of directed graphs +representing the two symbolic executions.
+This class is used to store a networkx.DiGraph, decorated with SimStates, representing the full history of a symbolic program execution. +It constructs an ExecutionGraph, from a project and the results of an +executed project session.
+An internal method which renders the assembly corresponding to a given basic block as a formatted string
+b (Block) – The block to render.
+The rendered string.
+An internal method which lists SimProcedure calls occuring in a block
+b (Block) – the block to scan
+An internal method which checks whether the jumpkind of a Block is +a syscall.
+b (Block) – the relevant Block
+Whether the jumpkind is a syscall
+Convert the SimState-decorated graph into a graph decorated with +integers, carrying symbolic program execution data in the attributes +stdout, stderr, contents (this holds a basic block), +constraints, actions (optionally) and state.
+The resulting graph.
+Convert the SimState-decorated graph into a graph decorated with
+integers, carrying symbolic program execution data in the attributes
+stdout, stderr, contents, constraints ,`vex` and state. The
+difference from reconstruct_bbl_addr_graph() is that the data is
+now pretty-printed and suitable for serialization.
The resulting graph.
+Dump the graph as cytoscapejs readable JSON.
+name (str) – The filename for the generated json.
+| + | + |
| + | + |
| + | + |
| + | + |
| + | + |
|
+Simultaneously maps and folds over a nested Python datastructure in preorder traversal order. The datastructure may consist of arbitrarily nested lists, tuples, dictionaries and sets. Note that for dictionaries, both keys and values will be traversed. |
+
|
+Folds over a Python datastructure in preorder traversal. The datastructure may consist of arbitrarily nested lists, tuples, dictionaries and sets. Note that for dictionaries, both keys and values will be traversed. |
+
|
+Maps a Python datastructure. The datastructure may consist of arbitrarily nested lists, tuples, dictionaries and sets. |
+
|
+Composes two functions, f and g, to create a new function h(*a, **kw) = f(g(*a, **kw)) |
+
Simultaneously maps and folds over a nested Python datastructure in preorder traversal order. The datastructure may consist of arbitrarily nested lists, tuples, dictionaries and sets. Note that for dictionaries, both keys and values will be traversed.
+val0 (any) – The datastructure to traverse.
f (Callable[[any, T], tuple[any, T]]) – This function takes as input a value inside the datastructure, the accumulated value and should return a mapped value and newly accumulated value.
accum0 (T) – Initial accumulation parameter.
The mapped datastructure and final accumulated value.
+tuple[any, T]
+Folds over a Python datastructure in preorder traversal. The datastructure may consist of arbitrarily nested lists, tuples, dictionaries and sets. Note that for dictionaries, both keys and values will be traversed.
+val0 (any) – The datastructure to traverse.
f (Callable[[any, U], U]) – This function takes as input the value inside the datastructure, the accumulated value and should return a new accumulated value.
accum0 (U) – Initial accumulation parameter.
The final accumulated value.
+U
+Maps a Python datastructure. The datastructure may consist of arbitrarily nested lists, tuples, dictionaries and sets.
+val0 (any) – The datastructure to map. Note that for dictionaries, both keys and values will be mapped.
+The mapped datastructure.
+any
+Composes two functions, f and g, to create a new function h(*a, **kw) = f(g(*a, **kw))
+f (Callable[[B], C]) – The first function to compose.
g (Callable[[...], B]) – The second function to compose.
A newly composed function which takes in an arbitrary number of arguments and keyword arguments, and returns a C.
+Callable[[…], C]
+| + | + |
|
+Disable cozy logging |
+
|
+Set the level of logging |
+
|
+Log at the info level |
+
|
+Log at the warning level |
+
|
+Log at the error level |
+
|
+Log at the debug level |
+
|
+Log at the critical level |
+
Disable cozy logging
+Set the level of logging
+Log at the info level
+Log at the warning level
+Log at the error level
+Log at the debug level
+Log at the critical level
+| + | + |
|
+Generates a fresh symbolic pointer for the input architecture. |
+
|
+Generates claripy expressions for constraining the input symbolic pointer to a specific concrete value. |
+
|
+Converts an integer from two's complement form back to an integer, assuming the value is stored in num_bits space. |
+
|
+Converts an integer value to two's complement representation, assuming the value is stored in num_bits space. |
+
Generates a fresh symbolic pointer for the input architecture.
+arch (Type[Arch]) – The architecture the pointer is for. For example in x64, the paramater passed should be archinfo.ArchAMD64, and a 64 bit symbolic pointer will be returned.
name (str | None) – A human readable name for the symbolic pointer. If None is passed an autogenerated symbolic_ptr_i name is used.
A fresh symbolic bitvector whose size is appropriate for the input architecture.
+claripy.BVS
+Generates claripy expressions for constraining the input symbolic pointer to a specific concrete value.
+symbolic_ptr (claripy.ast.bits) – The symbolic pointer to constrain.
concrete_addr (int) – The concrete address which the symbolic pointer should be equal to.
can_be_null (bool) – If this value is True, the returned constraints will contain a disjunction which allows the symbolic pointer to be NULL.
A claripy proposition constraining the symbolic pointer.
+claripy.ast.bool
+Converts an integer from two’s complement form back to an integer, assuming the value is stored in num_bits space.
+val (int) – The two’s complement integer to convert. This number must be non-negative.
num_bits (int) – The number of bits used to store the number.
A signed Python representation of the integer.
+int
+Converts an integer value to two’s complement representation, assuming the value is stored in num_bits space.
+val (int) – The integer value to convert.
num_bits (int) – The number of bits used to store the integer.
A two’s complement representation of the value. This value is non-negative.
+int
+| + | Represents a project for a single executable |
+
Represents a project for a single executable
+angr_proj (angr.Project) – The angr project created for this cozy project.
fun_prototypes (dict[str | int, str]) – Maps function names or function addresses to their type signatures.
Constructor for a project.
+binary_path (str) – The path to the binary to analyze.
fun_prototypes (dict[str | int, str] | None) – Initial dictionary that maps function names or addresses to their type signatures. If None is passed, fun_prototypes is initialized to the empty dictionary.
kwargs – Extra arguments to pass to angr.Project
Returns the ranges of the objects stored in the executable (for example: ELF objects). If obj_filter is specified, only objects that pass the filter make it into the return list.
+obj_filter (Callable[[Backend], bool] | None) – Used to filter certain objects from the output list.
+A list of memory ranges.
+list[range]
+Finds the rebased addressed of a symbol. Functions are the most common symbol type.
+sym_name (str) – The symbol to lookup.
+The rebased symbol address
+int
+Adds a function prototype to this project.
+fun (str | int) – The function’s name or address.
fun_prototype (str) – The function’s type signature.
None
+None
+Returns a new session derived from this project.
+start_fun (str | int | None) – The name or address of the function which this session will start with. If None is specified, then the program will start at the entry point (main function).
+The fresh session.
+Hooks a symbol in the angr project. If the symbol is one from libc, this method will also replace
+what is stored in angr.SIM_PROCEDURES["libc"][symbol_name].
symbol_name (str) – The name of the symbol to hook.
simproc_class (type[SimProcedure]) – The class to use to hook the symbol. Note that this is not an instance of SimProcedure, but is instead a reference to the class itself.
kwargs – These are the keyword arguments that will be passed to the procedure’s run method eventually.
replace (bool | None) – Control the behavior on finding that the address is already hooked. If true, silently replace the hook. If false, warn and do not replace the hook. If none (default), warn and replace the hook.
int
+The address of the new symbol.
+Hooks a syscall in the angr project.
+syscall_name (str) – The name of the syscall to hook.
simproc_class (type[SimProcedure]) – The class to use to hook the symbol. Note that this is not an instance of SimProcedure, but is instead a reference to the class itself.
| + | Simple HTTP request handler with GET and HEAD commands. |
+
| + | + |
|
+Serves Cozy-Viz on localhost:8080. |
+
Bases: http.server.SimpleHTTPRequestHandler
Simple HTTP request handler with GET and HEAD commands.
+This serves files from the current directory and any of its +subdirectories. The MIME type for files is determined by +calling the .guess_type() method.
+The GET and HEAD requests are identical except that the HEAD +request omits the actual contents of the file.
+Serve a GET request.
+Serves Cozy-Viz on localhost:8080.
+Useful for visualization of information generated using
+cozy.execution_graph.compare_and_dump().
To include comparison data, use the pre and post arguments, and add +a query string to the URL, like so: localhost:8080?pre=/pre&post=/post.
+pre (dict, optional) – served as JSON at /pre on the server. Default {}.
post (dict, optional) – served as JSON at /post on the server. Default {}.
port (int, optional) – An alternative port to serve on. Default 8080.
| + | + |
| + | + |
| + | This class is used for storing the results of running a session. |
+
| + | + |
| + | + |
| + | + |
| + | A session is a particular run of a project, consisting of attached directives (asserts/assumes). You can malloc memory for storage prior to running the session. Once you are ready to run the session, use the run method. |
+
|
++ |
|
++ |
|
++ |
This class is used for storing the results of running a session.
+deadended (list[DeadendedState]) – States that reached normal termination.
errored (list[ErrorState]) – States that reached an error state. This may be triggered for example by program errors such as division by 0, or by reaching a cozy.directive.ErrorDirective.
asserts_failed (list[AssertFailed]) – States where an assertion was able to be falsified.
assume_warnings (list[tuple[Assume, SimState]]) – An assume warning occurs when a Assume is reached, and the added assumption contradicts the constraints for that state. This means that due to the assumption, the new constraints are not satisfiable.
postconditions_failed (list[PostconditionFailedState]) – States where the function returned, and the assertion as part of the postcondition could be falsified.
spinning (list[SpinningState]) – States that were stashed due to a loop bound being breached.
Returns True if there were any assertions triggered during this run.
+True if there were assertions triggered.
+bool
+Returns True if there were any postcondition assertions triggered during this run.
+True if there were postcondition assertions triggered.
+bool
+Return str(self).
+Creates a composite human readable report with information about errored states, asserts failed, postconditions failed, and spinning states.
+args (any) – The arguments to concretize
concrete_post_processor (Callable[[any], any] | None) – This function is used to post-process concretized versions of args before they are added to the return string. Some examples of this function include converting an integer to a negative number due to use of two’s complement, or slicing off parts of the argument based on another part of the input arguments.
num_examples (int) – The maximum number of concrete examples to show the user.
The report as a string
+str
+Creates a human readable report about a list of errored states.
+args (any) – The arguments to concretize
concrete_post_processor (Callable[[any], any] | None) – This function is used to post-process concretized versions of args before they are added to the return string. Some examples of this function include converting an integer to a negative number due to use of two’s complement, or slicing off parts of the argument based on another part of the input arguments.
num_examples (int) – The maximum number of concrete examples to show the user for each errored state.
The report as a string
+str
+Creates a human readable report about a list of failed postcondition assertions.
+args (any) – The arguments to concretize
concrete_post_processor (Callable[[any], any] | None) – This function is used to post-process concretized versions of args before they are added to the return string. Some examples of this function include converting an integer to a negative number due to use of two’s complement, or slicing off parts of the argument based on another part of the input arguments.
num_examples (int) – The maximum number of concrete examples to show the user for each assertion failed state.
The report as a string
+str
+Creates a human readable report about the failed postcondition assertions.
+args (any) – The arguments to concretize
concrete_post_processor (Callable[[any], any] | None) – This function is used to post-process concretized versions of args before they are added to the return string. Some examples of this function include converting an integer to a negative number due to use of two’s complement, or slicing off parts of the argument based on another part of the input arguments.
num_examples (int) – The maximum number of concrete examples to show the user for each assertion failed state.
The report as a string
+str
+Creates a human readable report about any failed assertions.
+args (any) – The arguments to concretize
concrete_post_processor (Callable[[any], any] | None) – This function is used to post-process concretized versions of args before they are added to the return string. Some examples of this function include converting an integer to a negative number due to use of two’s complement, or slicing off parts of the argument based on another part of the input arguments.
num_examples (int) – The maximum number of concrete examples to show the user for each assertion failed state.
The report as a string
+str
+Bases: _SessionExploration
Bases: _SessionExploration
A session is a particular run of a project, consisting of attached directives (asserts/assumes). You can malloc memory for storage prior to running the session. Once you are ready to run the session, use the run method.
+:ivar angr.SimState state: The initial state tied to this particular session. You can access this member to modify properties of the state before a run.
+:ivar cozy.project.Project proj: The Project tied to this session.
+:ivar str | int | None start_fun: The starting function tied to this session. If start_fun is None, then the session starts in an entry state.
+:ivar list[Directive] directives: The directives added to this session.
+:ivar bool has_run: True if the cozy.project.Session.run() method has been called, otherwise False.
Constructs a session derived from a project. The cozy.project.Project.session() is the preferred method for creating a session, not this constructor.
Stores a file in a virtual filesystem available during execution. This method simply forwards the arguments to state.fs.insert.
+filename (str) – The filename of the new file.
simfile (angr.SimFile) – The file to make available to the simulated program.
None
+None
+Mallocs a fixed amount of memory using the angr heap simulation plugin. Useful for setting things up in memory before the run() method is called.
num_bytes (int) – The number of bytes to allocate.
+A pointer to the allocated memory block.
+int
+Stores data at some address. This method simply forwards the arguments to state.memory.store.
+addr (int) – Address to store the data at.
data (claripy.ast.bits) – The data to store in memory.
kwargs – Additional keyword arguments to pass to state.memory.store
Adds multiple directives to the session.
+directives (Directive) – The directives to add.
+None
+None
+Adds multiple constraints to the session’s state.
+constraints (claripy.ast.bool) – The constraints to add
+None
+None
+Runs a session to completion, either starting from the start_fun used to create the session, or from the program start. Note that currently a session may be run only once. If run is called multiple times, a RuntimeError will be thrown.
+args (list[claripy.ast.bits]) – The arguments to pass to the function. angr will utilize the function’s type signature to figure out the calling convention to use with the arguments.
cache_intermediate_info (bool) – If this flag is True, then information about intermediate states will be
cached. This is required for dumping the execution graph which is used in visualization. +:param int | None ret_addr: What address to return to if calling as a function +:param int | None loop_bound: Sets an upper bound on loop iteration count. Useful for programs with non-terminating loops. +:return: The result of running this session. +:rtype: RunResult
+| + | This class encapsulates the idea of a side effect whose body may consist of mixed symbolic and concrete values. |
+
| + | This class encapsulates the idea of a side effect whose body previously consisted of mixed symbolic and concrete |
+
|
+Attaches a side effect to the passed state. |
+
|
+Gets the side effects attached to a specific state |
+
|
+Gets the side effects from the given channel attached to a specific state. An empty list is returned for channels |
+
|
++ |
| + | + |
This class encapsulates the idea of a side effect whose body may consist of mixed symbolic and concrete values.
+state_history (SimStateHistory) – The point in execution at which the side effect was performed.
body – The body must be a mixture of string-keyed Python dictionaries, Python lists, Python tuples, and claripy concrete and symbolic values.
concrete_post_processor – The optional post processing function to apply to concretized versions of the side effect’s body if post processing is required.
label – The label to apply to the side effect, used to align instances of side effects when making comparisons. For example, if you have two call sites to a network send function, you would want different labels for the two different call locations.
This class encapsulates the idea of a side effect whose body previously consisted of mixed symbolic and concrete +values, but now consists of only concrete values (ie, BVV and FPV). At the point of the construction, this concrete +value has not yet been passed through the user provided concrete_post_processor, whose job is to take the concrete value +and transform the BVV values into ordinary Python values. The purpose of concrete_post_processor for instance could be +to transform a two’s complement BVV that is negative into a negative Python integer. This will make the display +more readable to the user. Hence, the concrete_post_processor can be viewed as a post-processing function.
+base_effect (PerformedSideEffect) – The non-symbolic side effect that was concretized.
state_history (SimStateHistory) – The point in execution at which the side effect was performed.
body – The body must be a mixture of string-keyed Python dictionaries, Python lists, Python tuples, and claripy concrete values.
concrete_post_processor – The optional post processing function to apply to concretized versions of the side effect’s body if post processing is required.
label – The label to apply to the side effect, used to align instances of side effects when making comparisons. For example, if you have two call sites to a network send function, you would want different labels for the two different call locations.
Attaches a side effect to the passed state.
+state (SimState) – The state in which the side effect should be performed and attached to.
channel (str) – The name of the channel in which the side effect should be performed. Different side effects should be sent down different channels. For example, the virtual print side effect channel is different from the networking side effect channel.
body – The body must be a mixture of string-keyed Python dictionaries, Python lists, Python tuples, claripy concrete values, and claripy symbolic values. This should represent the payload of the side effect.
concrete_post_processor – The optional post processing function to apply to concretized versions of the side effect’s body if post processing is required.
label – The label to apply to the side effect, used to align instances of side effects when making comparisons. For example, if you have two call sites to a network send function, you would want different labels for the two different call locations.
Gets the side effects attached to a specific state
+state (SimState) – The state from which we should retrieve the side effects.
+dict[str, list[PerformedSideEffect]]
+All side effects attached to this state. Each entry in the dictionary is a different channel.
+Gets the side effects from the given channel attached to a specific state. An empty list is returned for channels +in which the channel has not yet been used.
+state (SimState) – The state from which we should retrieve the side effects channel.
channel (str) – The name of the channel
list[PerformedSideEffect]
+A list of side effects for the requested channel.
+| + | + |
| + | A Stubber outputs Python source code that represents stubs for the callees of a given binary function. |
+
A Stubber outputs Python source code that represents stubs for the callees of a given binary function.
+If foo is the function to be analyzed, and foo calls a two-argument function bar, then the following stub +will be among those generated for foo:
+
+pass
+The stub can then be filled out and used during symbolic execution.
+binary_path (str) – Path for the binary under analysis.
+cfg (angr.analyses.cfg.cfg_fast.CFGFast) – CFG for the binary.
cg (networkx.classes.multidigraph.MultiDiGraph) – Call graph for the binary.
Returns the function with the given name from the CFG.
+func_name (str) – Name of the function to extract.
+Function with the given name.
+angr.knowledge_plugins.functions.function.Function
+Returns the list of functions called by function func_name.
+func_name (str) – Name of the caller function.
+The list of functions called by func_name.
+list[angr.knowledge_plugins.functions.function.Function]
+Returns an empty Python class definition (in string form) named after func that inherits from angr.SimProcedure.
+func (angr.knowledge_plugins.functions.function.Function) – Function to be stubbed.
+Empty Python class definition representing a symbolic execution stub for function func.
+str
+Returns a list of stubs for the callees of function func_name.
+func_name (str) – Name of the caller function.
+Stubs for the callees of function func_name.
+list[str]
+| + | Stores information pertaining specifically to a single SimState. |
+
| + | This class is used to indicate that execution terminated normally in the contained state. |
+
| + | This class is used to indicate that the contained state was killed by the LocalLoopSeer, indicating that an upper |
+
| + | This class is used to indicate that execution failed due to an |
+
| + | This class is used to indicate that execution failed due to an |
+
| + | This class is used to indicate a state that resulted in an error (either my an execution error or |
+
Stores information pertaining specifically to a single SimState.
+state (SimState) – The state we are storing information about.
state_id (int) – The index of this particular state in the corresponding list in RunResult. Note that errored states have separate state_ids from deadended states. Therefore a particular input state here is uniquely identified by the pair (state_id, state_tag), not just state_id by itself.
state_type_str (str) – A string representation of the state’s type
The data that has been written to stdout when the program is in this state.
+The data written to stdout
+bytes
+The data that has been written to stderr when the program is in this state.
+The data written to stderr
+bytes
+Returns the output of the virtual prints that occurred while reaching this state.
+A list of VirtualPrint directives, along with the values they produced.
+list[tuple[VirtualPrint, claripy.ast.Base]]
+The memory writes that occurred while reaching this state.
+An interval dictionary, with the keys being ranges and the values being tuple[int, frozenset[int]]. The first element of the tuple is a unique placeholder, the second element of the tuple are the possible instruction pointer values that wrote to this memory.
+P.IntervalDict
+Concretizes the arguments used to put the program in this singleton state.
+args (any) – The input arguments to concretize. This argument may be a Python datastructure, the concretizer will make a deep copy with claripy symbolic variables replaced with concrete values.
num_examples (int) – The maximum number of concrete examples to generate for this singleton state.
A list of concrete inputs that satisfies the constraints attached to the state.
+list[TerminalStateInput]
+Bases: TerminalState
This class is used to indicate that execution terminated normally in the contained state.
+Constructor for DeadendedState
+state (SimState) – The state that terminated normally.
state_id (int) – The identifer of the state, determined by its position in the list cozy.project.RunResult.deadended
Bases: TerminalState
This class is used to indicate that the contained state was killed by the LocalLoopSeer, indicating that an upper +bound on number of loop iterations was reached.
+Constructor for SpinningState
+state (SimState) – The state that was spinning
state_id (int) – The identifer of the state, determined by its position in the list cozy.project.RunResult.spinning
Bases: TerminalState
This class is used to indicate that execution failed due to an Assert being satisfiable.
assertion (Assert) – The assertion that was triggered.
cond (claripy.ast.bool) – The condition that caused the assertion to trigger
Constructor for AssertFailedState
+assertion (Assert) – The assertion that was triggered.
claripy.ast.bool – The condition which if falsified will trigger the assertion.
failure_state (SimState) – The state that was created to test the assertion.
state_id (int) – The identifier of the state, determined by its position in the list cozy.project.RunResult.asserts_failed
Bases: TerminalState
This class is used to indicate that execution failed due to an Assert being satisfiable.
assertion (Assert) – The assertion that was triggered.
cond (claripy.ast.bool) – The condition that caused the assertion to trigger
Constructor for AssertFailedState
+assertion (Postcondition) – The postcondition that was triggered.
claripy.ast.bool – The condition which if falsified will trigger the postcondition assertion.
failure_state (SimState) – The state that was created to test the postcondition assertion.
state_id (int) – The identifier of the state, determined by its position in the list cozy.project.RunResult.postconditions_failed
Bases: TerminalState
This class is used to indicate a state that resulted in an error (either my an execution error or ErrorDirective).
error (SimError) – The error that was thrown.
traceback – The traceback attached to the error.
Constructor for ErrorState
+error_record (ErrorRecord) – The error thrown for this state.
state_id (int) – The identifier of the state, determined by it’s position in the list cozy.project.RunResult.errored
|
+Parses a C-style type definition given in the input string, assuming the given architecture. Registers this type with angr. |
+
|
+Parses a series of type definition given in the input string. Registers this type with angr. |
+
Parses a C-style type definition given in the input string, assuming the given architecture. Registers this type with angr.
+type_definition (str) – The type definition, given in C-style format.
arch (Arch) – The architecture this type should be used with.
The parsed typed.
+SimType
+Parses a series of type definition given in the input string. Registers this type with angr.
+type_definition (str) – The type definition, given in C-style format.
arch (Arch) – The architecture this type should be used with.
The parsed typed.
+SimType
+This page contains auto-generated API reference documentation [1].
+Concolic execution is a state exploration strategy that uses concrete values to
+guide symbolic execution. cozy performs concolic execution slightly differently
+than what you might be used to with angr, including angr’s Unicorn engine. In
+our implementation of concolic execution, concrete values for each symbol are
+chosen, and symbolic execution proceeds as normal. When a branch is created in
+the symbolic execution, the concrete values are substituted into the constraints
+of both children, and the children that evaluate to false are placed in a deferred
+stash. Once execution reaches a terminal state, a deferred child is selected using
+some heuristic, and its constraints are used to generate a new concrete input.
+This is equivalent to negating a portion of the path constraint that you might
+typically see in literature on concolic execution. Our core implementation of
+concolic execution can be used outside of the cozy workflow as a standalone
+exploration technique. The relevant classes if you wish to do this can be found
+in the cozy.concolic.exploration module.
Since cozy is a comparative framework, we implement an additional strategy +called joint concolic execution. In joint concolic execution, we alternate +between the two programs when generating concrete values. After a concrete value +is implemented, we run both programs on the same concrete values, which automatically +leads to compatible state pairs being generated.
+Note that like typical symbolic execution, concolic execution can be complete +if so desired. The execution is complete if there are no deferred states in either +program. However the primary benefit of concolic execution is that we can explore +promising paths at the expense of an incomplete analysis. The promising paths in cozy +are determined by heuristics. There are two different heuristics required for +concolic execution:
+A termination heuristic, which determines when to halt concolic execution.
A candidate heuristic, which determines which deferred state to explore next.
Some pre-made heuristics can be found in cozy.concolic.heuristics. Let’s
+walk through an example of using a joint concolic session to explore how to use
+cozy.concolic.session.JointConcolicSession.
Let’s assume that we already have a prepatched and postpatched cozy project set up:
+sess_prepatched = proj_prepatched.session('process_sensor_data')
+add_directives(sess_prepatched)
+initialize_state(sess_orig)
+
+sess_postpatched = proj_postpatched.session('process_sensor_data')
+add_directives(sess_postpatched)
+initialize_state(sess_postpatched)
+We are now ready to create and run a joint concolic session. We must remember to pass
+a set of symbols used in the program to the
+run() method, as we need to assign
+concrete values to every symbolic value. We also construct the candidate and termination
+heuristics:
joint_sess = JointConcolicSession(sess_prepatched, sess_postpatched,
+ candidate_heuristic_left=BBTransitionCandidate(),
+ candidate_heuristic_right=BBTransitionCandidate(),
+ termination_heuristic_left=CyclomaticComplexityTermination.from_session(sess_prepatched),
+ termination_heuristic_right=CyclomaticComplexityTermination.from_session(sess_postpatched))
+(prepatched_results, postpatched_results) = joint_sess.run([], [], symbols)
+Here we are setting heuristics so that we do not explore every state. Instead, our candidate
+heuristic will pick states with the most unique basic block edge transitions in their history,
+and the exploration will be terminated once the number of terminal states exceeds the
+cyclomatic complexity of the session’s function. The return result from the
+run() method gives two
+RunResult objects, which can be directly be used by
+cozy.analysis.Comparison:
comparison_results = analysis.Comparison(prepatched_results, postpatched_results)
+We can of course visualize the results in the browser:
+# Here args is not the function arguments, but rather the contents of the memory
+# mutated by initialize_state
+execution_graph.visualize_comparison(proj_prepatched, proj_postpatched,
+ prepatched_results, postpatched_results,
+ comparison_results,
+ concrete_arg_mapper=concrete_mapper, args=args,
+ num_examples=2, open_browser=True)
+The full implementation used in this guide can be found at +https://github.com/draperlaboratory/cozy/blob/main/examples/cmp_weather_v5_concolic.py
+${JSON.stringify(concretion, undefined, 2)}
+ `)
+ }
+
+ const sharedMsg = sharedConcretions.length == 0
+ ? "No concretions available"
+ : html`Viewing ${sharedConcretions.length} concrete input examples shared by both branches`
+
+ const leftMsg = leftOnlyConcretions.length == 0
+ ? rightOnlyConcretions.length == 0
+ ? "There are no inputs that go down the left but not the right branch. The two branches correspond to exactly the same inputs."
+ : "There are no inputs that go down the left but not the right branch. The left branch refines the right."
+ : html`Viewing ${leftOnlyConcretions.length} concrete input examples that go down the left but not the right branch`
+
+ const rightMsg = rightOnlyConcretions.length == 0
+ ? leftOnlyConcretions.length == 0
+ ? "There are no inputs that go down the right but not the left branch. The two branches correspond to exactly the same inputs."
+ : "There are no inputs that go down the right but not the left branch. The right branch refines the left."
+ : html`Viewing ${rightOnlyConcretions.length} concrete input examples that go down the right but not the left branch`
+
+ return html`
+
+ ${hunks}`
+ }
+}
diff --git a/cozy-viz/components/memoryDifference.js b/cozy-viz/components/memoryDifference.js
new file mode 100644
index 0000000..a5d8a8f
--- /dev/null
+++ b/cozy-viz/components/memoryDifference.js
@@ -0,0 +1,38 @@
+import { html } from 'https://unpkg.com/htm/preact/index.module.js?module'
+import { Component } from 'https://unpkg.com/preact@latest?module'
+import ConcretionSelector from './concretionSelector.js'
+
+export default class MemoryDifference extends Component {
+ constructor() {
+ super();
+ this.state = { view: "symbolic" }
+ }
+
+ render(props, state) {
+ const rightId = props.rightFocus.bot.id()
+ const addresses = []
+ const conc_adiffs = props.leftFocus.bot.data().compatibilities[rightId].conc_memdiff ?? []
+ const adiffs = state.view === "symbolic"
+ ? props.leftFocus.bot.data().compatibilities[rightId].memdiff
+ : conc_adiffs[state.view]
+ for (const addr in adiffs) {
+ const addrparts = addr
+ .split('\n')
+ .map(part => [part, html`${pruningStatus.pruningRegex},
+ or correspond to a branch that doesn't match this regex Comparing
+ ${props.prelabel}
+ and
+ ${props.postlabel}.
+
Limiting attention to branches that:
${JSON.stringify(x, replacer, 2)}`)}
+ ${
+ this.state.node?.data().constraints?.map?.(
+ c => html`${c}`
+ )}`
+ }
+ case "assembly" : {
+ return html`${this.state.node.data().contents}`
+ }
+ case "vex" : {
+ return html`${this.state.node.data().vex}`
+ }
+ case "errors" : {
+ if (this.state.node.data().error) {
+ return html`${this.state.node.data().error}`
+ } else if (this.state.node.data().spinning) {
+ return html`Spinning: Loop bounds exceeded` + } else { + return null + } + } + case "stdout" : { + if (this.state.node.data().stdout) { + return html`
${this.state.node.data().stdout}`
+ } else {
+ return null
+ }
+ }
+ case "stderr" : {
+ if (this.state.node.data().stderr) {
+ return html`${this.state.node.data().stderr}`
+ } else {
+ return null
+ }
+ }
+ case "simprocs" : {
+ return html`${
+ this.state.node?.data().simprocs?.map?.(
+ simproc => html`${simproc}`
+ )}`
+ }
+ case "assertion" : {
+ if (this.state.node?.data().assertion_info) {
+ return html`
+
+ Condition: ${this.state.node?.data().failed_cond}
+ Address: ${this.state.node?.data().assertion_addr}
+
+ `
+ } else {
+ return null
+ }
+ }
+ case "postcondition" : {
+ if (this.state.node?.data().postcondition_info) {
+ return html`
+
+ Condition: ${this.state.node?.data().failed_cond}
+
+ `
+ } else {
+ return null
+ }
+ }
+ default: return null;
+ }
+ }
+
+ setView(mode) {
+ this.setState({mode}, () => this.refreshPosition())
+ }
+
+ clearTooltip() {
+ this.setState({style : {
+ visibility:"hidden",
+ left: 0,
+ top: 0,
+ zIndex: 0,
+ }})
+ }
+
+ render(_props,state) {
+ return html`| + | + |
| + | + |
| + | + |
| + | + |
| + | + |
| + | + |
| + | + |
| + | + |
| + | + |
| + | + |
| + | + |
| + | + |
| + | + |
| + | + |
On this page we will cover the architecture of cozy and how you can use +it to compare two binary programs. cozy is based on the angr symbolic +execution framework, so we support the same architectures as angr. We +will be following the null_deref example, which can be found in the +examples and test_programs folder in the cozy repository. The null_deref +source code is a very simple C program which writes the integer 42 to +some location in memory:
+Prepatched null_deref (first program being compared):
+#include <stdio.h>
+
+void my_fun(int *num) {
+ *num = 42;
+}
+
+int main(int argc, char *argv[]) {
+ int my_num;
+ my_fun(&my_num);
+ printf("my_num: %d\n", my_num);
+ return 0;
+}
+Postpatched null_deref_patched (second program being compared):
+#include <stdio.h>
+
+void my_fun(int *num) {
+ if (num != NULL) {
+ *num = 42;
+ }
+}
+
+int main(int argc, char *argv[]) {
+ int my_num;
+ my_fun(&my_num);
+ printf("my_num: %d\n", my_num);
+ return 0;
+}
+Let’s assume that we are compiling for x64 architecture. In this case we +are interested in comparing my_fun between the two programs. Much like angr, +cozy can be used interactively through a Python REPL or through a Python script.
+To make comparisons between two programs with different function +implementations, cozy uses symbolic execution. Both programs are fed +the same symbolic input, and cozy runs symbolic execution until all states +terminate. At the end of execution, we have a list of deadended (terminated) +states from the prepatched program, and a list of deadended states from the +postpatched program. Each of these states have constraints associated with +them that were collected as the program stepped through symbolic execution.
+Suppose that we take some state A from the prepatched run, and some state +B from the postpatched run. We say that A and B are compatible if the +constraints associated with the A and B are jointly satisfiable. In +pseudocode syntax, this roughly means that the following is True:
+is_sat(A.constraints & B.constraints)
+Recall that the input to our functions are symbolic variables, so the +set of constraints is in terms of these symbolic variables. We can think +of the constraints as creating a predicate that exactly determines the +subset of the input that leads to a specific state. Taking the conjunction +of the constraints is therefore equivalent to creating a predicate +that restricts the set of input values to the intersection of the input +set for state A and state B. If this predicate is satisfiable, then +this intersection of sets is nonempty, which means that there is at +least one concrete input that will cause the program to end in state A +in the prepatched program and state B in the postpatched program.
+Therefore the naive approach is to compare all pairs of terminal states +from the prepatched and postpatched and check for satisfiability. cozy +makes an optimization by using memoization, so in practice compatibility +checks over most programs should be fast. cozy is also capable of generating +concrete examples, which is useful for generating test cases and +walking through program execution.
+Let’s open a Python REPL and import the required libraries:
+import cozy
+from cozy.project import Project
+from cozy.directive import Assume, Assert
+import claripy
+Let’s begin by creating cozy projects for the two programs given +previously. A Project is a cozy class that encapsulates a single +program:
+proj_prepatched = Project("null_deref")
+proj_postpatched = Project("null_deref_patched")
+To execute the my_fun function, angr needs to know the function signature +of the functions. This information is typically not retained in the binary, +so we need to determine that with some other method. In this case we have +the source code, so we can add the function signature quite easily:
+proj_prepatched.add_prototype("my_fun", "void f(int *a)")
+proj_postpatched.add_prototype("my_fun", "void f(int *a)")
+We now need to create sessions from each project. A session is created
+from a specific project, and represents a single run of symbolic
+execution. Here we pass “my_fun” to the
+session() method, which indicates that
+we are going to be running the “my_fun” function:
sess_prepatched = proj_prepatched.session("my_fun")
+sess_postpatched = proj_postpatched.session("my_fun")
+Since we will only be comparing the my_fun function, we need to create +the symbolic value to pass to the functions:
+arg0 = claripy.BVS("num_arg", 64)
+The symbolic value arg0 has 64 bits because it represents a pointer +on a 64-bit architecture.
+Alternatively we could have used the cozy.primitives.sym_ptr() helper
+function to create the claripy symbolic variable:
import archinfo
+arg0 = cozy.primitives.sym_ptr(archinfo.ArchAMD64, "num_arg")
+We will now constrain arg0 to be either NULL or be equal to a valid memory +address in our two sessions. Currently angr has limited support for symbolic +memory addressing, so we will malloc space for our integers then constrain +arg0 accordingly:
+addr_prepatched = sess_prepatched.malloc(4) # integers are 4 bytes on the target arch
+sess_prepatched.add_constraints((arg0 == 0x0) | (arg0 == addr_prepatched))
+addr_postpatched = sess_postpatched.malloc(4)
+sess_postpatched.add_constraints((arg0 == 0x0) | (arg0 == addr_postpatched))
+So before any execution we have constrained arg0 to be either NULL
+(0x0) or a concrete 64-bit address returned by
+malloc().
cozy provides support for directives, which are attached to specific
+program instructions. Two basic directives that you should know about
+are cozy.directive.Assume and cozy.directive.Assert.
+Assume and assert function by pausing execution once a specific instruction
+is reached and adding constraints to the SMT solver. Assumes are used for
+adding preconditions, and are often set to be triggered at the start of
+functions. Asserts are triggered if there exists an input that will cause
+the assert to evaluate to false. Note that directives do not change the
+code being executed: they work more or less in the same way as debug
+breakpoints.
To demonstrate that a null dereference can occur in the prepatched binary +and not in the postpatched binary, let’s add asserts to specific addresses. +Running the binaries through a tool like Ghidra reveals that the NULL +dereference occurs at an offset of 0x10 from the start of my_fun in the +prepatched binary. At this point the address being dereferenced is stored +in the RAX register. Let’s create a directive that encodes these observations:
+mem_write_okay_prepatched = Assert.from_fun_offset(
+ project=proj_prepatched,
+ fun_name="my_fun",
+ offset=0x10,
+ condition_fun=lambda state: state.regs.rax != 0x0,
+ info_str="Dereferencing null pointer"
+ )
+When execution reaches my_fun+0x10, the evaluation will be halted and +cozy will pass the angr.SimState to the condition_fun and will check to see +if it is possible to find an input value that will trigger the condition. +Let’s add the directive to the prepatch session:
+sess_prepatched.add_directives(mem_write_okay_prepatched)
+Let’s invoke the prepatched my_fun with arg0 as the symbolic input via the
+run() method:
run_result = sess_prepatched.run([arg0])
+print(run_result)
+Which prints the following result that informs us that an assertion was triggered:
+RunResult(1 deadended, 0 errored, 1 asserts_failed, 0 assume_warnings, 0 postconditions_failed, 0 spinning)
+To view a report on what went wrong with the assertion, let’s create
+a report using the report_asserts_failed()
+method:
print(run_result.report([arg0]))
+Which prints off the human-readable report:
+Errored Report:
+No errored states
+
+Asserts Failed Report:
+Assert for address 0x401179 was triggered: <Bool int_arg_0_64 != 0x0>
+Dereferencing null pointer
+Here are 1 concrete input(s) for this particular assertion:
+1.
+ [<BV64 0x0>]
+
+Postconditions Failed Report:
+No postcondition failure triggered
+
+Spinning (Looping) States Report:
+No spinning states were reported
+As part of the report, cozy reports that the concretized input that leads to +this assertion being triggered occurs when the input argument is 0.
+Now let’s make another assert for the postpatched session and verify +that no NULL dereference occurs in the postpatch:
+mem_write_okay_postpatched = Assert.from_fun_offset(
+ project=proj_postpatched,
+ fun_name="my_fun",
+ offset=0x17,
+ condition_fun=lambda state: state.regs.rax != 0x0,
+ info_str="Dereferencing null pointer"
+ )
+sess_postpatched.add_directives(mem_write_okay_postpatched)
+run_result = sess_postpatched.run()
+print(run_result)
+In the console we see that no assertions were triggered:
+RunResult(1 deadended, 0 errored, 0 asserts_failed, 0 assume_warnings, 0 postconditions_failed)
+To compare two program executions, we need two cozy.project.RunResult objects.
+Let’s create fresh sessions and re-run without any directives attached. This time we will make use of
+primitive.sym_ptr_constraints() to generate the constraints instead of creating them manually:
sess_prepatched = proj_prepatched.session("my_fun")
+sess_postpatched = proj_postpatched.session("my_fun")
+addr_prepatched = sess_prepatched.malloc(cozy.constants.INT_SIZE)
+sess_prepatched.add_constraints(cozy.primitives.sym_ptr_constraints(arg0, addr_prepatched, can_be_null=True))
+addr_postpatched = sess_postpatched.malloc(cozy.constants.INT_SIZE)
+sess_postpatched.add_constraints(cozy.primitives.sym_ptr_constraints(arg0, addr_postpatched, can_be_null=True))
+Now let’s run both of our new sessions:
+prepatched_result = sess_prepatched.run([arg0])
+postpatched_result = sess_postpatched.run([arg0])
+We can inspect the results object to see how many states we are dealing with:
+print(prepatched_result)
+print(postpatched_result)
+This prints the following messages:
+RunResult(1 deadended, 0 errored, 0 asserts_failed, 0 assume_warnings, 0 postconditions_failed, 0 spinning)
+RunResult(2 deadended, 0 errored, 0 asserts_failed, 0 assume_warnings, 0 postconditions_failed, 0 spinning)
+We can now make a comparison between these two terminated results. Constructing a Comparison object is used to do +the comparison computation:
+comparison_results = cozy.analysis.Comparison(prepatched_result, postpatched_result, simplify=True)
+To view a human readable report, we can now call the cozy.analysis.Comparison.report() method, which
+will convert the Comparison to a human readable summary:
print(comparison_results.report([arg0]))
+We now see the human readable report
+ 1STATE PAIR (0, DEADENDED_STATE), (0, DEADENDED_STATE) are different
+ 2Memory difference detected for 0,0:
+ 3{'range(0x0, 0x4)': (<BV32 0x2a000000>, <BV32 0x0>)}
+ 4Instruction pointers for these memory writes:
+ 5{'range(0x0, 0x4)': (frozenset({<BV64 0x401179>}), frozenset())}
+ 6Register difference detected for 0,0:
+ 7{'eflags': (<BV64 0x0>, <BV64 0x44>), 'flags': (<BV64 0x0>, <BV64 0x44>), 'rflags': (<BV64 0x0>, <BV64 0x44>)}
+ 8Here are 1 concrete input(s) for this particular state pair:
+ 91.
+10 Input arguments: [<BV64 0x0>]
+11 Concrete mem diff: {'range(0x0, 0x4)': (<BV32 0x2a000000>, <BV32 0x0>)}
+12 Concrete reg diff: {'eflags': (<BV64 0x0>, <BV64 0x44>), 'flags': (<BV64 0x0>, <BV64 0x44>), 'rflags': (<BV64 0x0>, <BV64 0x44>)}
+13
+14STATE PAIR (0, DEADENDED_STATE), (1, DEADENDED_STATE) are different
+15The memory was equal for this state pair
+16Register difference detected for 0,1:
+17{'eflags': (<BV64 0x0>, <BV64 0x4>), 'flags': (<BV64 0x0>, <BV64 0x4>), 'rflags': (<BV64 0x0>, <BV64 0x4>)}
+18Here are 1 concrete input(s) for this particular state pair:
+191.
+20 Input arguments: [<BV64 0xc0000000>]
+21 Concrete reg diff: {'eflags': (<BV64 0x0>, <BV64 0x4>), 'flags': (<BV64 0x0>, <BV64 0x4>), 'rflags': (<BV64 0x0>, <BV64 0x4>)}
+22
+23There are no prepatched orphans
+24There are no postpatched orphans
+We can see that cozy found a diff between the 0th deadended +(terminated) state in the prepatched program (we will refer to this +state as s0) and the 0th deadended state in the postpatched program +(we will refer to this state as s0’). Together these two states form a +state pair, which is displayed on line 1 of the report. As we will see +from the following lines of the report, s0 represents the sole final +symbolic state for the prepatched function (there is only one path +through this function), and s0’ represents the final state for the +“false” branch of the postpatched function (i.e., the path that is +triggered by a NULL argument).
+Line 3 displays the memory addresses that are different. Contents of +memory for written ranges are mapped to a tuple containing the +symbolic bytes at those addresses as a (prepatched, postpatched) +tuple. In this case, memory at addresses 0x0 to 0x4 is 0x2a000000 in +s0 (because the prepatched function writes 0x2a = 42 to the NULL +address), and 0x0 in s0’ (because the NULL check prevents the write +from occurring).
+Line 5 tells the instruction pointer the program was at when it wrote +to those specific memory address ranges. Here we see that the +prepatched program was at the instruction 0x401179 when it wrote to +address 0x0, and the postpatched program never wrote to that address +(hence the empty frozenset).
+Line 7 gives the symbolic register difference between the states. As we can see, the flags registers +are different due to the presence of a branch in the postpatched program. As with the memory, each register +maps to a (prepatched, postpatched) tuple which gives the symbolic contents of the registers.
+Lines 8-12 gives concretized input that will cause the prepatched program to end in state s0 and +the postpatched program in state s0’. The input argument is concretized to 0x0 (aka NULL). Additionally since +the memory contents and register contents may be symbolic, we provide a concretized version of those as well.
+Lines 14-21 tells us that there is another diff for the state pair +(0,1). The second state in this pair represents the “true” branch +through the postpatched function. In this case we observe that the +only difference is in the flags registers, and that there are no +observable differences in memory. The concrete input argument for this +pair is when the input is non-NULL.
+The next lines describe any orphaned states - typically there will be none. An orphaned state is a state in which +there are no compatible pair states.
+Further examples on how to use cozy for some simple programs can be found at https://github.com/draperlaboratory/cozy/tree/main/examples
+Some of the default C library hooks provided by angr will not function properly with +comparitive symbolic execution, including joint concolic execution. The issue stems +from two different factors:
+1. Hooks may provide an incomplete implementation of the C library hooks, or the complete
+implementation may be disabled by default. For example, the strtok_r function’s
+more complete implementation may be disabled by default, and should be enabled by setting
+angr.SimState.libc.simple_strtok to False. Likewise the strstr libc function
+has a configuration option angr.SimState.libc.max_symbolic_strstr which is by
+default set to a very conservative value of 1.
2. The default angr hooks create fresh symbolic variables, and constrain these symbolic
+values by adding to the state’s constraints. This is problematic since in comparitive
+symbolic execution we assume that both programs are fed the same symbolic variables.
+Fortunately it is possible to eliminate the fresh symbolic variables in most cases. To see
+an example of how to do this, see our provided replacement hook for strlen at
+cozy.hooks.strlen.strlen.
In general, the best strategy for dealing with hooks is to be aware of their limitations,
+understand the configuration options found in angr.SimState.libc, and replace
+the default hooks when needed.
To replace a hook for a specific project, you may use the
+cozy.project.Project.hook_symbol() method.
Contents:
+In this example we will cover adding user defined types to the angr project as well as +visualizing our results with cozy. We will be using the AMP Hackathon Target 5 binaries, +which can be found in the examples folder in the cozy repository. There is no source +code available for these binaries, so some manual inspection of the assembly in your +preferred reverse engineering tool may be necessary.
+The micropatch bug in the Target 5 demo occurs during conversion of the temperature +value. Within the function we want replace the following logic:
+int32_t rover_process(RoverMessage_t* msg){
+ // ...
+ //convert Kelvin to Farhenheit.
+ temp = ( (temp - 273) * 1.8 ) + 32;
+ // ...
+}
+With this logic:
+int32_t rover_process(RoverMessage_t* msg){
+ // ...
+ //convert Celsius to Farhenheit.
+ temp = ( temp * 1.8 ) + 32;
+ // ...
+}
+To achieve this patch, we replaced the constant 273 in the original binary with 0.
+Let’s get started by making two cozy projects, one for each binary:
+proj_prepatched = cozy.project.Project('examples/amp_target5_hackathon/gs_data_processor')
+proj_postpatched = cozy.project.Project('examples/amp_target5_hackathon/gs_data_processor_draper_patched')
+Our next task will be to define the structs used by this function. The primary inputs +to this function is the temperature field and the cmd field. Let’s register these datatypes +with cozy:
+cozy.types.register_type('struct RoverData_t { int temp; unsigned int cmd; }', proj_prepatched.arch)
+rover_message_struct = cozy.types.register_type('struct RoverMessage_t { unsigned char header[8]; struct RoverData_t packetData; }', proj_prepatched.arch)
+We are now ready to add the type signature of the method we wish to analyze to the cozy project:
+proj_prepatched.add_prototype("rover_process", "int rover_process(struct RoverMessage_t *msg)")
+proj_postpatched.add_prototype("rover_process", "int rover_process(struct RoverMessage_t *msg)")
+Now let’s create two symbolic variables to represent the temp and cmd fields in the RoverData_t struct:
temp = claripy.BVS("temp", 32)
+cmd = claripy.BVS("cmd", 32)
+We now define a run function, which will run a prepatched or postpatched session:
+def run(sess: cozy.project.Session):
+ arg0 = sess.malloc(rover_message_struct.size)
+ sess.mem[arg0].struct.RoverMessage_t.packetData.temp = temp.reversed
+ sess.mem[arg0].struct.RoverMessage_t.packetData.cmd = cmd.reversed
+
+ return sess.run([arg0])
+In this case we are mutating the memory by changing the memory of the angr state before
+cozy runs. In this case we use angr’s API to mutate the temp and cmd fields. Since the
+incoming network packet uses network order endianness, we store temp.reversed and
+cmd.reversed to swap the endianness.
Let’s use our new run function to run the prepatched and postpatched session:
+prepatched_results = run(proj_prepatched.session("rover_process"))
+postpatched_results = run(proj_postpatched.session("rover_process"))
+Now we make the comparison between the two RunResult objects:
+comparison = cozy.analysis.Comparison(prepatched_results, postpatched_results)
+After which we can launch the visualization in our web browser. This should automatically +open a browser window which visualizes our results:
+cozy.execution_graph.visualize_comparison(proj_prepatched, proj_postpatched,
+ prepatched_results, postpatched_results,
+ comparison,
+ args={"temp": temp, "cmd": cmd},
+ num_examples=2, open_browser=True)
+| + c | ||
| + |
+ cozy | + |
| + |
+ cozy.__main__ | + |
| + |
+ cozy.analysis | + |
| + |
+ cozy.claripy_ext | + |
| + |
+ cozy.concolic | + |
| + |
+ cozy.concolic.exploration | + |
| + |
+ cozy.concolic.heuristics | + |
| + |
+ cozy.concolic.session | + |
| + |
+ cozy.concrete | + |
| + |
+ cozy.constants | + |
| + |
+ cozy.directive | + |
| + |
+ cozy.execution_graph | + |
| + |
+ cozy.functools_ext | + |
| + |
+ cozy.hooks | + |
| + |
+ cozy.hooks.strlen | + |
| + |
+ cozy.hooks.strncmp | + |
| + |
+ cozy.hooks.strtok_r | + |
| + |
+ cozy.log | + |
| + |
+ cozy.primitives | + |
| + |
+ cozy.project | + |
| + |
+ cozy.server | + |
| + |
+ cozy.session | + |
| + |
+ cozy.side_effect | + |
| + |
+ cozy.stubs | + |
| + |
+ cozy.terminal_state | + |
| + |
+ cozy.types | + |
+ Searching for multiple words only shows matches that contain + all words. +
+ + + + + + + + +Many programs of interest that we wish to simulate produce side effects, which we would like to be available for comparison in our analysis. +To enable this use case, cozy has a subsystem for producing IO side effects. Common examples of IO side effects we have found in example programs +include writing to stdout/stderr, writing to the network, or writing over a serial connection.
+Modeling IO side effects is typically straightforward, and can be accomplished by hooking side effect producing functions and instead redirecting +the side effect payload to a list attached to the current state. When a child state is forked from its parent, it obtains a copy of side effects +from its parent. cozy keeps track of IO side effects over different channels (ie, a channel for stdout, network, etc.) and attempts to +intelligently align side effects in the visualization interface.
+Note that by default, angr automatically concretizes data written to stdout/stderr. cozy side effects keeps the data symbolic and avoids the concretization. +In this way cozy’s side effects interface is superior to the angr default.
+The primary function to take a look at is cozy.side_effect.perform(). The first argument is the angr.SimState that the side effect
+will attach to. This argument can be obtained by hooking a side effect function, whose angr.SimProcedure.run() method takes in a
+angr.SimState object. Alternatively you can set a breakpoint using cozy.directive.Breakpoint and obtain the angr.SimState
+object in the breakpoint’s breakpoint_fun callback.
Here is an example of the use of cozy.side_effect.perform() in a custom angr.SimProcedure hook:
# Here we are hooking a function called process_command,
+# so we need to make a class that inherits from SimProcedure
+class process_command(angr.SimProcedure):
+ def run(self, cmd_str):
+ strlen = angr.SIM_PROCEDURES["libc"]["strlen"]
+ max_len = self.state.solver.max(self.inline_call(strlen, cmd_str).ret_expr)
+ # Here we construct the side effect payload. Here it is a bunch of symbolic data.
+ cmd = [self.state.memory.load(cmd_str + i, 1) for i in range(max_len)]
+ def concrete_post_processor(concrete_cmd):
+ return [chr(r.concrete_value) for r in concrete_cmd]
+ cozy.side_effect.perform(self.state, "process_command", cmd, concrete_post_processor=concrete_post_processor)
+The second argument is the side effect channel. Different types of side effects should be performed over different channels. For example, +you may have a channel for networked output and a channel for stdout.
+The third argument is the side effect body. The body must be a mixture of string-keyed Python dictionaries, Python lists, Python tuples, +claripy concrete values, and claripy symbolic values. This should represent the payload of the side effect.
+The fourth argument is an optional post processing function to apply to concretized versions of the side effect’s body if post processing is required. +In this example we use the Python chr function to convert the integer to Python characters, which will be shown in the visualization +user interface.
+The fifth argument is an optional label used to aid alignment in the user interface. For example, if you have multiple sites that produce +side effects on the same channel, you will want to label the different sites with different labels. This aids the alignment algorithm to intelligently +compare the produced side effects. One possible label is the code address location that the side effect is produced at.
+