diff --git a/mythril/analysis/modules/weak_random.py b/mythril/analysis/modules/weak_random.py new file mode 100644 index 00000000..d716f51f --- /dev/null +++ b/mythril/analysis/modules/weak_random.py @@ -0,0 +1,72 @@ +from z3 import * +from mythril.analysis.ops import * +from mythril.analysis import solver +from mythril.analysis.report import Issue +from mythril.exceptions import UnsatError +import logging + +''' +MODULE DESCRIPTION: + +Check for CALLs that send >0 Ether as a result of computation based on predictable state variables such as +block.coinbase, block.gaslimit, block.timestamp, block.number + +TODO: +- block.blockhash(block.number-1) +- block.blockhash(some_block_past_256_blocks_from_now)==0 +- external source of random numbers (e.g. Oraclize) +''' + + +def execute(statespace): + issues = [] + + for call in statespace.calls: + + if ("callvalue" in str(call.value)): + logging.debug("[WEAK_RANDOM] Skipping refund function") + continue + + # We're only interested in calls that send Ether + + if call.value.type == VarType.CONCRETE: + if call.value.val == 0: + continue + + + + description = "In the function '" + call.node.function_name + "' " + description += "the following predictable state variables are used to determine Ether recipient:\n" + + # Look for predictable state variables in node & call recipient constraints + + vars = ["coinbase", "gaslimit", "timestamp", "number"] + + found = [] + for var in vars: + for constraint in call.node.constraints: + if var in str(constraint): + found.append(var) + break + else: + if var in str(call.to): + found.append(var) + + if len(found): + for item in found: + description += "- block.{}\n".format(item) + try: + model = solver.get_model(call.node.constraints) + logging.debug("[WEAK_RANDOM] MODEL: " + str(model)) + + for d in model.decls(): + logging.debug("[WEAK_RANDOM] main model: %s = 0x%x" % (d.name(), model[d].as_long())) + + issue = Issue(call.node.module_name, call.node.function_name, call.addr, "Weak random", "Warning", + description) + issues.append(issue) + + except UnsatError: + logging.debug("[WEAK_RANDOM] no model found") + + return issues diff --git a/solidity_examples/weak_random.sol b/solidity_examples/weak_random.sol new file mode 100644 index 00000000..88fc4e12 --- /dev/null +++ b/solidity_examples/weak_random.sol @@ -0,0 +1,49 @@ +pragma solidity ^0.4.16; + +contract WeakRandom { + struct Contestant { + address addr; + uint gameId; + } + + uint public constant prize = 2.5 ether; + uint public constant totalTickets = 50; + uint public constant pricePerTicket = prize / totalTickets; + + uint public gameId = 1; + uint public nextTicket = 0; + mapping (uint => Contestant) public contestants; + + function () payable public { + uint moneySent = msg.value; + + while (moneySent >= pricePerTicket && nextTicket < totalTickets) { + uint currTicket = nextTicket++; + contestants[currTicket] = Contestant(msg.sender, gameId); + moneySent -= pricePerTicket; + } + + if (nextTicket == totalTickets) { + chooseWinner(); + } + + // Send back leftover money + if (moneySent > 0) { + msg.sender.transfer(moneySent); + } + } + + function chooseWinner() private { + address seed1 = contestants[uint(block.coinbase) % totalTickets].addr; + address seed2 = contestants[uint(msg.sender) % totalTickets].addr; + uint seed3 = block.difficulty; + bytes32 randHash = keccak256(seed1, seed2, seed3); + + uint winningNumber = uint(randHash) % totalTickets; + address winningAddress = contestants[winningNumber].addr; + + gameId++; + nextTicket = 0; + winningAddress.transfer(prize); + } +}