Maian python3.6 version 1

README.md

@@ -2,6 +2,11 @@
 
 The repository contains Python implementation of Maian -- a tool for automatic detection of buggy Ethereum smart contracts of three different types: prodigal, suicidal and greedy. Maian processes contract's bytecode and tries to build a trace of transactions to find and confirm bugs. The technical aspects of the approach are described in [our paper](https://arxiv.org/abs/1802.06038). 
 
+## Update
+* Maian source code is being ported to python3(>=3.6). Find the new manual to install and run Maian below.
+* For Linux based distributions with python3.5 as default python version, note that your pip3 might point to python3.5 instead of 3.6
+* Currently, the GUI-based Maian is still in development.
+
 ## Evaluating Contracts
 Maian analyzes smart contracts defined in a file `<contract file>` with:  
 
@@ -17,13 +22,13 @@ Maian checks for three types of buggy contracts:
 
 For instance, to check if the contract `ParityWalletLibrary.sol` given in Solidity source code with `WalletLibrary` as main contract is suicidal use
 
-	$ python maian.py -s ParityWalletLibrary.sol WalletLibrary -c 0
+	$ python3.6 maian.py -s example_contracts/ParityWalletLibrary.sol WalletLibrary -c 0
 
 The output should look like this:
 
 ![smiley](maian.png)
 
-To get the full list of options use `python maian.py -h`
+To get the full list of options use `python3.6 maian.py -h`
 
 
 
@@ -39,17 +44,22 @@ A snapshot of one run is given below
 Maian should run smoothly on Linux (we've checked on Ubuntu/Mint) and MacOS. Our attempts to run it on Windows have failed. 
 The list of dependencies is as follows:
 
-1. Go Ethereum, check https://ethereum.github.io/go-ethereum/install/
-2. Solidity compiler, check http://solidity.readthedocs.io/en/develop/installing-solidity.html
-3. Z3 Theorem prover, check https://github.com/Z3Prover/z3
-4. web3, try `pip install web3`
-5. PyQt5 (only for GUI Maian), try `sudo apt install python-pyqt5` 
+1. Python3.6 and pip3
+2. Go Ethereum, check https://ethereum.github.io/go-ethereum/install/
+3. Solidity compiler, check http://solidity.readthedocs.io/en/develop/installing-solidity.html
+4. Z3 Theorem prover, check https://github.com/Z3Prover/z3 or `pip3 install z3-solver`
+5. web3, try `python3.6 -m pip install web3` or `pip3 install web3`
+6. PyQt5 (only for GUI Maian), check  https://gist.github.com/ujjwal96/1dcd57542bdaf3c9d1b0dd526ccd44ff
+7. rlp version 0.6.0, try `python3.6 -m pip install rlp==0.6.0`
+8. pysha3, try `python3.6 -m pip install pysha3`
+
+**All these dependencies must be installed for python3.6**
 
 ## Important
 
 To reduce the number of false positives, Maian deploys the analyzed contracts (given either as Solidity or bytecode source) on 
 a private blockchain, and confirms the found bugs by sending appropriate transactions to the contracts. 
-Therefore, during the execution of the tool, a private Ethereum blockchain is running in the background (blocks are mined on it in the same way as on the Mainnet). Our code stops the private blockchain once Maian finishes the search, however, in some  extreme cases, the blockchain keeps running. Please make sure that after the execution of the program, the private blockchain is off (i.e. `top` does not have `geth` task that corresponds to the private blockchain). 
+Therefore, during the execution of the tool, a private Ethereum blockchain is running in the background (blocks are mined on it in the same way as on the Mainnet). Our code stops the private blockchain once Maian finishes the search, however, in some  extreme cases, the blockchain keeps running. Please make sure that after the execution of the program, the private blockchain is off (i.e. `top` does not have `geth` task that corresponds to the private blockchain). Also, your system time must be the current time. 
 
 ## License
 
@@ -58,4 +68,4 @@ Maian is released under the [MIT License](https://opensource.org/licenses/MIT),
 ## Donations
 
 To help keep this and other future tools free and up to date, consider donating Ether to our account: 0xfd03b29b5c20f878836a3b35718351adf24f4a06
-
+

tool/blockchain.py

@@ -1,5 +1,5 @@
 from __future__ import print_function
-from web3 import Web3, KeepAliveRPCProvider, IPCProvider
+from web3 import Web3
 import subprocess, signal
 import time
 import sys
@@ -32,22 +32,25 @@ def start_private_chain(chain,etherbase,debug=False):
 
 
 
-    if Web3(KeepAliveRPCProvider(host='127.0.0.1', port=MyGlobals.port_number)).isConnected() :
+    if Web3(Web3.HTTPProvider("http://127.0.0.1:"+str(MyGlobals.port_number))).isConnected(): 
+    # Web3(KeepAliveRPCProvider(host='127.0.0.1', port=MyGlobals.port_number)).isConnected() :
             print('\033[91m[-] Some blockchain is active, killing it... \033[0m', end='')
             kill_active_blockchain()
-            if not( Web3(KeepAliveRPCProvider(host='127.0.0.1', port=MyGlobals.port_number)).isConnected() ):
+            if not( Web3(Web3.HTTPProvider("http://127.0.0.1:"+str(MyGlobals.port_number))).isConnected() ):
+                # Web3(KeepAliveRPCProvider(host='127.0.0.1', port=MyGlobals.port_number)).isConnected() ):
                 print('\033[92m Killed \033[0m')
             else:
                 print('Cannot kill')
 
     print('\033[1m[ ] Connecting to PRIVATE blockchain %s  \033[0m' % chain, end='')
     if debug:
-        pro = subprocess.Popen(['geth','--rpc','--rpccorsdomain','"*"','--rpcapi="db,eth,net,web3,personal,web3"', '--rpcport',MyGlobals.port_number, '--datadir','blockchains/'+chain,'--networkid','123','--mine','--minerthreads=1','--etherbase='+MyGlobals.etherbase_account])
+        pro = subprocess.Popen(['geth','--rpc','--rpccorsdomain','"*"','--rpcapi="db,eth,net,web3,personal,web3"', '--port', '35555', '--rpcport',MyGlobals.port_number, '--datadir','blockchains/'+chain,'--networkid','123','--mine','--minerthreads=1','--etherbase='+MyGlobals.etherbase_account])
     else:
-        pro = subprocess.Popen(['geth','--rpc','--rpccorsdomain','"*"','--rpcapi="db,eth,net,web3,personal,web3"', '--rpcport',MyGlobals.port_number, '--datadir','blockchains/'+chain,'--networkid','123','--mine','--minerthreads=1','--etherbase='+MyGlobals.etherbase_account],stdout=devnull, stderr=devnull)
+        pro = subprocess.Popen(['geth','--rpc','--rpccorsdomain','"*"','--rpcapi="db,eth,net,web3,personal,web3"', '--port', '35555', '--rpcport',MyGlobals.port_number, '--datadir','blockchains/'+chain,'--networkid','123','--mine','--minerthreads=1','--etherbase='+MyGlobals.etherbase_account],stdout=devnull, stderr=devnull)
 
     global web3
-    MyGlobals.web3 = Web3(KeepAliveRPCProvider(host='127.0.0.1', port=MyGlobals.port_number))
+    MyGlobals.web3 = Web3(Web3.HTTPProvider("http://127.0.0.1:"+str(MyGlobals.port_number), request_kwargs={'timeout': 20}))
+    # Web3(KeepAliveRPCProvider(host='127.0.0.1', port=MyGlobals.port_number))
     while( not MyGlobals.web3.isConnected() ):
         print('',end='.')
         if MyGlobals.exec_as_script:

tool/contracts.py

@@ -1,5 +1,5 @@
 from __future__ import print_function
-from web3 import Web3, KeepAliveRPCProvider, IPCProvider
+from web3 import Web3
 import os.path
 import json
 import sched, time
@@ -56,7 +56,7 @@ def get_function_hashes(contract):
                     hs += i['type']
                     fr = False
             hs += ')'
-            hash_op = Web3.sha3(hs.encode('utf-8'), encoding='bytes')
+            hash_op = Web3.sha3(hs.encode('utf-8'))
 
             fhashes[hash_op[2:10]] = hs
 
@@ -162,8 +162,8 @@ def normalize_address(x, allow_blank=False):
 def predict_contract_address(accountAddress):
 
     nonce = int(MyGlobals.web3.eth.getTransactionCount(accountAddress)) 
-    adr = Web3.sha3(rlp.encode([normalize_address(accountAddress), nonce]), encoding='bytes')[-40:]
-    return '0x'+adr
+    adr = str(Web3.sha3(rlp.encode([normalize_address(accountAddress), nonce])).hex())[-40:]
+    return Web3.toChecksumAddress('0x'+adr)
 
 
 

tool/execute_instruction.py

@@ -242,7 +242,7 @@ def execute( code, stack, pos, storage, mmemory, data, trace, calldepth, debug,
 
                 val = ''
                 all_good = True
-                for i in range(exact_offset/32):
+                for i in range(exact_offset//32):
                     if (exact_address + i*32) not in mmemory or not is_fixed(mmemory[exact_address+i*32]): 
                         all_good = False
                         break
@@ -353,7 +353,7 @@ def execute( code, stack, pos, storage, mmemory, data, trace, calldepth, debug,
 
 
             if value < 10000:
-                for i in range(value/32):
+                for i in range(value//32):
                     mmemory[addr + 32 * i] = { 'type':'undefined','step':step }
 
         stack.append( {'type':'constant','step':step, 'z3':BitVec('call_at_step_'+str(step), 256) & 0x1} )     # assume the result of call can be any (True or False)
@@ -383,7 +383,7 @@ def execute( code, stack, pos, storage, mmemory, data, trace, calldepth, debug,
                 print('\033[95m[-] In CALLDATACOPY the length of array (%d) is not multiple of 32 \033[0m' % length )
             return pos, True
 
-        for i in range( length / 32 ):
+        for i in range( length // 32 ):
             data[ datapos + 32 * i ] = BitVec('input'+str(calldepth)+'['+str(datapos + 32 * i )+']',256)
             store_in_memory( mmemory, memaddr + 32 * i , {'type':'constant','step':step,'z3':data[ datapos + 32 * i ]} )
 
@@ -446,12 +446,12 @@ def execute( code, stack, pos, storage, mmemory, data, trace, calldepth, debug,
         ea = get_value(addr)
         ev = get_value(value) % 256
 
-        if (ea/32)*32 not in mmemory: 
-            mmemory[(ea/32)*32] = {'type':'constant','step':step, 'z3':BitVecVal(ev << (31- (ea%32)), 256) }
-        elif is_fixed( mmemory[(ea/32)*32]['z3'] ):
-            v = get_value( mmemory[(ea/32)*32]['z3'] )
+        if (ea//32)*32 not in mmemory: 
+            mmemory[(ea//32)*32] = {'type':'constant','step':step, 'z3':BitVecVal(ev << (31- (ea%32)), 256) }
+        elif is_fixed( mmemory[(ea//32)*32]['z3'] ):
+            v = get_value( mmemory[(ea//32)*32]['z3'] )
             v = (v & (~BitVecVal(0xff,256) << (31- (ea%32)))) ^ (ev << (31- (ea%32)))
-            mmemory[(ea/32)*32]['z3'] = v
+            mmemory[(ea//32)*32]['z3'] = v
 
 
     elif op == 'SLOAD':

tool/gui-maian.py

@@ -14,7 +14,7 @@
 
 
 from PyQt5 import QtCore, QtGui, QtWidgets
-from Queue import Queue
+from queue import Queue
 import sys
 import subprocess
 import threading
@@ -303,9 +303,20 @@ def setupUi(self, MAIAN):
         self.retranslateUi(MAIAN)
         QtCore.QMetaObject.connectSlotsByName(MAIAN)
 
-        self.pushStart.clicked.connect(self.start_thread)
-        self.txtLog.textChanged.connect(self.changed_log)
-        self.txtSolidity.textChanged.connect(self.changed_source)
+        try:
+            self.pushStart.clicked.connect(self.start_thread)
+        except:
+            pass
+
+        try:    
+            self.txtLog.textChanged.connect(self.changed_log)
+        except:
+            pass
+
+        try:    
+            self.txtSolidity.textChanged.connect(self.changed_source)
+        except:
+            pass
 
         self.last_pos = 0  
         self.locked_text = False
@@ -553,7 +564,10 @@ def cev():
 
     thread = QtCore.QThread()
     my_receiver = MyReceiver(queue)
-    my_receiver.mysignal.connect(ui.append_text)
+    try:
+        my_receiver.mysignal.connect(ui.append_text)
+    except:
+        pass
     my_receiver.moveToThread(thread)
     thread.started.connect(my_receiver.run)
     thread.start()    

tool/maian.py

@@ -21,7 +21,7 @@
 '''
 
 from __future__ import print_function
-from web3 import Web3, KeepAliveRPCProvider, IPCProvider
+from web3 import Web3
 import argparse,subprocess,sys
 
 
@@ -137,6 +137,7 @@ def main(args):
 
 
         code = MyGlobals.web3.eth.getCode(contract_address)
+        code = str(code.hex())
         if code[0:2] == '0x': code = code[2:]
 
         if 0 == MyGlobals.checktype: ret = check_suicide.check_one_contract_on_suicide(code, contract_address, MyGlobals.debug, MyGlobals.read_from_blockchain, True, fhashes)

tool/parse_code.py

@@ -3,16 +3,16 @@
 def print_code(code,ops):
     for o in ops:
         print('%6x  : %4d : %2s : %12s : %s' % (o['id'],o['id'], o['op'],o['o'] , o['input']) )
-    print('Total byte/code size: %d %d' % (len(code)/2,len(ops)) )
+    print('Total byte/code size: %d %d' % (len(code)//2,len(ops)) )
 
 def get_one_op( code, pos, size_of_input, debug=False ):
     if pos + 2 + size_of_input > len(code ):
-        if debug: print('Incorrect code op at %x : %d : %d :  %s' % (pos/2, pos+2+size_of_input, len(code), code[pos:] ) )
+        if debug: print('Incorrect code op at %x : %d : %d :  %s' % (pos//2, pos+2+size_of_input, len(code), code[pos:] ) )
     instruction = '0x' + code[pos:pos+2]
     o = ''
     if instruction in cops:
         o = cops[ instruction ]
-    t = {'id':int(pos/2),'op':code[pos:pos+2],'input':code[pos+2:pos+2+2*size_of_input],'o':o}
+    t = {'id':int(pos//2),'op':code[pos:pos+2],'input':code[pos+2:pos+2+2*size_of_input],'o':o}
     return (pos + 2 + 2*size_of_input, t)
 
 def parse_code( code, debug = False):

tool/run_examples

@@ -1,8 +1,8 @@
-python maian.py -s example_contracts/example_suicidal.sol KAI -c 0
-python maian.py -b example_contracts/example_suicidal.bytecode -c 0
-python maian.py -bs example_contracts/example_suicidal.bytecode_source -c 0
-python maian.py -s example_contracts/example_prodigal.sol Adoption -c 1
-python maian.py -b example_contracts/example_prodigal.bytecode -c 1
-python maian.py -bs example_contracts/example_prodigal.bytecode_source -c 1
-python maian.py -b example_contracts/example_greedy.bytecode -c 2
-python maian.py -s example_contracts/ParityWalletLibrary.sol WalletLibrary -c 0
+python3.6 maian.py -s example_contracts/example_suicidal.sol KAI -c 0
+python3.6 maian.py -b example_contracts/example_suicidal.bytecode -c 0
+python3.6 maian.py -bs example_contracts/example_suicidal.bytecode_source -c 0
+python3.6 maian.py -s example_contracts/example_prodigal.sol Adoption -c 1
+python3.6 maian.py -b example_contracts/example_prodigal.bytecode -c 1
+python3.6 maian.py -bs example_contracts/example_prodigal.bytecode_source -c 1
+python3.6 maian.py -b example_contracts/example_greedy.bytecode -c 2
+python3.6 maian.py -s example_contracts/ParityWalletLibrary.sol WalletLibrary -c 0

tool/values.py

@@ -1,4 +1,5 @@
-from web3 import Web3, KeepAliveRPCProvider, IPCProvider
+from web3 import Web3
+# , KeepAliveRPCProvider, IPCProvider
 import copy
 from z3 import *
 
@@ -143,10 +144,10 @@ class MyGlobals(object):
 
     # Params related to blockchain
     port_number = '8550'
-    confirming_transaction ='0x3094c123bd9ffc3f41dddefd3ea88e4296e45015b62e892f8bdf9d1b645ef2d2'
-    etherbase_account = '0x69190bde29255c02363477462f17e816a9533d3a'
-    adversary_account = '5a1cd1d07d9f59898c434ffc90a74ecd937feb12'
-    sendingether_account = '564625b3ae8d0602a8fc0fe22c884b091098417f'
+    confirming_transaction = '0x3094c123bd9ffc3f41dddefd3ea88e4296e45015b62e892f8bdf9d1b645ef2d2'
+    etherbase_account = Web3.toChecksumAddress('0x69190bde29255c02363477462f17e816a9533d3a')
+    adversary_account = Web3.toChecksumAddress('5a1cd1d07d9f59898c434ffc90a74ecd937feb12').lstrip('0x')
+    sendingether_account = Web3.toChecksumAddress('564625b3ae8d0602a8fc0fe22c884b091098417f').lstrip('0x')
     send_initial_wei = 44
     web3 = None