From 9f106a801884a3dfb4f817e9bfcf928272a5ea06 Mon Sep 17 00:00:00 2001
From: raz0r <me@raz0r.name>
Date: Thu, 14 Dec 2017 20:01:37 +0300
Subject: [PATCH] add basic detection of faulty PRNGs

Currently the module looks for common predictable state variables in ether transfer constraints

Sample output:
==== Weak random ====
Type: Warning
Contract: WeakRandom
Function name: _function_0xe9874106
PC address: 1285
In the function '_function_0xe9874106' the following predictable state
variables are used to determine Ether recipient:
- block.coinbase

TODO:
- block.blockhash(block.number-1)
- block.blockhash(some_block_past_256_blocks_from_now)==0
- external source of random numbers (e.g. Oraclize)
---
 mythril/analysis/modules/weak_random.py | 72 +++++++++++++++++++++++++
 solidity_examples/weak_random.sol       | 49 +++++++++++++++++
 2 files changed, 121 insertions(+)
 create mode 100644 mythril/analysis/modules/weak_random.py
 create mode 100644 solidity_examples/weak_random.sol

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);
+    }
+}