search

trailofbits / manticore

Symbolic execution tool
https://blog.trailofbits.com/2017/04/27/manticore-symbolic-execution-for-humans/
GNU Affero General Public License v3.0
3.67k stars 472 forks source link

Lack of documentation on how to execute bytecode-only Ethereum contracts #841

Open ggrieco-tob opened 6 years ago

ggrieco-tob commented 6 years ago

There is no clear documentation or examples of how to symbolically execute a bytecode-only Ethereum contract. In this case, the ABI will be provided by the user, but there is no public interface to associate it with bytecode to run.

Further explanation:

We need clear documentation and examples for creating and interacting with bytecode-only contracts. There are two sets of scenarios to consider: ones where a constructor generates the running bytecode and one where we just paste in an already-known and running bytecode.

The documentation and examples should contemplate the association of a previously known ABI description and the usage of symbolic parameters on both create and normal transactions.

Here are some writeups we would love to see!

You may want to reference the minimal_bytecode.py example to get started!

feliam commented 6 years ago

Is it common to have the ABI and not the source code ? We don't need the ABI to analize a bytecode only contract. (Just saying ^. Totally doable, and a nice to have feature.)

montyly commented 6 years ago

Yes this can happen. For example, the crypto kitties game had a contract geneScience, for which we only knew a part of the ABI (we knew only the functions used in the other open source contracts)

arun-munagala commented 6 years ago

So is there a way to symbolically execute just bytecode?

feliam commented 6 years ago

Yes there is. Well..

Though the code that makes the reporting at the end of each state currently assumes there is solidity generated metadata associated to each contract. And it fails.

Now that there is some interest in binary only I'll try to revive that capability here: https://github.com/trailofbits/manticore/pull/889

arun-munagala commented 6 years ago

When i try to run the example minimal.py with some bytecode in it. I get the following error. What is the way around for it? Traceback (most recent call last): File "examples/evm/minimal.py", line 27, in init_bytecode = m.compile(source_code) File "/home/iam/.virtualenvs/manticore-6excCQm7/local/lib/python2.7/site-packages/manticore/ethereum.py", line 657, in compile name, source_code, bytecode, runtime, srcmap, srcmap_runtime, hashes, abi, warnings = ManticoreEVM._compile(source_code, contract_name) File "/home/iam/.virtualenvs/manticore-6excCQm7/local/lib/python2.7/site-packages/manticore/ethereum.py", line 716, in _compile output, warnings = ManticoreEVM._run_solc(temp) File "/home/iam/.virtualenvs/manticore-6excCQm7/local/lib/python2.7/site-packages/manticore/ethereum.py", line 679, in _run_solc installed_version = m.groupdict()['version'] AttributeError: 'NoneType' object has no attribute 'groupdict'

feliam commented 6 years ago

Could you share which "solc" compiler version do you have installed? thanks.

arun-munagala commented 6 years ago

@feliam Sorry for the late reply. I have 0.4.23 "solc --version solc, the solidity compiler commandline interface Version: 0.4.23-develop.2018.4.19+commit.6f0fbcf8.Linux.g++"

arun-munagala commented 6 years ago

@feliam I have now pulled the latest update. The minimal_bytecode_only.py runs until the evm dissasembler and then i get this error. File "/home/iam/.virtualenvs/manticore-6excCQm7/local/lib/python2.7/site-packages/manticore/ethereum.py", line 1558, in global_coverage runtime_bytecode = self.get_metadata(account_address).runtime_bytecode AttributeError: 'NoneType' object has no attribute 'runtime_bytecode'

feliam commented 6 years ago

It looks like the code there has been changed? https://github.com/trailofbits/manticore/blob/b5d9d1da278ed281bbda7e8c0dac2c7010fc5e57/manticore/ethereum.py#L1539-L1557

arun-munagala commented 6 years ago

Ah yes. Thank you!

ggrieco-tob commented 6 years ago

In the last revision of manticore, the minimal_bytecode_only.py script fails to execute correctly:

$ python3.6 examples/evm/minimal_bytecode_only.py 
[+] Creating a user account 534687980630689331618847425822969211489979010407
[+] Init bytecode: b'608060405234801561001057600080fd5b506101cc806100206000396000f30060806040527f41000000000000000000000000000000000000000000000000000000000000006000366000818110151561003557fe5b905001357f010000000000000000000000000000000000000000000000000000000000000090047f0100000000000000000000000000000000000000000000000000000000000000027effffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff19167effffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff19161415610135577fcf34ef537ac33ee1ac626ca1587a0a7e8e51561e5514f8cb36afa1c5102b3bab6040518080602001828103825260088152602001807f476f7420616e204100000000000000000000000000000000000000000000000081525060200191505060405180910390a161019e565b7fcf34ef537ac33ee1ac626ca1587a0a7e8e51561e5514f8cb36afa1c5102b3bab6040518080602001828103825260128152602001807f476f7420736f6d657468696e6720656c7365000000000000000000000000000081525060200191505060405180910390a15b0000a165627a7a72305820fd5ec850d8409e19cfe593b9ee3276cc3ac12b0e3406d965317dc9c1aeb7f2670029'
[+] EVM init assembler:
0x0 PUSH1 0x80
0x2 PUSH1 0x40
0x4 MSTORE
0x5 CALLVALUE
0x6 DUP1
0x7 ISZERO
0x8 PUSH2 0x10
0xb JUMPI
0xc PUSH1 0x0
0xe DUP1
0xf REVERT
0x10 JUMPDEST
0x11 POP
0x12 PUSH2 0x1cc
0x15 DUP1
0x16 PUSH2 0x20
0x19 PUSH1 0x0
0x1b CODECOPY
0x1c PUSH1 0x0
0x1e RETURN
0x1f STOP
0x20 PUSH1 0x80
0x22 PUSH1 0x40
0x24 MSTORE
0x25 PUSH32 0x4100000000000000000000000000000000000000000000000000000000000000
0x46 PUSH1 0x0
0x48 CALLDATASIZE
0x49 PUSH1 0x0
0x4b DUP2
0x4c DUP2
0x4d LT
0x4e ISZERO
0x4f ISZERO
0x50 PUSH2 0x35
0x53 JUMPI
0x54 INVALID
0x55 JUMPDEST
0x56 SWAP1
0x57 POP
0x58 ADD
0x59 CALLDATALOAD
0x5a PUSH32 0x100000000000000000000000000000000000000000000000000000000000000
0x7b SWAP1
0x7c DIV
0x7d PUSH32 0x100000000000000000000000000000000000000000000000000000000000000
0x9e MUL
0x9f PUSH31 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
0xbf NOT
0xc0 AND
0xc1 PUSH31 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
0xe1 NOT
0xe2 AND
0xe3 EQ
0xe4 ISZERO
0xe5 PUSH2 0x135
0xe8 JUMPI
0xe9 PUSH32 0xcf34ef537ac33ee1ac626ca1587a0a7e8e51561e5514f8cb36afa1c5102b3bab
0x10a PUSH1 0x40
0x10c MLOAD
0x10d DUP1
0x10e DUP1
0x10f PUSH1 0x20
0x111 ADD
0x112 DUP3
0x113 DUP2
0x114 SUB
0x115 DUP3
0x116 MSTORE
0x117 PUSH1 0x8
0x119 DUP2
0x11a MSTORE
0x11b PUSH1 0x20
0x11d ADD
0x11e DUP1
0x11f PUSH32 0x476f7420616e2041000000000000000000000000000000000000000000000000
0x140 DUP2
0x141 MSTORE
0x142 POP
0x143 PUSH1 0x20
0x145 ADD
0x146 SWAP2
0x147 POP
0x148 POP
0x149 PUSH1 0x40
0x14b MLOAD
0x14c DUP1
0x14d SWAP2
0x14e SUB
0x14f SWAP1
0x150 LOG1
0x151 PUSH2 0x19e
0x154 JUMP
0x155 JUMPDEST
0x156 PUSH32 0xcf34ef537ac33ee1ac626ca1587a0a7e8e51561e5514f8cb36afa1c5102b3bab
0x177 PUSH1 0x40
0x179 MLOAD
0x17a DUP1
0x17b DUP1
0x17c PUSH1 0x20
0x17e ADD
0x17f DUP3
0x180 DUP2
0x181 SUB
0x182 DUP3
0x183 MSTORE
0x184 PUSH1 0x12
0x186 DUP2
0x187 MSTORE
0x188 PUSH1 0x20
0x18a ADD
0x18b DUP1
0x18c PUSH32 0x476f7420736f6d657468696e6720656c73650000000000000000000000000000
0x1ad DUP2
0x1ae MSTORE
0x1af POP
0x1b0 PUSH1 0x20
0x1b2 ADD
0x1b3 SWAP2
0x1b4 POP
0x1b5 POP
0x1b6 PUSH1 0x40
0x1b8 MLOAD
0x1b9 DUP1
0x1ba SWAP2
0x1bb SUB
0x1bc SWAP1
0x1bd LOG1
0x1be JUMPDEST
0x1bf STOP
Traceback (most recent call last):
  File "examples/evm/minimal_bytecode_only.py", line 19, in <module>
    init=init_bytecode)
  File "/home/gustavo/.local/lib/python3.6/site-packages/manticore-0.1.10-py3.6.egg/manticore/ethereum.py", line 1596, in create_contract
    self._transaction('CREATE', owner, balance, address, data=init)
  File "/home/gustavo/.local/lib/python3.6/site-packages/manticore-0.1.10-py3.6.egg/manticore/ethereum.py", line 1752, in _transaction
    raise EthereumError("code bad type")
manticore.ethereum.EthereumError: code bad type
defunctio commented 6 years ago

Should be resolved once #1010 is merged I believe.

offlinemark commented 6 years ago

need to revisit this, since that pr was merged.

gitcoinbot commented 5 years ago

Issue Status: 1. Open 2. Started 3. Submitted 4. Done

This issue now has a funding of 400.0 DAI (400.0 USD @ $1.0/DAI) attached to it as part of the Ethereum Community Fund via ECF Web 3.0 Infrastructure Fund fund.

gitcoinbot commented 5 years ago

💰 A crowdfund contribution worth 50000.00000 CBTX has been attached to this funded issue from @royhodge830.💰

Want to chip in also? Add your own contribution here.

gitcoinbot commented 5 years ago

Issue Status: 1. Open 2. Started 3. Submitted 4. Done

Workers have applied to start work.

These users each claimed they can complete the work by 11 months, 2 weeks from now. Please review their action plans below:

1) joinstackinc has applied to start work _(Funders only: approve worker | reject worker)_.

Would love to write a documentation for how to execute a bytecode-only Ethereum contract... Would treat the two scenarios presented.

Learn more on the Gitcoin Issue Details page.

mkosowsk commented 5 years ago

@writeprovidence could you please go a bit more into detail for your plan of attack when you have a moment? Thanks! 👍

gitcoinbot commented 5 years ago

💰 A crowdfund contribution worth 40.00000 DAI (40.0 USD @ $1.0/DAI) has been attached to this funded issue from @.💰

Want to chip in also? Add your own contribution here.

gitcoinbot commented 5 years ago

@writeprovidence Hello from Gitcoin Core - are you still working on this issue? Please submit a WIP PR or comment back within the next 3 days or you will be removed from this ticket and it will be returned to an ‘Open’ status. Please let us know if you have questions!

Funders only: Snooze warnings for 1 day | 3 days | 5 days | 10 days | 100 days

writeprovidence commented 5 years ago

still on it

writeprovidence commented 5 years ago

I'm really sorry @mkosowsk I have to stop work on this issue.

Destiner commented 5 years ago

Hi, is this still relevant? Would like to dive in. cc @mkosowsk.

mkosowsk commented 5 years ago

Hi @ggrieco-tob, could you please comment on if this issue is still relevant for @Destiner?

Thanks!

frankchen07 commented 5 years ago

hey @ggrieco-tob - Frank from Gitcoin here, just helping to follow up! ^

ggrieco-tob commented 5 years ago

Sorry for the delay. I think this issue is still relevant.

mkosowsk commented 5 years ago

@Destiner feel free to apply on the Gitcoin Issue Details page and tyou will be approved. My apologies on the delay!

gitcoinbot commented 5 years ago

Issue Status: 1. Open 2. Started 3. Submitted 4. Done

Work has been started.

These users each claimed they can complete the work by 7 months from now. Please review their action plans below:

1) mihairaulea has been approved to start work.

Hello, read through the description, read through the comments, this is about writing 8 python examples of different flavours on how to execute bytecode contracts using manticore. It will involve documenting the code, showing some side effects, and digging through Manticore API. Ran the python example with no issues.

Learn more on the Gitcoin Issue Details page.

mihairaulea commented 5 years ago

Hello, starting work now, thanks for the approval.

gitcoinbot commented 5 years ago

@mihairaulea Hello from Gitcoin Core - are you still working on this issue? Please submit a WIP PR or comment back within the next 3 days or you will be removed from this ticket and it will be returned to an ‘Open’ status. Please let us know if you have questions!

Funders only: Snooze warnings for 1 day | 3 days | 5 days | 10 days | 100 days

mihairaulea commented 5 years ago

Hello, almost done. Will push tomorrow.

gitcoinbot commented 5 years ago

@mihairaulea Hello from Gitcoin Core - are you still working on this issue? Please submit a WIP PR or comment back within the next 3 days or you will be removed from this ticket and it will be returned to an ‘Open’ status. Please let us know if you have questions!

Funders only: Snooze warnings for 1 day | 3 days | 5 days | 10 days | 100 days

mihairaulea commented 5 years ago

Hi, you request symbolic constructors for the contract, but manticore does not currently supports this: https://github.com/trailofbits/manticore/blob/master/manticore/platforms/evm.py#L529 . @montyly should we drop that from the PR?

feliam commented 5 years ago

So that's kind of a big problem for us (a tool trying to find all possible contract paths). User can append symbolic bytes to the initialization bytecode as "constructor arguments". Then you could, in fact, append actual code. And the EVM execution model would never know where the initialization bytecode ends and where the appended arguments start. So it must treat them all as code and check for the JUMPDEST thing.

I think we should just skip the appended arguments (symbolic or not) from the JUMPDEST condition check assuming that is dead code. And just document that if the user pass actual reachable code after the initialization bytecode, manticore will not explore it. Thoughts?

mihairaulea commented 5 years ago

I don't know the codebase well enough, but it seems like a custom CREATE transaction could in fact be created with symbolic bytes. The current API clearly does not support this, however. The EVM instance does not allow symbolic bytes as data.

gitcoinbot commented 5 years ago

@mihairaulea Hello from Gitcoin Core - are you still working on this issue? Please submit a WIP PR or comment back within the next 3 days or you will be removed from this ticket and it will be returned to an ‘Open’ status. Please let us know if you have questions!

Funders only: Snooze warnings for 1 day | 3 days | 5 days | 10 days | 100 days

gitcoinbot commented 5 years ago

@mihairaulea Hello from Gitcoin Core - are you still working on this issue? Please submit a WIP PR or comment back within the next 3 days or you will be removed from this ticket and it will be returned to an ‘Open’ status. Please let us know if you have questions!

Funders only: Snooze warnings for 1 day | 3 days | 5 days | 10 days | 100 days

gitcoinbot commented 5 years ago

Issue Status: 1. Open 2. Started 3. Submitted 4. Done

@mihairaulea due to inactivity, we have escalated this issue to Gitcoin's moderation team. Let us know if you believe this has been done in error!

Funders only: Snooze warnings for 1 day | 3 days | 5 days | 10 days | 100 days

gitcoinbot commented 5 years ago

Issue Status: 1. Open 2. Started 3. Submitted 4. Done

@mihairaulea due to inactivity, we have escalated this issue to Gitcoin's moderation team. Let us know if you believe this has been done in error!

Funders only: Snooze warnings for 1 day | 3 days | 5 days | 10 days | 100 days

disconnect3d commented 5 years ago

Just for clarification: I think we can skip the symbolic bytecode part for now.

Mikerah commented 3 years ago

Is there a way to pass in a contract's bytecode as a command line argument as opposed to only solidity/vyper files? I'm working on a project in which the contracts are written in a different language but compiles to evm bytecode.