[WIP] Formal Verification of SafetyChecker

packages/contracts/contracts/optimistic-ethereum/ovm/SafetyChecker.sol

@@ -1,12 +1,11 @@
 pragma solidity ^0.5.0;
 pragma experimental ABIEncoderV2;
 
-/* Contract Imports */
-import { ExecutionManager } from "./ExecutionManager.sol";
-
 /* Library Imports */
 import { ContractResolver } from "../utils/resolvers/ContractResolver.sol";
 
+//import { console } from "@nomiclabs/buidler/console.sol";
+
 /**
  * @title SafetyChecker
  * @notice Safety Checker contract used to check whether or not bytecode is
@@ -15,29 +14,19 @@ import { ContractResolver } from "../utils/resolvers/ContractResolver.sol";
  *              2. All CALLs are to the Execution Manager and have no value.
  */
 contract SafetyChecker is ContractResolver {
-    /*
-     * Contract Variables
-     */
-
-    uint256 public opcodeWhitelistMask;
-
-
     /*
      * Constructor
      */
 
     /**
      * @param _addressResolver Address of the AddressResolver contract.
-     * @param _opcodeWhitelistMask Whitelist mask of allowed opcodes.
      */
     constructor(
-        address _addressResolver,
-        uint256 _opcodeWhitelistMask
+        address _addressResolver
     )
         public
         ContractResolver(_addressResolver)
     {
-        opcodeWhitelistMask = _opcodeWhitelistMask;
     }
 
 
@@ -63,136 +52,102 @@ contract SafetyChecker is ContractResolver {
         view
         returns (bool)
     {
-        bool seenJUMP = false;
-        bool insideUnreachableCode = false;
-        uint256 ops = 0;
-        for (uint256 pc = 0; pc < _bytecode.length; pc++) {
+        // autogenerated by gen_safety_checker_constants.py
+        /*uint256[8] memory skip = [
+          uint256(0x0001010101010101010101010000000001010101010101010101010101010000),
+          uint256(0x0100000000000000000000000000000000000000010101010101000000010100),
+          uint256(0x0000000000000000000000000000000001010101000000010101010100000000),
+          uint256(0x0203040500000000000000000000000000000000000000000000000000000000),
+          uint256(0x0101010101010101010101010101010101010101010101010101010101010101),
+          uint256(0x0101010101000000000000000000000000000000000000000000000000000000),
+          uint256(0x0000000000000000000000000000000000000000000000000000000000000000),
+          uint256(0x0000000000000000000000000000000000000000000000000000000000000000)];*/
+        uint256 _opcodeProcMask = ~uint256(0xffffffffffffffffffffffe000000000fffffffff070ffff9c0ffffec000f001);
+        uint256 _opcodeStopMask = ~uint256(0x6008000000000000000000000000000000000000004000000000000000000001);
+        uint256 _opcodePushMask = ~uint256(0xffffffff000000000000000000000000);
+
+        uint256 codeLength;
+        uint256 _pc;
+        assembly {
+            _pc := add(_bytecode, 0x20)
+        }
+        codeLength = _pc + _bytecode.length;
+        do {
             // current opcode: 0x00...0xff
-            uint256 op = uint8(_bytecode[pc]);
-
-            // PUSH##
-            if (op >= 0x60 && op <= 0x7f) {
-                // subsequent bytes are not opcodes. Skip them.
-                pc += (op - 0x5f);
+            uint256 op;
+
+            // inline assembly removes the extra add + bounds check
+            assembly {
+                let tmp := mload(_pc)
+
+                // this works, it just isn't fast
+                let mpc := 0
+
+                // this is fast
+                /*mpc := add(mpc, byte(0, mload(add(skip, byte(mpc, tmp)))))
+                mpc := add(mpc, byte(0, mload(add(skip, byte(mpc, tmp)))))
+                mpc := add(mpc, byte(0, mload(add(skip, byte(mpc, tmp)))))
+                mpc := add(mpc, byte(0, mload(add(skip, byte(mpc, tmp)))))
+                mpc := add(mpc, byte(0, mload(add(skip, byte(mpc, tmp)))))
+                mpc := add(mpc, byte(0, mload(add(skip, byte(mpc, tmp)))))*/
+
+                // footer
+                _pc := add(_pc, mpc)
+                op := byte(mpc, tmp)
             }
-            // If we're in between a STOP or REVERT or JUMP and a JUMPDEST
-            if (insideUnreachableCode) {
-                // JUMPDEST
-                if (op == 0x5b) {
-                    // this bytecode is now reachable via JUMP or JUMPI
-                    insideUnreachableCode = false;
-                }
-            } else {
-                // check that opcode is whitelisted (using the whitelist bit mask)
-                uint256 opBit = 1 << op;
-                if (opcodeWhitelistMask & opBit != opBit) {
-                    // encountered a non-whitelisted opcode!
-                    return false;
-                }
-                // append this opcode to a list of ops
-                ops <<= 8;
-                ops |= op;
-                // [0x57, 0x56, 0x00, 0xfd, 0xfe, 0xf3, 0xf1] all have handlers
-                if (opBit & 0x600a00000000000000000000000000000000000000c000000000000000000001 != 0) {
-                    // JUMPI
-                    if (op == 0x57) {
-                        // We can now reach all JUMPDESTs
-                        seenJUMP = true;
-                    // JUMP
-                    } else if (op == 0x56) {
-                        // We can now reach all JUMPDESTs
-                        seenJUMP = true;
-                        // we are now inside unreachable code until we hit a JUMPDEST!
-                        insideUnreachableCode = true;
-                    // STOP or REVERT or INVALID or RETURN (see safety checker docs in wiki for more info)
-                    } else if (op == 0x00 || op == 0xfd || op == 0xfe || op == 0xf3) {
-                        // If we can't jump to JUMPDESTs, then all remaining bytecode is unreachable
-                        if (!seenJUMP) {
-                            return true;
-                        }
-                        // We are now inside unreachable code until we hit a JUMPDEST!
-                        insideUnreachableCode = true;
-                    // CALL
-                    } else if (op == 0xf1) {
-                        // Minimum 4 total ops:
-                        // 1. PUSH1 value
-                        // 2. PUSH20 execution manager address
-                        // 3. PUSH or DUP gas
-                        // 4. CALL
-
-                        // if opIndex < 3, there would be 0s here, so we don't need the check
-                        uint256 gasOp = (ops >> 8) & 0xFF;
-                        uint256 addressOp = (ops >> 16) & 0xFF;
-                        uint256 valueOp = (ops >> 24) & 0xFF;
-                        if (
-                            gasOp < 0x60 || // PUSHes are 0x60...0x7f
-                            gasOp > 0x8f || // DUPs are 0x80...0x8f
-                            addressOp != 0x73 || // address must be set with a PUSH20
-                            valueOp != 0x60 // value must be set with a PUSH1
-                        ) {
-                            return false;
-                        } else {
-                            uint256 pushedBytes;
-                            // gas is set with a PUSH##
-                            if (gasOp >= 0x60 && gasOp <= 0x7f) {
-                                pushedBytes = gasOp - 0x5f;
-                            }
-
-                            // 23 is from 1 + PUSH20 + 20 bytes of address + PUSH or DUP gas
-                            byte callValue = _bytecode[pc - (23 + pushedBytes)];
-
-                            // 21 is from 1 + 19 bytes of address + PUSH or DUP gas
-                            address callAddress = toAddress(_bytecode, (pc - (21 + pushedBytes)));
-
-                            // CALL is made to the execution manager with msg.value of 0 ETH
-                            if (callAddress != address(resolveExecutionManager()) || callValue != 0 ) {
-                                return false;
-                            }
+
+            // + push opcodes
+            // + stop opcodes [STOP(0x00),JUMP(0x56),RETURN(0xf3),REVERT(0xfd),INVALID(0xfe)]
+            // + caller opcode CALLER(0x33) (which is technically on the blacklist)
+            // + blacklisted opcodes
+            uint256 opBit = 1 << op;
+            if (opBit & _opcodeProcMask == 0) {
+                if (opBit & _opcodePushMask == 0) {
+                    // subsequent bytes are not opcodes. Skip them.
+                    _pc += (op - 0x5e);
+                    // all pushes are valid opcodes
+                    continue;
+                } else if (opBit & _opcodeStopMask == 0) {
+                    // STOP or JUMP or RETURN or REVERT or INVALID (see safety checker docs in wiki for more info)
+                    // We are now inside unreachable code until we hit a JUMPDEST!
+                    do {
+                        _pc++;
+                        assembly {
+                            op := byte(0, mload(_pc))
                         }
+                        if (op == 0x5b) break;
+                        if ((1 << op) & _opcodePushMask == 0) _pc += (op - 0x5f);
+                    } while (_pc < codeLength);
+                    // op is 0x5b, so we don't continue here since the _pc++ is fine
+                } else if (op == 0x33) {
+                    // Sequence around CALLER must be:
+                    // 1. CALLER (execution manager address) <-- We are here
+                    // 2. PUSH1 0x0
+                    // 3. SWAP1
+                    // 4. GAS (gas for call)
+                    // 5. CALL
+
+                    uint256 ops;
+                    assembly {
+                        ops := shr(208, mload(_pc))
                     }
+
+                    // allowed = CALLER PUSH1 0x0 SWAP1 GAS CALL
+                    if (ops != 0x336000905af1) {
+                        //console.log('Encountered a bad call');
+                        return false;
+                    }
+
+                    _pc += 6;
+                    continue;
+                } else {
+                    // encountered a non-whitelisted opcode!
+                    //console.log('Encountered a non-whitelisted opcode (in decimal):', op, "at location", _pc);
+                    return false;
                 }
             }
-        }
+            _pc++;
+        } while (_pc < codeLength);
         return true;
     }
-
-
-    /*
-     * Internal Functions
-     */
-
-    /**
-     * Converts the 20 bytes at _start of _bytes into an address.
-     * @param _bytes The bytes to extract the address from.
-     * @param _start The start index from which to extract the address from
-     *               (e.g. 0 if _bytes starts with the address).
-     * @return Bytes converted to an address.
-     */
-    function toAddress(
-        bytes memory _bytes,
-        uint256 _start
-    )
-        internal
-        pure
-        returns (address addr)
-    {
-        require(_bytes.length >= (_start + 20), "Addresses must be at least 20 bytes");
-
-        assembly {
-            addr := mload(add(add(_bytes, 20), _start))
-        }
-    }
-
-
-    /*
-     * Contract Resolution
-     */
-
-    function resolveExecutionManager()
-        internal
-        view
-        returns (ExecutionManager)
-    {
-        return ExecutionManager(resolveContract("ExecutionManager"));
-    }
 }

packages/contracts/contracts/optimistic-ethereum/ovm/test-helpers/StubSafetyChecker.sol

@@ -13,7 +13,7 @@ contract StubSafetyChecker is SafetyChecker {
 
     constructor()
         public
-        SafetyChecker(address(0x0), 0)
+        SafetyChecker(address(0x0))
     {}
 
 

packages/contracts/contracts/optimistic-ethereum/ovm/verify/.gitignore

@@ -0,0 +1,3 @@
+mcore_*
+__pycache__
+*.pyc

packages/contracts/contracts/optimistic-ethereum/ovm/verify/gen_safety_checker_constants.py

@@ -0,0 +1,62 @@
+#!/usr/bin/env python3
+# pip3 install pyevmasm
+from pyevmasm import instruction_tables
+
+#print(instruction_tables.keys())
+
+def asm(x):
+  return [instruction_tables['istanbul'][i].opcode for i in x]
+
+push_opcodes = asm(["PUSH%d" % i for i in range(1,33)])
+stop_opcodes = asm(["STOP", "JUMP", "RETURN", "REVERT", "INVALID"])
+blacklist_ops = set([
+  "ADDRESS", "BALANCE", "BLOCKHASH",
+  "CALL", "CALLCODE", "CALLER", "CHAINID", "COINBASE",
+  "CREATE", "CREATE2", "DELEGATECALL", "DIFFICULTY",
+  "EXTCODESIZE", "EXTCODECOPY", "EXTCODEHASH",
+  "GASLIMIT", "GASPRICE", "NUMBER",
+  "ORIGIN", "SELFBALANCE", "SELFDESTRUCT",
+  "SLOAD", "SSTORE", "STATICCALL", "TIMESTAMP"])
+blacklist_opcodes = asm(list(blacklist_ops))
+whitelist_opcodes = []
+for x in instruction_tables['istanbul']:
+  if x.name not in blacklist_ops:
+    whitelist_opcodes.append(x.opcode)
+
+pushmask = 0
+for x in push_opcodes:
+  pushmask |= 1 << x
+
+stopmask = 0
+for x in stop_opcodes:
+  stopmask |= 1 << x
+
+stoplist = [0]*256
+procmask = 0
+for i in range(256):
+  if i in whitelist_opcodes and \
+      i not in push_opcodes and \
+      i not in stop_opcodes:
+    # can skip this opcode
+    stoplist[i] = 1
+  else:
+    procmask |= 1 << i
+
+# PUSH1 through PUSH4, can't skip in slow
+for i in range(0x60, 0x64):
+  stoplist[i] = i-0x5e
+
+if __name__ == "__main__":
+  rr = "uint256[8] memory skip = [\n"
+  for i in range(0, 0x100, 0x20):
+    ret = "uint256(0x"
+    for j in range(i, i+0x20, 1):
+      ret += ("%02X" % stoplist[j])
+    rr += ret+"),\n"
+
+  rr = rr[:-2] + "];"
+  print(rr)
+  print("uint256 _opcodeProcMask = ~uint256(0x%x);" % procmask)
+  print("uint256 _opcodeStopMask = ~uint256(0x%x);" % stopmask)
+  print("uint256 _opcodePushMask = ~uint256(0x%x);" % pushmask)
+

packages/contracts/contracts/optimistic-ethereum/ovm/verify/k/.gitignore

@@ -0,0 +1 @@
+out

packages/contracts/contracts/optimistic-ethereum/ovm/verify/k/build.sh

@@ -0,0 +1,5 @@
+#!/bin/bash
+cd dapp
+solc --allow-paths . --combined-json=abi,bin,bin-runtime,srcmap,srcmap-runtime,ast src/SafetyChecker.sol > out/dapp.sol.json
+
+

packages/contracts/contracts/optimistic-ethereum/ovm/verify/k/config.json

@@ -0,0 +1,17 @@
+{
+  "src": {
+    "specification": "src/specification.act.md",
+    "smt_prelude": "src/prelude.smt2.md",
+    "rules": [
+      "src/lemmas.k.md"
+    ]
+  },
+  "implementations": {
+    "SafetyChecker": {
+      "src": "src/SafetyChecker.sol"
+    }
+  },
+  "dapp_root": "dapp"
+}
+
+

packages/contracts/contracts/optimistic-ethereum/ovm/verify/k/dapp/src/SafetyChecker.sol

@@ -0,0 +1 @@
+../../../../SafetyChecker.sol

packages/contracts/contracts/optimistic-ethereum/ovm/verify/k/dapp/utils

@@ -0,0 +1 @@
+../../../../utils