From 5a38737edea4684cf4080c9dda4fe35c7caf43fc Mon Sep 17 00:00:00 2001 From: feliam Date: Mon, 5 Feb 2018 15:00:05 -0300 Subject: [PATCH] Fix sha3 (#703) * the fix * Add default example sha3 when unknown * Review * Remove IF statement on potentially symbolic value --- manticore/ethereum.py | 6 ++++++ manticore/platforms/evm.py | 30 ++++++++++++++++++++++++++---- 2 files changed, 32 insertions(+), 4 deletions(-) diff --git a/manticore/ethereum.py b/manticore/ethereum.py index 0da2e9e..a6f8bd3 100644 --- a/manticore/ethereum.py +++ b/manticore/ethereum.py @@ -361,6 +361,7 @@ class ABI(object): padding = 32 - byte_size # for 160 value = arithmetic_simplifier(Operators.CONCAT(size, *map(Operators.ORD, data[offset+padding:offset+padding+byte_size]))) return simplify(value) + if ty == u'uint256': return get_uint(256, offset), offset+32 elif ty in (u'bool', u'uint8'): @@ -1155,6 +1156,11 @@ class ManticoreEVM(Manticore): summary.write("\n") + if blockchain._sha3: + summary.write("Known hashes:\n") + for key, value in blockchain._sha3.items(): + summary.write('%s::%x\n'%(key.encode('hex'), value)) + if is_something_symbolic: summary.write('\n\n(*) Example solution given. Value is symbolic and may take other values\n') diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index f61fd26..ccbdaa5 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -1504,7 +1504,7 @@ class EVM(Eventful): value = sha3.keccak_256(buf).hexdigest() value = int('0x'+value,0) self._publish('on_concrete_sha3', buf, value) - logger.info("Found new SHA3 example %r -> %x", buf, value) + logger.info("Found a concrete SHA3 example %r -> %x", buf, value) return value @@ -1924,7 +1924,7 @@ class EVMWorld(Platform): self.forward_events_from(self.current) self.subscribe('on_concrete_sha3', self._concrete_sha3_callback) - def _concrete_sha3_callback(self,buf, value): + def _concrete_sha3_callback(self, buf, value): if buf in self._sha3: assert self._sha3[buf] == value self._sha3[buf] = value @@ -2444,27 +2444,49 @@ class EVMWorld(Platform): self._publish('on_symbolic_sha3', data, self._sha3.items()) results = [] + + #If know_hashes is true then there is a _known_ solution for the hash known_hashes = False for key, value in self._sha3.items(): + assert not any( map(issymbolic, key)) cond = compare_buffers(key, data) if solver.can_be_true(self._constraints, cond): results.append((cond, value)) known_hashes = Operators.OR(cond, known_hashes) + #results contains all the possible and known solutions + + #If known_hashes can be False then data can take at least one concrete + #value of which we do not know a hash for. + + #Calculate the sha3 of one extra example solution and add this as a + #potential result + #This is an incomplete result: + # Intead of choosing one single extra concrete solution we should save + # the state and when a new sha3 example is found load it back and try + #the new concretization for sha3. + with self._constraints as temp_cs: if solver.can_be_true(temp_cs, Operators.NOT(known_hashes)): temp_cs.add(Operators.NOT(known_hashes)) + #a_buffer is different from all strings we know a hash for a_buffer = solver.get_value(temp_cs, data) cond = compare_buffers(a_buffer, data) + #Get the sha3 for a_buffer + a_value = int(sha3.keccak_256(a_buffer).hexdigest(), 16) + #add the new sha3 pair to the known_hashes and result + self._publish('on_concrete_sha3', a_buffer, a_value) + results.append((cond, a_value)) known_hashes = Operators.OR(cond, known_hashes) - + if solver.can_be_true(self._constraints, known_hashes): self._constraints.add(known_hashes) value = 0 #never used for cond, sha in results: value = Operators.ITEBV(256, cond, sha, value) else: - raise TerminateState() + raise TerminateState("Unknown hash") self.current._push(value) self.current.pc += self.current.instruction.size +