mirror of https://github.com/ConsenSys/mythril
Nathan
5 years ago
committed by
GitHub
commit
ed06c3148e
@ -0,0 +1,117 @@ |
||||
from ethereum import utils |
||||
from mythril.laser.smt import ( |
||||
BitVec, |
||||
Function, |
||||
URem, |
||||
symbol_factory, |
||||
ULE, |
||||
And, |
||||
ULT, |
||||
Bool, |
||||
Or, |
||||
) |
||||
from typing import Dict, Tuple, List |
||||
|
||||
TOTAL_PARTS = 10 ** 40 |
||||
PART = (2 ** 256 - 1) // TOTAL_PARTS |
||||
INTERVAL_DIFFERENCE = 10 ** 30 |
||||
hash_matcher = "fffffff" # This is usually the prefix for the hash in the output |
||||
|
||||
|
||||
class KeccakFunctionManager: |
||||
""" |
||||
A bunch of uninterpreted functions are considered like keccak256_160 ,... |
||||
where keccak256_160 means the input of keccak256() is 160 bit number. |
||||
the range of these functions are constrained to some mutually disjoint intervals |
||||
All the hashes modulo 64 are 0 as we need a spread among hashes for array type data structures |
||||
All the functions are kind of one to one due to constraint of the existence of inverse |
||||
for each encountered input. |
||||
For more info https://files.sri.inf.ethz.ch/website/papers/sp20-verx.pdf |
||||
""" |
||||
|
||||
def __init__(self): |
||||
self.store_function = {} # type: Dict[int, Tuple[Function, Function]] |
||||
self.interval_hook_for_size = {} # type: Dict[int, int] |
||||
self._index_counter = TOTAL_PARTS - 34534 |
||||
self.quick_inverse = {} # type: Dict[BitVec, BitVec] # This is for VMTests |
||||
|
||||
@staticmethod |
||||
def find_concrete_keccak(data: BitVec) -> BitVec: |
||||
""" |
||||
Calculates concrete keccak |
||||
:param data: input bitvecval |
||||
:return: concrete keccak output |
||||
""" |
||||
keccak = symbol_factory.BitVecVal( |
||||
int.from_bytes( |
||||
utils.sha3(data.value.to_bytes(data.size() // 8, byteorder="big")), |
||||
"big", |
||||
), |
||||
256, |
||||
) |
||||
return keccak |
||||
|
||||
def get_function(self, length: int) -> Tuple[Function, Function]: |
||||
""" |
||||
Returns the keccak functions for the corresponding length |
||||
:param length: input size |
||||
:return: tuple of keccak and it's inverse |
||||
""" |
||||
try: |
||||
func, inverse = self.store_function[length] |
||||
except KeyError: |
||||
func = Function("keccak256_{}".format(length), length, 256) |
||||
inverse = Function("keccak256_{}-1".format(length), 256, length) |
||||
self.store_function[length] = (func, inverse) |
||||
return func, inverse |
||||
|
||||
@staticmethod |
||||
def get_empty_keccak_hash() -> BitVec: |
||||
""" |
||||
returns sha3("") |
||||
:return: |
||||
""" |
||||
val = 89477152217924674838424037953991966239322087453347756267410168184682657981552 |
||||
return symbol_factory.BitVecVal(val, 256) |
||||
|
||||
def create_keccak(self, data: BitVec) -> Tuple[BitVec, Bool]: |
||||
""" |
||||
Creates Keccak of the data |
||||
:param data: input |
||||
:return: Tuple of keccak and the condition it should satisfy |
||||
""" |
||||
length = data.size() |
||||
func, inverse = self.get_function(length) |
||||
|
||||
condition = self._create_condition(func_input=data) |
||||
self.quick_inverse[func(data)] = data |
||||
return func(data), condition |
||||
|
||||
def _create_condition(self, func_input: BitVec) -> Bool: |
||||
""" |
||||
Creates the constraints for hash |
||||
:param func_input: input of the hash |
||||
:return: condition |
||||
""" |
||||
length = func_input.size() |
||||
func, inv = self.get_function(length) |
||||
try: |
||||
index = self.interval_hook_for_size[length] |
||||
except KeyError: |
||||
self.interval_hook_for_size[length] = self._index_counter |
||||
index = self._index_counter |
||||
self._index_counter -= INTERVAL_DIFFERENCE |
||||
|
||||
lower_bound = index * PART |
||||
upper_bound = lower_bound + PART |
||||
|
||||
cond = And( |
||||
inv(func(func_input)) == func_input, |
||||
ULE(symbol_factory.BitVecVal(lower_bound, 256), func(func_input)), |
||||
ULT(func(func_input), symbol_factory.BitVecVal(upper_bound, 256)), |
||||
URem(func(func_input), symbol_factory.BitVecVal(64, 256)) == 0, |
||||
) |
||||
return cond |
||||
|
||||
|
||||
keccak_function_manager = KeccakFunctionManager() |
||||
@ -0,0 +1,25 @@ |
||||
from typing import cast |
||||
import z3 |
||||
|
||||
from mythril.laser.smt.bitvec import BitVec |
||||
|
||||
|
||||
class Function: |
||||
"""An uninterpreted function.""" |
||||
|
||||
def __init__(self, name: str, domain: int, value_range: int): |
||||
"""Initializes an uninterpreted function. |
||||
|
||||
:param name: Name of the Function |
||||
:param domain: The domain for the Function (10 -> all the values that a bv of size 10 could take) |
||||
:param value_range: The range for the values of the function (10 -> all the values that a bv of size 10 could take) |
||||
""" |
||||
self.domain = z3.BitVecSort(domain) |
||||
self.range = z3.BitVecSort(value_range) |
||||
self.raw = z3.Function(name, self.domain, self.range) |
||||
|
||||
def __call__(self, item: BitVec) -> BitVec: |
||||
"""Function accessor, item can be symbolic.""" |
||||
return BitVec( |
||||
cast(z3.BitVecRef, self.raw(item.raw)), annotations=item.annotations |
||||
) |
||||
@ -0,0 +1,138 @@ |
||||
from mythril.laser.smt import Solver, symbol_factory, And |
||||
from mythril.laser.ethereum.keccak_function_manager import keccak_function_manager |
||||
import z3 |
||||
import pytest |
||||
|
||||
|
||||
@pytest.mark.parametrize( |
||||
"input1, input2, expected", |
||||
[ |
||||
(symbol_factory.BitVecVal(100, 8), symbol_factory.BitVecVal(101, 8), z3.unsat), |
||||
(symbol_factory.BitVecVal(100, 8), symbol_factory.BitVecVal(100, 16), z3.unsat), |
||||
(symbol_factory.BitVecVal(100, 8), symbol_factory.BitVecVal(100, 8), z3.sat), |
||||
( |
||||
symbol_factory.BitVecSym("N1", 256), |
||||
symbol_factory.BitVecSym("N2", 256), |
||||
z3.sat, |
||||
), |
||||
( |
||||
symbol_factory.BitVecVal(100, 256), |
||||
symbol_factory.BitVecSym("N1", 256), |
||||
z3.sat, |
||||
), |
||||
( |
||||
symbol_factory.BitVecVal(100, 8), |
||||
symbol_factory.BitVecSym("N1", 256), |
||||
z3.unsat, |
||||
), |
||||
], |
||||
) |
||||
def test_keccak_basic(input1, input2, expected): |
||||
s = Solver() |
||||
|
||||
o1, c1 = keccak_function_manager.create_keccak(input1) |
||||
o2, c2 = keccak_function_manager.create_keccak(input2) |
||||
s.add(And(c1, c2)) |
||||
|
||||
s.add(o1 == o2) |
||||
assert s.check() == expected |
||||
|
||||
|
||||
def test_keccak_symbol_and_val(): |
||||
""" |
||||
check keccak(100) == keccak(n) && n == 10 |
||||
:return: |
||||
""" |
||||
s = Solver() |
||||
hundred = symbol_factory.BitVecVal(100, 256) |
||||
n = symbol_factory.BitVecSym("n", 256) |
||||
o1, c1 = keccak_function_manager.create_keccak(hundred) |
||||
o2, c2 = keccak_function_manager.create_keccak(n) |
||||
s.add(And(c1, c2)) |
||||
s.add(o1 == o2) |
||||
s.add(n == symbol_factory.BitVecVal(10, 256)) |
||||
assert s.check() == z3.unsat |
||||
|
||||
|
||||
def test_keccak_complex_eq(): |
||||
""" |
||||
check for keccak(keccak(b)*2) == keccak(keccak(a)*2) && a != b |
||||
:return: |
||||
""" |
||||
s = Solver() |
||||
a = symbol_factory.BitVecSym("a", 160) |
||||
b = symbol_factory.BitVecSym("b", 160) |
||||
o1, c1 = keccak_function_manager.create_keccak(a) |
||||
o2, c2 = keccak_function_manager.create_keccak(b) |
||||
s.add(And(c1, c2)) |
||||
two = symbol_factory.BitVecVal(2, 256) |
||||
o1 = two * o1 |
||||
o2 = two * o2 |
||||
o1, c1 = keccak_function_manager.create_keccak(o1) |
||||
o2, c2 = keccak_function_manager.create_keccak(o2) |
||||
|
||||
s.add(And(c1, c2)) |
||||
s.add(o1 == o2) |
||||
s.add(a != b) |
||||
|
||||
assert s.check() == z3.unsat |
||||
|
||||
|
||||
def test_keccak_complex_eq2(): |
||||
""" |
||||
check for keccak(keccak(b)*2) == keccak(keccak(a)*2) |
||||
This isn't combined with prev test because incremental solving here requires extra-extra work |
||||
(solution is literally the opposite of prev one) so it will take forever to solve. |
||||
:return: |
||||
""" |
||||
s = Solver() |
||||
a = symbol_factory.BitVecSym("a", 160) |
||||
b = symbol_factory.BitVecSym("b", 160) |
||||
o1, c1 = keccak_function_manager.create_keccak(a) |
||||
o2, c2 = keccak_function_manager.create_keccak(b) |
||||
s.add(And(c1, c2)) |
||||
two = symbol_factory.BitVecVal(2, 256) |
||||
o1 = two * o1 |
||||
o2 = two * o2 |
||||
o1, c1 = keccak_function_manager.create_keccak(o1) |
||||
o2, c2 = keccak_function_manager.create_keccak(o2) |
||||
|
||||
s.add(And(c1, c2)) |
||||
s.add(o1 == o2) |
||||
|
||||
assert s.check() == z3.sat |
||||
|
||||
|
||||
def test_keccak_simple_number(): |
||||
""" |
||||
check for keccak(b) == 10 |
||||
:return: |
||||
""" |
||||
s = Solver() |
||||
a = symbol_factory.BitVecSym("a", 160) |
||||
ten = symbol_factory.BitVecVal(10, 256) |
||||
o, c = keccak_function_manager.create_keccak(a) |
||||
|
||||
s.add(c) |
||||
s.add(ten == o) |
||||
|
||||
assert s.check() == z3.unsat |
||||
|
||||
|
||||
def test_keccak_other_num(): |
||||
""" |
||||
check keccak(keccak(a)*2) == b |
||||
:return: |
||||
""" |
||||
s = Solver() |
||||
a = symbol_factory.BitVecSym("a", 160) |
||||
b = symbol_factory.BitVecSym("b", 256) |
||||
o, c = keccak_function_manager.create_keccak(a) |
||||
two = symbol_factory.BitVecVal(2, 256) |
||||
o = two * o |
||||
s.add(c) |
||||
o, c = keccak_function_manager.create_keccak(o) |
||||
s.add(c) |
||||
s.add(b == o) |
||||
|
||||
assert s.check() == z3.sat |
||||
Loading…
Reference in new issue