From 49023f25fe181993a0644ca5a63e541ef75da9c0 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Tue, 3 Dec 2019 21:26:57 +0000 Subject: [PATCH] move everything to plugin --- mythril/laser/ethereum/cfg.py | 24 -- .../implementations/plugin_annotations.py | 5 +- .../plugins/implementations/state_merge.py | 211 +++++++++++++++++- mythril/laser/ethereum/state/account.py | 32 --- mythril/laser/ethereum/state/constraints.py | 6 - mythril/laser/ethereum/state/global_state.py | 2 + mythril/laser/ethereum/state/world_state.py | 136 +---------- 7 files changed, 213 insertions(+), 203 deletions(-) diff --git a/mythril/laser/ethereum/cfg.py b/mythril/laser/ethereum/cfg.py index 915c65c8..08be0c85 100644 --- a/mythril/laser/ethereum/cfg.py +++ b/mythril/laser/ethereum/cfg.py @@ -86,30 +86,6 @@ class Node: code=code, ) - def merge_nodes(self, node: "Node", constraints: Constraints): - """ - Merges two nodes - :param node: The node to be merged - :param constraints: The merged constraints - :return: - """ - self.states += node.states - self.uid = get_new_gbl_id() - self.flags |= node.flags - self.constraints = constraints - - def check_merge_condition(self, node: "Node"): - """ - Checks whether two nodes are merge-able or not - :param node: The other node to be merged - :return: - """ - return ( - self.function_name == node.function_name - and self.contract_name == node.contract_name - and self.start_addr == node.start_addr - ) - class Edge: """The respresentation of a call graph edge.""" diff --git a/mythril/laser/ethereum/plugins/implementations/plugin_annotations.py b/mythril/laser/ethereum/plugins/implementations/plugin_annotations.py index 160df6cb..2a4705ba 100644 --- a/mythril/laser/ethereum/plugins/implementations/plugin_annotations.py +++ b/mythril/laser/ethereum/plugins/implementations/plugin_annotations.py @@ -66,7 +66,7 @@ class DependencyAnnotation(StateAnnotation): class WSDependencyAnnotation(StateAnnotation): """Dependency Annotation for World state - This world state annotation maintains a stack of state annotations. + This world state annotation maintains a stack of state annotations. It is used to transfer individual state annotations from one transaction to the next. """ @@ -89,3 +89,6 @@ class WSDependencyAnnotation(StateAnnotation): def merge_annotations(self, other: "WSDependencyAnnotation"): for a1, a2 in zip(self.annotations_stack, other.annotations_stack): a1.merge_annotation(a2) + + def persist_to_world_state(self) -> bool: + return True diff --git a/mythril/laser/ethereum/plugins/implementations/state_merge.py b/mythril/laser/ethereum/plugins/implementations/state_merge.py index c4824ca9..1b400490 100644 --- a/mythril/laser/ethereum/plugins/implementations/state_merge.py +++ b/mythril/laser/ethereum/plugins/implementations/state_merge.py @@ -1,12 +1,18 @@ from copy import copy -from typing import Dict, List +from typing import Dict, List, Tuple, cast from mythril.laser.ethereum.svm import LaserEVM from mythril.laser.ethereum.plugins.plugin import LaserPlugin from mythril.laser.ethereum.state.world_state import WorldState +from mythril.laser.ethereum.state.account import Account +from mythril.laser.ethereum.cfg import Node, get_new_gbl_id +from mythril.laser.ethereum.state.constraints import Constraints +from mythril.laser.smt import symbol_factory, Array, BitVec, If, Or, And, Not, Bool import logging log = logging.getLogger(__name__) +CONSTRAINT_DIFFERENCE_LIMIT = 15 + class StateMerge(LaserPlugin): def initialize(self, symbolic_vm: LaserEVM): @@ -59,24 +65,213 @@ class StateMerge(LaserPlugin): ) svm.open_states = new_states - @staticmethod - def check_merge_condition(state1: WorldState, state2: WorldState): + def check_merge_condition(self, state1: WorldState, state2: WorldState): """ Check whether two world states can be merged :param state1: :param state2: :return: whether the states can be merged or not """ - basic_condition = state1.check_merge_condition(state2) + basic_condition = self.check_ws_merge_condition(state1, state2) return basic_condition - @staticmethod - def merge_states(state1: WorldState, state2: WorldState) -> WorldState: + def merge_states(self, state1: WorldState, state2: WorldState): """ Merge state2 into state1 :param state1: The state to be merged into :param state2: The state which is merged into state1 :return: """ - state1.merge_states(state2) - return state1 + + # Merge constraints + state1.constraints, condition1, _ = self._merge_constraints( + state1.constraints, state2.constraints + ) + + # Merge balances + state1.balances = cast(Array, If(condition1, state1.balances, state2.balances)) + state1.starting_balances = cast( + Array, If(condition1, state1.starting_balances, state2.starting_balances) + ) + + # Merge accounts + for address, account in state2.accounts.items(): + if address not in state1._accounts: + state1.put_account(account) + else: + self.merge_accounts( + state1._accounts[address], account, condition1, state1.balances + ) + + # Merge annotations + self._merge_annotations(state1, state2) + + # Merge Node + self.merge_nodes(state1.node, state2.node, state1.constraints) + + @staticmethod + def _merge_constraints( + constraints1: Constraints, constraints2: Constraints + ) -> Tuple[Constraints, Bool, Bool]: + dict1, dict2 = {}, {} + for constraint in constraints1: + dict1[constraint] = True + for constraint in constraints2: + dict2[constraint] = True + c1, c2 = symbol_factory.Bool(True), symbol_factory.Bool(True) + new_constraint1, new_constraint2 = ( + symbol_factory.Bool(True), + symbol_factory.Bool(True), + ) + same_constraints = Constraints() + for key in dict1: + if key not in dict2: + c1 = And(c1, key) + if Not(key) not in dict2: + new_constraint1 = And(new_constraint1, key) + else: + same_constraints.append(key) + for key in dict2: + if key not in dict1: + c2 = And(c2, key) + if Not(key) not in dict1: + new_constraint2 = And(new_constraint2, key) + else: + same_constraints.append(key) + merge_constraints = same_constraints + [Or(new_constraint1, new_constraint2)] + return merge_constraints, c1, c2 + + @staticmethod + def _check_constraint_merge( + constraints1: Constraints, constraints2: Constraints + ) -> bool: + dict1, dict2 = {}, {} + for constraint in constraints1: + dict1[constraint] = True + for constraint in constraints2: + dict2[constraint] = True + c1, c2 = 0, 0 + for key in dict1: + if key not in dict2 and Not(key) not in dict2: + c1 += 1 + for key in dict2: + if key not in dict1 and Not(key) not in dict1: + c2 += 1 + if c1 + c2 > CONSTRAINT_DIFFERENCE_LIMIT: + return False + return True + + def _check_merge_annotations(self, state1: WorldState, state2: WorldState): + """ + + :param state: + :return: + """ + if len(state2.annotations) != len(state1._annotations): + return False + if ( + self._check_constraint_merge(state1.constraints, state2.constraints) + is False + ): + return False + for v1, v2 in zip(state2.annotations, state1._annotations): + if v1.check_merge_annotation(v2) is False: # type: ignore + return False + return True + + @staticmethod + def _merge_annotations(state1: "WorldState", state2: "WorldState"): + """ + + :param state: + :return: + """ + for v1, v2 in zip(state1.annotations, state2.annotations): + v1.merge_annotations(v2) # type: ignore + + def check_ws_merge_condition(self, state1: WorldState, state2: WorldState): + """ + Checks whether we can merge these states or not + """ + if state1.node and not self.check_node_merge_condition( + state1.node, state2.node + ): + return False + + for address, account in state2.accounts.items(): + if ( + address in state1._accounts + and self.check_account_merge_condition( + state1._accounts[address], account + ) + is False + ): + return False + if not self._check_merge_annotations(state1, state2): + return False + + return True + + @staticmethod + def merge_accounts( + account1: Account, + account2: Account, + path_condition: Bool, + merged_balance: Array, + ): + """ + Checks the merge-ability + :param account1: The account to merge with + :param account2: The second account to merge + :param path_condition: The constraint for this account + :param merged_balance: The merged balance + :return: + """ + assert ( + account1.nonce == account2.nonce + and account1.deleted == account2.deleted + and account1.code.bytecode == account2.code.bytecode + ) + + account1._balances = merged_balance + account1.balance = lambda: account1._balances[account1.address] + account1.storage.merge_storage(account2.storage, path_condition) + + @staticmethod + def check_account_merge_condition(account1: Account, account2: Account): + """ + Checks whether we can merge accounts or not + """ + return ( + account1.nonce == account2.nonce + and account1.deleted == account2.deleted + and account1.code.bytecode == account2.code.bytecode + ) + + @staticmethod + def merge_nodes(node1: Node, node2: Node, constraints: Constraints): + """ + Merges two nodes + :param node1: The node to be merged + :param node2: The other node to be merged + :param constraints: The merged constraints + :return: + """ + node1.states += node2.states + node1.uid = get_new_gbl_id() + node1.flags |= node2.flags + node1.constraints = constraints + + @staticmethod + def check_node_merge_condition(node1: Node, node2: Node): + """ + Checks whether two nodes are merge-able or not + :param node1: The node to be merged + :param node2: The other node to be merged + :return: Boolean, True if we can merge + """ + return ( + node1.function_name == node2.function_name + and node1.contract_name == node2.contract_name + and node1.start_addr == node2.start_addr + ) diff --git a/mythril/laser/ethereum/state/account.py b/mythril/laser/ethereum/state/account.py index afe77c1c..d988110e 100644 --- a/mythril/laser/ethereum/state/account.py +++ b/mythril/laser/ethereum/state/account.py @@ -186,38 +186,6 @@ class Account: ) self._balances[self.address] += balance - def merge_accounts( - self, account: "Account", path_condition: Bool, merged_balance: Array - ): - """ - Checks the merge-ability - :param account: The account to merge with - :param path_condition: The constraint for this account - :param merged_balance: The merged balance - :return: - """ - assert ( - self.nonce == account.nonce - and self.deleted == account.deleted - and self.code.bytecode == account.code.bytecode - ) - - self._balances = merged_balance - self.balance = lambda: self._balances[self.address] - self.storage.merge_storage(account.storage, path_condition) - - def check_merge_condition(self, account: "Account"): - """ - Checks whether we can merge or not - :param account: The account to check merge-ability with - :return: True if we can merge them - """ - return ( - self.nonce == account.nonce - and self.deleted == account.deleted - and self.code.bytecode == account.code.bytecode - ) - @property def as_dict(self) -> Dict: """ diff --git a/mythril/laser/ethereum/state/constraints.py b/mythril/laser/ethereum/state/constraints.py index 8772e868..b72b58c4 100644 --- a/mythril/laser/ethereum/state/constraints.py +++ b/mythril/laser/ethereum/state/constraints.py @@ -30,12 +30,6 @@ class Constraints(list): self._default_timeout = 100 self._is_possible = is_possible - def compress(self): - constraint = True - for c in self[:]: - constraint = And(constraint, c) - return constraint - @property def is_possible(self) -> bool: """ diff --git a/mythril/laser/ethereum/state/global_state.py b/mythril/laser/ethereum/state/global_state.py index 6774bde0..747cc9e0 100644 --- a/mythril/laser/ethereum/state/global_state.py +++ b/mythril/laser/ethereum/state/global_state.py @@ -140,6 +140,8 @@ class GlobalState: :param annotation: """ self._annotations.append(annotation) + if annotation.persist_to_world_state: + self.world_state.annotate(annotation) @property def annotations(self) -> List[StateAnnotation]: diff --git a/mythril/laser/ethereum/state/world_state.py b/mythril/laser/ethereum/state/world_state.py index c69a0d6a..a4793967 100644 --- a/mythril/laser/ethereum/state/world_state.py +++ b/mythril/laser/ethereum/state/world_state.py @@ -9,15 +9,10 @@ from ethereum.utils import mk_contract_address from mythril.laser.ethereum.state.account import Account from mythril.laser.ethereum.state.annotation import StateAnnotation from mythril.laser.ethereum.state.constraints import Constraints -from mythril.laser.ethereum.plugins.implementations.plugin_annotations import ( - WSDependencyAnnotation, -) if TYPE_CHECKING: from mythril.laser.ethereum.cfg import Node -CONSTRAINT_DIFFERENCE_LIMIT = 15 - class WorldState: """The WorldState class represents the world state as described in the @@ -26,7 +21,7 @@ class WorldState: def __init__( self, transaction_sequence=None, - annotations: List[WSDependencyAnnotation] = None, + annotations: List[StateAnnotation] = None, constraints: Constraints = None, ) -> None: """Constructor for the world state. Initializes the accounts record. @@ -41,130 +36,7 @@ class WorldState: self.node = None # type: Optional['Node'] self.transaction_sequence = transaction_sequence or [] - self._annotations = annotations or [] # type: List[WSDependencyAnnotation] - - def merge_states(self, state: "WorldState"): - """ - Merge this state with "state" - :param state: The state to be merged with - :return: - """ - - # Merge constraints - self.constraints, condition1, _ = self._merge_constraints(state.constraints) - - # Merge balances - self.balances = cast(Array, If(condition1, self.balances, state.balances)) - self.starting_balances = cast( - Array, If(condition1, self.starting_balances, state.starting_balances) - ) - - # Merge accounts - for address, account in state.accounts.items(): - if address not in self._accounts: - self.put_account(account) - else: - self._accounts[address].merge_accounts( - account, condition1, self.balances - ) - - # Merge annotations - self._merge_annotations(state) - - # Merge Node - self.node.merge_nodes(state.node, self.constraints) - - def _merge_constraints( - self, constraints: Constraints - ) -> Tuple[Constraints, Bool, Bool]: - dict1, dict2 = {}, {} - for constraint in self.constraints: - dict1[constraint] = True - for constraint in constraints: - dict2[constraint] = True - c1, c2 = symbol_factory.Bool(True), symbol_factory.Bool(True) - new_constraint1, new_constraint2 = ( - symbol_factory.Bool(True), - symbol_factory.Bool(True), - ) - same_constraints = Constraints() - for key in dict1: - if key not in dict2: - c1 = And(c1, key) - if Not(key) not in dict2: - new_constraint1 = And(new_constraint1, key) - else: - same_constraints.append(key) - for key in dict2: - if key not in dict1: - c2 = And(c2, key) - if Not(key) not in dict1: - new_constraint2 = And(new_constraint2, key) - else: - same_constraints.append(key) - merge_constraints = same_constraints + [Or(new_constraint1, new_constraint2)] - return merge_constraints, c1, c2 - - def _check_constraint_merge(self, constraints: Constraints) -> bool: - dict1, dict2 = {}, {} - for constraint in self.constraints: - dict1[constraint] = True - for constraint in constraints: - dict2[constraint] = True - c1, c2 = 0, 0 - for key in dict1: - if key not in dict2 and Not(key) not in dict2: - c1 += 1 - for key in dict2: - if key not in dict1 and Not(key) not in dict1: - c2 += 1 - if c1 + c2 > CONSTRAINT_DIFFERENCE_LIMIT: - return False - return True - - def _check_merge_annotations(self, state: "WorldState"): - """ - - :param state: - :return: - """ - if len(state.annotations) != len(self._annotations): - return False - if self._check_constraint_merge(state.constraints) is False: - return False - for v1, v2 in zip(state.annotations, self._annotations): - if v1.check_merge_annotation(v2) is False: - return False - return True - - def _merge_annotations(self, state: "WorldState"): - """ - - :param state: - :return: - """ - for v1, v2 in zip(state.annotations, self._annotations): - v1.merge_annotations(v2) - - def check_merge_condition(self, state: "WorldState"): - """ - Checks whether we can merge this state with "state" or not - :param state: The state to check the merge-ability with - :return: True if we can merge them - """ - if self.node and not self.node.check_merge_condition(state.node): - return False - - for address, account in state.accounts.items(): - if ( - address in self._accounts - and self._accounts[address].check_merge_condition(account) is False - ): - return False - if not self._check_merge_annotations(state): - return False - - return True + self._annotations = annotations or [] # type: List[StateAnnotation] @property def accounts(self): @@ -272,7 +144,7 @@ class WorldState: new_account.storage = storage self.put_account(new_account) - def annotate(self, annotation: WSDependencyAnnotation) -> None: + def annotate(self, annotation: StateAnnotation) -> None: """ :param annotation: @@ -280,7 +152,7 @@ class WorldState: self._annotations.append(annotation) @property - def annotations(self) -> List[WSDependencyAnnotation]: + def annotations(self) -> List[StateAnnotation]: """ :return: