4

I'm thinking maybe looking through the OP codes, you can realize that the contract can only send money to a given address. Would this kind of formal verification be hard to write?

2

It is rather easy I think, even with solidity

contract Example{

address recipient = 0x0000cafebabe;

function send(){
    recipient.send(this.balance);
 }
}

results in (optimized bytecode):

606060405260008054600160a060020a03191663cafebabe178155604e908190602790396000f3606060405260e060020a6000350463b46300ec8114601a575b005b60186000805473ffffffffffffffffffffffffffffffffffffffff9081169190301631606082818181858883f1505050505056

etherscan.io can disassemble the bytecode once it is on the mainnet or use `disasm' form the geth tools

    echo "606060405260008054600160a060020a03191663cafebabe178155604e908190602790396000f3606060405260e060020a6000350463b46300ec8114601a575b005b60186000805473ffffffffffffffffffffffffffffffffffffffff9081169190301631606082818181858883f1505050505056" | disasm 

Gives back:

0      PUSH1  => 60
2      PUSH1  => 40
4      MSTORE
5      PUSH1  => 00
7      DUP1
8      SLOAD
9      PUSH1  => 01
11     PUSH1  => a0
13     PUSH1  => 02
15     EXP
16     SUB
17     NOT
18     AND
19     PUSH4  => cafebabe
24     OR
25     DUP2
26     SSTORE
27     PUSH1  => 4e
29     SWAP1
30     DUP2
31     SWAP1
32     PUSH1  => 27
34     SWAP1
35     CODECOPY
36     PUSH1  => 00
38     RETURN
39     PUSH1  => 60
41     PUSH1  => 40
43     MSTORE
44     PUSH1  => e0
46     PUSH1  => 02
48     EXP
49     PUSH1  => 00
51     CALLDATALOAD
52     DIV
53     PUSH4  => b46300ec
58     DUP2
59     EQ
60     PUSH1  => 1a
62     JUMPI
63     JUMPDEST
64     STOP
65     JUMPDEST
66     PUSH1  => 18
68     PUSH1  => 00
70     DUP1
71     SLOAD
72     PUSH20  => ffffffffffffffffffffffffffffffffffffffff
93     SWAP1
94     DUP2
95     AND
96     SWAP2
97     SWAP1
98     ADDRESS
99     AND
100    BALANCE
101    PUSH1  => 60
103    DUP3
104    DUP2
105    DUP2
106    DUP2
107    DUP6
108    DUP9
109    DUP4
110    CALL
111    POP
112    POP
113    POP
114    POP
115    POP
116    JUMP
| improve this answer | |
  • In the bytecode, what is the part which sends the money? – Fernando Tiberti Jul 2 '16 at 19:13
  • 1
    .send is implemented with CALL opcode (byte 110 in this example). – eth Jul 4 '16 at 9:10

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.