enzymefinance / oyente Goto Github PK

Recently I am using Oyente to analyze smart contracts, and I think it is an excellent tool!
However, I discover that there may exist a bug in symExec.py when it operates EXTCODESIZE. In the processing codes of this opcode, there is only one item should be poped out of stack. So in "if len(stack) > 1:", I think it should be: "if len(stack) > 0:".

When I ran some contract bytecode, Oyente usually 'STACK underflow'. For example this contract:
0x2aFDf89A247305dAE5C77327681dF8923E40e5d1

So I think this is a bug. I don't know whether I am right or not?

HI,All:
The contract shows as following:

contract theRun{
    function random() returns(uint result){
        uint salt = block.timestamp;
        uint y = salt % 5;
        return y;
    }
}

i used oyente to detect errors, but it output "time_dependency:false", i think it should output "time_dependency:true" because y depend on block.timestamp, its a puzzle for me

Hi,
I use "truffle init" to create MetaCoin.sol and ConvertLib.sol; and in MetaCoin.sol, it contains the code of "import "ConvertLib.sol"".
Now, using oyente, i get the bytecode of MetaCoin.sol is:
606060405263ffffffff7c01000000000000000000000000000000000000000000000000000000006000350416637bd703e8811461005057806390b98a111461007e578063f8b2cb4f146100b1575bfe5b341561005857fe5b61006c600160a060020a03600435166100df565b60408051918252519081900360200190f35b341561008657fe5b61009d600160a060020a036004351660243561017f565b604080519115158252519081900360200190f35b34156100b957fe5b61006c600160a060020a0360043516610217565b60408051918252519081900360200190f35b600073__ConvertLib.sol:ConvertLib_____________6396e4ee3d61010484610217565b60026000604051602001526040518363ffffffff167c0100000000000000000000000000000000000000000000000000000000028152600401808381526020018281526020019250505060206040518083038186803b151561016257fe5b6102c65a03f4151561017057fe5b5050604051519150505b919050565b600160a060020a033316600090815260208190526040812054829010156101a857506000610211565b600160a060020a0333811660008181526020818152604080832080548890039055938716808352918490208054870190558351868152935191937fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef929081900390910190a35060015b92915050565b600160a060020a0381166000908152602081905260409020545b9190505600a165627a7a723058206d8fcfcd47383a6b633e49e0b47ec81238656b30961e0903bcf9c2f0dba774a30029
this bytecode contains "ConvertLib.sol:ConvertLib___________", i debuged oyente, and found it can not be turned into opcode.

From @pirapira on September 26, 2016 11:18

In the yellow paper, DIV and SDIV instructions return zero when the divisor is zero. Is this also the case in oyente?

Copied from original issue: ethereum/oyente#5

Hi there,

I've extended Oyente a little bit in my fork (https://github.com/leonardoalt/oyente) to try and verify any Solidity assertion. An assertion is compiled by Solc as a simple jump to INVALID in case the condition fails. So I use the SMT branch queries to decide whether a certain symbolic path may reach an INVALID (an assertion failure), and if that's the case ask z3 for the model. This has worked pretty well for the examples I've tried, but of course if you introduce unbounded loops it's gonna explode.

The basic part is identifying assertions in the ASM code, since Solc uses INVALID for other cases as well,
for example if the called function doesn't exist (this is always contained in Block 0), or if CALLVALUE is zero. So far I've been considering as assertions blocks that start with INVALID except the cases above.
Question 1: Is anyone aware of a better way to detect assertions in the basic blocks?

If INVALID is reachable, the model is retrieved from z3 and printed. I also tried some tricks to automatically figure out in which Solidity function the assertion that failed is, by checking which blocks represent the start of each function (by using the signatures and hashes of the functions), building a reverse CFG and walking backwards from the block that contains the assertion. Of course this only guarantees what was the top-level function that led to the assertion, but its correctness is not guaranteed in case of nested function calls.
Question 2: Does anyone have an idea of how I can map this information back to the Solidity source code in a better way? Ideally I'd like to map back symbolic to Solidity variables as well, but I know it's even harder.

Notice that I am trying to do all that without changing the language or the compiler, which would make it easier but less usable.

Cheers,
Leo

What happens if this condition occurs?
if isinstance(address, (int, long)) and address not in global_state["Ia"]

Users need to enter only the entry file, which may include several .sol files

From @loiluu on September 24, 2016 3:29

There are existing tests built for evm virtual machines https://github.com/ethereum/tests/tree/develop/VMTests
We may use these tests to test the correctness of our vm implementation.

Copied from original issue: ethereum/oyente#4

when an error happens, I want to know the error happend in which function, can you give out this log???

disasm binary has been removed with the latest version

From @turbosnail9 on October 3, 2016 20:10

Fix typo in line 22 from "Thorem" to "Theorem"

Copied from original issue: ethereum/oyente/pull/6

Add a global timeout parameter. Terminate the symbolic execution after the timeout and do the analysis with all the explored paths so far.

There are no operations of opcodes: "EXTCODECOPY" "CREATE" "DELEGATECALL".

Hi there,

I'm running a few tests, and I've come across this behavior for the following contract:

pragma solidity ^0.4.11;

contract T {
  uint sum0;
  uint sum1;
  
  function t(bool b) {
    require(block.timestamp < 1000);
    
    if (b) {
      sum1 += msg.value;
    }
    else {
      sum0 += msg.value;
    }

  }
}

With the contract like this, it times out.
Without the require line, it runs instantly.
I haven't checked the constraints that are passed to z3, but I would assume the branch that leads to the if/else has one constraint on the timestamp.

Any high level thoughts on why this happens?

BLOCKHASH, COINBASE, TIMESTAMP, NUMBER, CALLDATALOAD, ....

Running batch_run.py gives this error in a lot of cases. Is this a regression?

ERROR:root:Storage key or value is not a number
Traceback (most recent call last):
  File "symExec.py", line 94, in compare_storage_unit_test
    key = str(long(key))
ValueError: invalid literal for long() with base 10: 'some_var_3'

From @chatch on February 6, 2017 6:1

Can you add the Dockerfile for https://hub.docker.com/r/hrishioa/oyente/ to the repo? Link it on docker hub too if possible.

I'd like to make some changes to it.

Copied from original issue: ethereum/oyente#7

Hi guys! Look a this code. I get Callstack Attack: True for this contract. That’s because of return beneficiary.call.value(this.balance)();. But I don‘t think it could be exploited any way.
I also don‘t know how to refactor it to eliminate Callstack Attack: True. Isn‘t it an Oyente bug?

pragma solidity ^0.4.11;

contract Foo {
  address public beneficiary = msg.sender;

  function withdraw() public
  returns (bool success)
  {
    if (msg.sender != beneficiary) {
      throw;
    }
    return beneficiary.call.value(this.balance)();
  }

  function ()
  payable
  {
  }
}

Here is a testcase that oyente didn't detect the bug

contract TestContract {
     uint balance;

     function testFunction() {
        if (block.timestamp % 2 == 0) {
                msg.sender.send(100);
        } else {
                msg.sender.send(200);
        }
     }
}

I don't know what is the correct formula to operate this opcode:
~x or 2**256 - 1 - x where x = stack.pop(0)

From @loiluu on March 10, 2017 8:53

Currently, the codebase is very messy, hard to follow. It also lacks documentation.

Copied from original issue: ethereum/oyente#9

I love the idea of a tool like this. Great to see it being worked on and would love to use it for Augur.

When testing with The DAO's original bytecode [pulled from dao github] however it doesn't throw any errors whatsoever.

(venv)sh-4.3# python oyente.py -b thedao.evm 
Running, please wait...
	============ Results ===========
	  CallStack Attack: 	 False
	  Concurrency Bug: 	 False
	  Time Dependency: 	 False
	  Reentrancy bug exists: False
	====== Analysis Completed ======

I'm not sure how much work this is, but doesn't seem to work with python 3 just now.

I see the format that disasm outputs has changed a bit. Our regex might need to be updated. And with the next version of go-ethereum (1.6.0), disasm has been merged into evm

Consider using logging library https://docs.python.org/2/library/logging.html instead of printout to the std console

hosted node for rpc calls to get latest blockchain data

Using the docker container, oyente crashes via a segmentation fault, while trying to do the concurrency bug check it seems. Oddly, the same contract can be checked via the oyente browser-solidity/remix webpage, however, it returns a different result on the callstack attack, indicating true on the web one, and false on the one I tried with docker.

Here's the command along with the remote contract:

python oyente.py -ru https://raw.githubusercontent.com/oraclize/ethereum-api/master/connectors/oraclizeConnector.sol

greeter check worked fine

Hi there,

After pulling the most recent code yesterday, the output that I get for a simple program is:

INFO:symExec:Running, please wait...
INFO:symExec:	============ Results ===========
INFO:symExec:	  CallStack Attack: 	 False
INFO:symExec:	====== Analysis Completed ======

I've noticed that there is a new function detect_bugs that is called if the symbolic execution times out and prints the other results.
Why isn't it called if the symb exec goes through?

Cheers,
Leo

Hi,
I would assume this contract is safe with respect to reentrancy, but Oyente says otherwise. Why is that?

pragma solidity ^0.4.11;

contract T {
    uint a;

  function t() {
        if (a > 0) {
            uint b = a;
            a = 0;
            msg.sender.transfer(b);
        }
  }
  
}

eg using https://letsencrypt.org/ for free certificates

should be sufficient to have https for 40.71.169.142 ie https://40.71.169.142

Add 2 parameters to the web form:

• Global timeout
• Email: email to users after their analysis is done. Users can close their windows after they have started the analysis.

When it operates opcode "JUMP" and "JUMPI", it has conversion "target_address = int(str(simplify(target_address)))". In Python it may throw error: "ValueError: invalid literal for int() with base 10", when target_address is a string that contains non-number.

From @loiluu on September 21, 2016 5:4

One way to improve the performance of the symbolic execution is to consider the existing blockchain state in the execution environment. For example, if a contract calls a function
a = contractB.getSomeData()
we can fetch the blockchain state to see what the value that contractB.getSomeData() would return and assign the value to a, instead of using a new symbolic value for a.

Copied from original issue: ethereum/oyente#3

Not sure whether it is a bug or tool limitation: when analyzing raw bytecode of simple contract with reentrancy bug oyente reports that it's not vulnerable, although when running it with --debug flag I see:

INFO:oyente.analysis:Reentrancy bug? True.

I looked into source code and seen this snippet in symExec.py:

    if not isTesting():
        s = ""
        if reentrancy_bug_found and source_map != None:
            pcs = global_problematic_pcs["reentrancy_bug"]
            pcs = [pc for pc in pcs if source_map.find_source_code(pc)]
            pcs = source_map.reduce_same_position_pcs(pcs)
            s = source_map.to_str(pcs, "Reentrancy bug")
        results["reentrancy"] = s
        s = "\t  Reentrancy bug: \t True" + s if s else "\t  Reentrancy bug: \t False"
        log.info(s)

Seems like reentrancy bug can only 'recognized' when there is source code present. Is this a bug or is it an intended behaviour?

Something working along the lines of

Install

Install solc

For example by

$ sudo add-apt-repository ppa:ethereum/ethereum
$ sudo apt-get update
$ sudo apt-get install solc

Install evm from go-ethereum

For example via:

1. https://geth.ethereum.org/downloads/ or
2. By from PPA if your using Ubuntu

$ sudo apt-get install software-properties-common
$ sudo add-apt-repository -y ppa:ethereum/ethereum
$ sudo apt-get update
$ sudo apt-get install ethereum

Install z3 Theorem Prover

1. Download the source code of version z3-4.5.0

2. Install z3 using Python bindings

$ python scripts/mk_make.py --python
$ cd build
$ make
$ sudo make install

Install requests library

1. Get Python request library via pip

$ pip install requests

This is the code snippet that handle PUSH which behaves the same for all type of PUSH from PUSH1 -> PUSH32:
elif instr_parts[0].startswith('PUSH', 0): # this is a push instruction
pushed_value = int(instr_parts[1], 16)
stack.insert(0, pushed_value)

From @loiluu on September 21, 2016 4:58

At the moment, Oyente does not support a large fraction of existing EVM opcodes, but not all of them. Please check the main file symExec.py to see which opcodes are supported at the moment.

Copied from original issue: ethereum/oyente#1

From @loiluu on September 21, 2016 4:59

At the moment, Oyente terminates a path when seeing a loop, and proceeds to other ones. In other words, our SE only explores an under-approximation of all the program symbolic paths.

It might be useful to note that there is a technical challenge regarding loops: statically analysing bytecode will result in unbounded loops. E.g. Array copy from data input will result in a loop, and statically we don’t know the size of the data input.

Copied from original issue: ethereum/oyente#2

So that users can fetch the docker and run their custom contract easier.
For example, they can do something like:

python oyente.py -r some_url

@ngotungson can you upgrade/ make the changes to support z3 v4.5.0

The test case in "vmArithmeticTest.json"
Symbolic test terminates at PC = 2 => It doesn't run into SIGNEXTEND
[1] PUSH1 0x05
[2] JUMP
[3] JUMPDEST
[4] STOP
[5] JUMPDEST
[8] PUSH2 0x8000
[9] DUP1
[19] PUSH9 0x010000000000000001
[20] SIGNEXTEND
[23] PUSH2 0x8001
[24] GT
[26] PUSH1 0x03
[27] JUMPI
[32] PUSH4 0xbadf000d
[34] PUSH1 0x11
[35] SSTORE

So users can upload/ paste their contract and Oyente will analyse the contract.

I tried test my contract "test.sol" by running the command
python oyente.py --error -s test.sol

the result is

	============ Results ===========
	  CallStack Attack: 	 False`
Exception - object of type 'bool' has no len()
Exception - object of type 'bool' has no len()
Exception - object of type 'bool' has no len()
Exception - object of type 'bool' has no len()
Exception - timeout
	   Concurrency Bug: 	 False
	  Time Dependency: 	 False
	  Reentrancy bug exists: False

what does the result means by "Exception"?

Another thing, If I run the command without arg --error, the script does not terminate at all

From @loiluu on March 6, 2017 4:50

Add several options like:

• Limit Memory Space
• DFS depth limit
• Gas-limit constraint
• Hard limit for loops

Copied from original issue: ethereum/oyente#8

The test case "byte10" in "vmBitwiseLogicOperationTest.json":
[8] PUSH8 0x8040201008040201
[41] PUSH32 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
[42] BYTE
[44] PUSH1 0x00
[45] SSTORE
raise exception: ERROR:root:long int too large to convert to int
Traceback (most recent call last):
File "symExec.py", line 127, in main
build_cfg_and_analyze()
File "symExec.py", line 173, in build_cfg_and_analyze
full_sym_exec() # jump targets are constructed on the fly
File "symExec.py", line 452, in full_sym_exec
return sym_exec_block(0, visited, stack, mem, global_state, path_conditions_and_vars, analysis)
File "symExec.py", line 476, in sym_exec_block
sym_exec_ins(start, instr, stack, mem, global_state, path_conditions_and_vars, analysis)
File "symExec.py", line 1014, in sym_exec_ins
byte = word & (255 << (8 * (32 - byte_no)))
OverflowError: long int too large to convert to int

Opcode BYTE failed all the tests:
Eg: the test case "byte0":
[8] PUSH8 0x8040201008040201
[10] PUSH1 0x00
[12] PUSH1 0x1f
[13] SUB
[14] BYTE
[16] PUSH1 0x00
[17] SSTORE

Result is 0: 512
But it should be 0: 1

Failed bitwise logic operation testcases: ['sgt3', 'lt1', 'slt2', 'not5', 'not1', 'not0', 'gt0']
=> Opcodes failed: SGT, LT, SLT, NOT, GT

When using any of the 0.4.12 compiler version and a corresponding pragma solidity ^0.4.12; I do not get any outputs regarding the checked issues, the result box is in fact empty:

Hi all,
I've been checking the following simple contract (trying to understand some of Oyente's internals):

pragma solidity ^0.4.0;
contract Test {
    uint32 x;
    function Test(uint32 y) {
        if(y > 9) x = y;
        else x = 7 * y;
    }
}

In oyente.py::analyze, when I print disasm_out, I get:

60606040525bfe00
000000: PUSH1 0x60
000002: PUSH1 0x40
000004: MSTORE
000005: JUMPDEST
000006: Missing opcode 0xfe
000007: STOP

As you can see, there are several things missing there.
Since I give a source file, Oyente will compile it using solc and then call evm disasm.

If I call solc --optimize --bin-runtime --asm test.sol, I get all the instructions, including the if/else jumps etc, therefore I assume that the bytecode generated without --asm will contain the same.
The issue comes when I call evm disasm on the bytecode. At this point most of the instructions simply vanish, hence the disasm that Oyente prints.

Does anybody have any idea what's the reason for that, and how to go around it?

Cheers,
Leo

Prepare the document on how to use oyente, what are the arguments, codebase structure for the first release :)

From @loiluu on March 13, 2017 6:56

Expand the transaction-ordering-dependence analysis to ERC20 token contracts to track the flow of tokens.

Copied from original issue: ethereum/oyente#15