From 7cc9a3de8fd7ec73da620405d2295c9d3d5dc303 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Sat, 16 Mar 2019 13:05:41 +0530 Subject: [PATCH] Add the BitWise instructions --- mythril/laser/ethereum/gas.py | 8 ++ mythril/laser/ethereum/instructions.py | 42 +++++++ mythril/laser/smt/__init__.py | 1 + mythril/laser/smt/bitvec.py | 21 ++++ tests/instructions/sar_test.py | 148 +++++++++++++++++++++++++ tests/instructions/shl_test.py | 123 ++++++++++++++++++++ tests/instructions/shr_test.py | 125 +++++++++++++++++++++ 7 files changed, 468 insertions(+) create mode 100644 tests/instructions/sar_test.py create mode 100644 tests/instructions/shl_test.py create mode 100644 tests/instructions/shr_test.py diff --git a/mythril/laser/ethereum/gas.py b/mythril/laser/ethereum/gas.py index 8fae5f53..7e283d15 100644 --- a/mythril/laser/ethereum/gas.py +++ b/mythril/laser/ethereum/gas.py @@ -62,6 +62,9 @@ OPCODE_GAS = { "XOR": (3, 3), "NOT": (3, 3), "BYTE": (3, 3), + "SHL": (3, 3), + "SHR": (3, 3), + "SAR": (3, 3), "SHA3": ( 30, 30 + 6 * 8, @@ -80,6 +83,7 @@ OPCODE_GAS = { "GASPRICE": (2, 2), "EXTCODESIZE": (700, 700), "EXTCODECOPY": (700, 700 + 3 * 768), # https://ethereum.stackexchange.com/a/47556 + "EXTCODEHASH": (400, 400), "RETURNDATASIZE": (2, 2), "RETURNDATACOPY": (3, 3), "BLOCKHASH": (20, 20), @@ -176,6 +180,10 @@ OPCODE_GAS = { "LOG3": (4 * 375, 4 * 375 + 8 * 32), "LOG4": (5 * 375, 5 * 375 + 8 * 32), "CREATE": (32000, 32000), + "CREATE2": ( + 32000, + 32000, + ), # TODO: The gas value is dynamic, to be done while implementing create2 "CALL": (700, 700 + 9000 + 25000), "NATIVE_COST": calculate_native_gas, "CALLCODE": (700, 700 + 9000 + 25000), diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index cd5e5cfa..e7d9ebc4 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -26,6 +26,7 @@ from mythril.laser.smt import ( Bool, Or, Not, + LShR, ) from mythril.laser.smt import symbol_factory @@ -464,6 +465,33 @@ class Instruction: global_state.mstate.stack.append(0 if s1 == 0 else URem(s0, s1)) return [global_state] + @StateTransition() + def shl_(self, global_state: GlobalState) -> List[GlobalState]: + shift, value = ( + util.pop_bitvec(global_state.mstate), + util.pop_bitvec(global_state.mstate), + ) + global_state.mstate.stack.append(value << shift) + return [global_state] + + @StateTransition() + def shr_(self, global_state: GlobalState) -> List[GlobalState]: + shift, value = ( + util.pop_bitvec(global_state.mstate), + util.pop_bitvec(global_state.mstate), + ) + global_state.mstate.stack.append(LShR(value, shift)) + return [global_state] + + @StateTransition() + def sar_(self, global_state: GlobalState) -> List[GlobalState]: + shift, value = ( + util.pop_bitvec(global_state.mstate), + util.pop_bitvec(global_state.mstate), + ) + global_state.mstate.stack.append(value >> shift) + return [global_state] + @StateTransition() def smod_(self, global_state: GlobalState) -> List[GlobalState]: """ @@ -1082,6 +1110,20 @@ class Instruction: return [global_state] + @StateTransition + def extcodehash_(self, global_state: GlobalState) -> List[GlobalState]: + """ + + :param global_state: + :return: List of global states possible, list of size 1 in this case + """ + # TODO: To be implemented + address = global_state.mstate.stack.pop() + global_state.mstate.stack.append( + global_state.new_bitvec("extcodehash_{}".format(str(address)), 256) + ) + return [global_state] + @StateTransition() def extcodecopy_(self, global_state: GlobalState) -> List[GlobalState]: """ diff --git a/mythril/laser/smt/__init__.py b/mythril/laser/smt/__init__.py index f46a8968..d849d0c4 100644 --- a/mythril/laser/smt/__init__.py +++ b/mythril/laser/smt/__init__.py @@ -13,6 +13,7 @@ from mythril.laser.smt.bitvec import ( BVAddNoOverflow, BVMulNoOverflow, BVSubNoUnderflow, + LShR, ) from mythril.laser.smt.bitvecfunc import BitVecFunc from mythril.laser.smt.expression import Expression, simplify diff --git a/mythril/laser/smt/bitvec.py b/mythril/laser/smt/bitvec.py index 00b519a7..381dc03f 100644 --- a/mythril/laser/smt/bitvec.py +++ b/mythril/laser/smt/bitvec.py @@ -211,6 +211,22 @@ class BitVec(Expression[z3.BitVecRef]): # MYPY: fix complaints due to z3 overriding __eq__ return Bool(cast(z3.BoolRef, self.raw != other.raw), annotations=union) + def __lshift__(self, other: Union[int, "BitVec"]) -> "BitVec": + if not isinstance(other, BitVec): + return BitVec( + self.raw << other, annotations=self.annotations + ) + union = self.annotations + other.annotations + return BitVec(self.raw << other.raw, annotations=union) + + def __rshift__(self, other: Union[int, "BitVec"]) -> "BitVec": + if not isinstance(other, BitVec): + return BitVec( + self.raw >> other, annotations=self.annotations + ) + union = self.annotations + other.annotations + return BitVec(self.raw >> other.raw, annotations=union) + def _comparison_helper( a: BitVec, b: BitVec, operation: Callable, default_value: bool, inputs_equal: bool @@ -254,6 +270,11 @@ def _arithmetic_helper(a: BitVec, b: BitVec, operation: Callable) -> BitVec: return BitVec(raw, annotations=union) +def LShR(a, b): + union = a.annotations + b.annotations + return BitVec(z3.LShR(a.raw, b.raw), annotations=union) + + def If(a: Union[Bool, bool], b: Union[BitVec, int], c: Union[BitVec, int]) -> BitVec: """Create an if-then-else expression. diff --git a/tests/instructions/sar_test.py b/tests/instructions/sar_test.py new file mode 100644 index 00000000..b618582f --- /dev/null +++ b/tests/instructions/sar_test.py @@ -0,0 +1,148 @@ +import pytest + +from mythril.disassembler.disassembly import Disassembly +from mythril.laser.ethereum.state.environment import Environment +from mythril.laser.ethereum.state.account import Account +from mythril.laser.ethereum.state.machine_state import MachineState +from mythril.laser.ethereum.state.global_state import GlobalState +from mythril.laser.ethereum.state.world_state import WorldState +from mythril.laser.ethereum.instructions import Instruction +from mythril.laser.ethereum.transaction.transaction_models import MessageCallTransaction +from mythril.laser.smt import symbol_factory, simplify + + +def get_state(): + active_account = Account("0x0", code=Disassembly("60606040")) + environment = Environment(active_account, None, None, None, None, None) + state = GlobalState(None, environment, None, MachineState(gas_limit=8000000)) + state.transaction_stack.append( + (MessageCallTransaction(world_state=WorldState(), gas_limit=8000000), None) + ) + return state + + +BVV = symbol_factory.BitVecVal +BV = symbol_factory.BitVecSym + +test_data = ( + ([BVV(-1, 256), BVV(1, 256)], BVV(-1, 256)), + ([BVV(23, 256), BVV(257, 256)], BVV(0, 256)), + ([BVV(23, 256), BVV(30, 256)], BVV(23 >> 30, 256)), + ([BVV(-10, 256), BVV(10, 256)], BVV(-1, 256)), + ([BV("a", 256), BV("b", 256)], BV("a", 256) >> BV("b", 256)), +) + + +@pytest.mark.parametrize("inputs,output", test_data) +def test_sar(inputs, output): + # Arrange + state = get_state() + + state.mstate.stack = inputs + instruction = Instruction("sar", dynamic_loader=None) + + # Act + new_state = instruction.evaluate(state)[0] + + # Assert + assert simplify(new_state.mstate.stack[-1]) == output + + +@pytest.mark.parametrize( + # Test cases from https://github.com/ethereum/EIPs/blob/master/EIPS/eip-145.md#sar-arithmetic-shift-right + "val1, val2, expected ", + ( + ( + "0x0000000000000000000000000000000000000000000000000000000000000001", + "0x00", + "0x0000000000000000000000000000000000000000000000000000000000000001", + ), + ( + "0x0000000000000000000000000000000000000000000000000000000000000001", + "0x01", + "0x0000000000000000000000000000000000000000000000000000000000000000", + ), + ( + "0x8000000000000000000000000000000000000000000000000000000000000000", + "0x01", + "0xc000000000000000000000000000000000000000000000000000000000000000", + ), + ( + "0x8000000000000000000000000000000000000000000000000000000000000000", + "0xff", + "0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff", + ), + ( + "0x8000000000000000000000000000000000000000000000000000000000000000", + "0x0100", + "0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff", + ), + ( + "0x8000000000000000000000000000000000000000000000000000000000000000", + "0x0101", + "0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff", + ), + ( + "0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff", + "0x00", + "0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff", + ), + ( + "0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff", + "0x01", + "0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff", + ), + ( + "0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff", + "0xff", + "0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff", + ), + ( + "0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff", + "0x0100", + "0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff", + ), + ( + "0x0000000000000000000000000000000000000000000000000000000000000000", + "0x01", + "0x0000000000000000000000000000000000000000000000000000000000000000", + ), + ( + "0x4000000000000000000000000000000000000000000000000000000000000000", + "0xfe", + "0x0000000000000000000000000000000000000000000000000000000000000001", + ), + ( + "0x7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff", + "0xf8", + "0x000000000000000000000000000000000000000000000000000000000000007f", + ), + ( + "0x7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff", + "0xfe", + "0x0000000000000000000000000000000000000000000000000000000000000001", + ), + ( + "0x7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff", + "0xff", + "0x0000000000000000000000000000000000000000000000000000000000000000", + ), + ( + "0x7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff", + "0x0100", + "0x0000000000000000000000000000000000000000000000000000000000000000", + ), + ), +) +def test_concrete_sar(val1, val2, expected): + # Arrange + state = get_state() + state.mstate.stack = [BVV(int(val1, 16), 256), BVV(int(val2, 16), 256)] + expected = BVV(int(expected, 16), 256) + instruction = Instruction("sar", dynamic_loader=None) + + # Act + new_state = instruction.evaluate(state)[0] + + # Assert + assert simplify(new_state.mstate.stack[-1]) == expected diff --git a/tests/instructions/shl_test.py b/tests/instructions/shl_test.py new file mode 100644 index 00000000..0e36c088 --- /dev/null +++ b/tests/instructions/shl_test.py @@ -0,0 +1,123 @@ +import pytest + +from mythril.disassembler.disassembly import Disassembly +from mythril.laser.ethereum.state.environment import Environment +from mythril.laser.ethereum.state.account import Account +from mythril.laser.ethereum.state.machine_state import MachineState +from mythril.laser.ethereum.state.global_state import GlobalState +from mythril.laser.ethereum.state.world_state import WorldState +from mythril.laser.ethereum.instructions import Instruction +from mythril.laser.ethereum.transaction.transaction_models import MessageCallTransaction +from mythril.laser.smt import symbol_factory, simplify + + +def get_state(): + active_account = Account("0x0", code=Disassembly("60606040")) + environment = Environment(active_account, None, None, None, None, None) + state = GlobalState(None, environment, None, MachineState(gas_limit=8000000)) + state.transaction_stack.append( + (MessageCallTransaction(world_state=WorldState(), gas_limit=8000000), None) + ) + return state + + +BVV = symbol_factory.BitVecVal +BV = symbol_factory.BitVecSym + +test_data = ( + ([BVV(2, 256), BVV(2, 256)], BVV(8, 256)), + ([BVV(23, 256), BVV(257, 256)], BVV(0, 256)), + ([BVV(23, 256), BVV(30, 256)], BVV(23 * (1 << 30), 256)), + ([BV("a", 256), BVV(270, 256)], 0), + ([BV("a", 256), BV("b", 256)], BV("a", 256) << BV("b", 256)), +) + + +@pytest.mark.parametrize("inputs,output,", test_data) +def test_shl(inputs, output): + # Arrange + state = get_state() + + state.mstate.stack = inputs + instruction = Instruction("shl", dynamic_loader=None) + + # Act + new_state = instruction.evaluate(state)[0] + + # Assert + assert simplify(new_state.mstate.stack[-1]) == output + + +@pytest.mark.parametrize( + # Testcases from https://github.com/ethereum/EIPs/blob/master/EIPS/eip-145.md#shl-shift-left + "val1, val2, expected", + ( + ( + "0x0000000000000000000000000000000000000000000000000000000000000001", + "0x00", + "0x0000000000000000000000000000000000000000000000000000000000000001", + ), + ( + "0x0000000000000000000000000000000000000000000000000000000000000001", + "0x01", + "0x0000000000000000000000000000000000000000000000000000000000000002", + ), + ( + "0x0000000000000000000000000000000000000000000000000000000000000001", + "0xff", + "0x8000000000000000000000000000000000000000000000000000000000000000", + ), + ( + "0x0000000000000000000000000000000000000000000000000000000000000001", + "0x0100", + "0x0000000000000000000000000000000000000000000000000000000000000000", + ), + ( + "0x0000000000000000000000000000000000000000000000000000000000000001", + "0x0101", + "0x0000000000000000000000000000000000000000000000000000000000000000", + ), + ( + "0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff", + "0x00", + "0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff", + ), + ( + "0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff", + "0x01", + "0xfffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe", + ), + ( + "0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff", + "0xff", + "0x8000000000000000000000000000000000000000000000000000000000000000", + ), + ( + "0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff", + "0x0100", + "0x0000000000000000000000000000000000000000000000000000000000000000", + ), + ( + "0x0000000000000000000000000000000000000000000000000000000000000000", + "0x01", + "0x0000000000000000000000000000000000000000000000000000000000000000", + ), + ( + "0x7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff", + "0x01", + "0xfffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe", + ), + ), +) +def test_concrete_shl(val1, val2, expected): + # Arrange + state = get_state() + state.mstate.stack = [BVV(int(val1, 16), 256), BVV(int(val2, 16), 256)] + expected = BVV(int(expected, 16), 256) + instruction = Instruction("shl", dynamic_loader=None) + + # Act + new_state = instruction.evaluate(state)[0] + + # Assert + assert simplify(new_state.mstate.stack[-1]) == expected diff --git a/tests/instructions/shr_test.py b/tests/instructions/shr_test.py new file mode 100644 index 00000000..aaf370e2 --- /dev/null +++ b/tests/instructions/shr_test.py @@ -0,0 +1,125 @@ +import pytest + +from mythril.disassembler.disassembly import Disassembly +from mythril.laser.ethereum.state.environment import Environment +from mythril.laser.ethereum.state.account import Account +from mythril.laser.ethereum.state.machine_state import MachineState +from mythril.laser.ethereum.state.global_state import GlobalState +from mythril.laser.ethereum.state.world_state import WorldState +from mythril.laser.ethereum.instructions import Instruction +from mythril.laser.ethereum.transaction.transaction_models import MessageCallTransaction +from mythril.laser.smt import symbol_factory, simplify, LShR + + +def get_state(): + active_account = Account("0x0", code=Disassembly("60606040")) + environment = Environment(active_account, None, None, None, None, None) + state = GlobalState(None, environment, None, MachineState(gas_limit=8000000)) + state.transaction_stack.append( + (MessageCallTransaction(world_state=WorldState(), gas_limit=8000000), None) + ) + return state + + +BVV = symbol_factory.BitVecVal +BV = symbol_factory.BitVecSym + +test_data = ( + ([BVV(33, 256), BVV(4, 256)], BVV(2, 256)), + ([BVV(1 << 100, 256), BVV(257, 256)], BVV(0, 256)), + ([BVV(23233, 256), BVV(10, 256)], BVV(23233 // (1 << 10), 256)), + ([BV("a", 256), BVV(270, 256)], 0), + ( + [BV("a", 256), BV("b", 256)], + LShR(BV("a", 256), BV("b", 256)), + ), # Current approximate specs +) + + +@pytest.mark.parametrize("inputs,output,", test_data) +def test_shr(inputs, output): + # Arrange + state = get_state() + + state.mstate.stack = inputs + instruction = Instruction("shr", dynamic_loader=None) + + # Act + new_state = instruction.evaluate(state)[0] + + # Assert + assert simplify(new_state.mstate.stack[-1]) == output + + +@pytest.mark.parametrize( + # Cases: https://github.com/ethereum/EIPs/blob/master/EIPS/eip-145.md#shr-logical-shift-right + "val1, val2, expected", + ( + ( + "0x0000000000000000000000000000000000000000000000000000000000000001", + "0x00", + "0x0000000000000000000000000000000000000000000000000000000000000001", + ), + ( + "0x0000000000000000000000000000000000000000000000000000000000000001", + "0x01", + "0x0000000000000000000000000000000000000000000000000000000000000000", + ), + ( + "0x8000000000000000000000000000000000000000000000000000000000000000", + "0x01", + "0x4000000000000000000000000000000000000000000000000000000000000000", + ), + ( + "0x8000000000000000000000000000000000000000000000000000000000000000", + "0xff", + "0x0000000000000000000000000000000000000000000000000000000000000001", + ), + ( + "0x8000000000000000000000000000000000000000000000000000000000000000", + "0x0100", + "0x0000000000000000000000000000000000000000000000000000000000000000", + ), + ( + "0x8000000000000000000000000000000000000000000000000000000000000000", + "0x0101", + "0x0000000000000000000000000000000000000000000000000000000000000000", + ), + ( + "0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff", + "0x00", + "0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff", + ), + ( + "0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff", + "0x01", + "0x7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff", + ), + ( + "0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff", + "0xff", + "0x0000000000000000000000000000000000000000000000000000000000000001", + ), + ( + "0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff", + "0x0100", + "0x0000000000000000000000000000000000000000000000000000000000000000", + ), + ( + "0x0000000000000000000000000000000000000000000000000000000000000000", + "0x01", + "0x0000000000000000000000000000000000000000000000000000000000000000", + ), + ), +) +def test_concrete_shr(val1, val2, expected): + state = get_state() + state.mstate.stack = [BVV(int(val1, 16), 256), BVV(int(val2, 16), 256)] + expected = BVV(int(expected, 16), 256) + instruction = Instruction("shr", dynamic_loader=None) + + # Act + new_state = instruction.evaluate(state)[0] + + # Assert + assert simplify(new_state.mstate.stack[-1]) == expected