Consensus errors

[holiman]

I'm eyeing through the EVM implementation, and thought I'd add any consensus errors that I can spot to this ticket. The ticket may contain some false positives, apologies in advance if that is the case

1. Missing analysis of valid JUMPDESTs. The EVM does not allow jumping into a data-section, for example into the 32 bytes following a PUSH32. So if the code is

PUSH01 5b
PUSH1 01
JUMP

Then it appears that manticore evm would jump into the 'artificial' jumpdest 5b at byte 1 and continue execution.

2. Missing JUMPDEST check. Apparently known already

3. DELEGATECALL/CALLCODE quirks. It looks like DELEGATECALL passes the current address as sender here. That's how CALLCODE works, whereas DELEGATECALL should pass the original sender as sender.

4. SELFDESTRUCT immediately deletes an address from the world: https://github.com/trailofbits/manticore/blob/master/manticore/platforms/evm.py#L1880 .

5. SELFDESTRUCT adds deleted account to a list, possibly adding the same account multiple times if SELFDESTRUCT is performed several times: https://github.com/trailofbits/manticore/blob/master/manticore/platforms/evm.py#L1881

6. (I'm unsure about this): I can't find where the stack value normalization happens. For example, the SUB operation returns potentially a negative integer. What happens if that negative integer is used as value for a CALL? Will a negative value be sent?

7. 63/64ths rule does not seem implemented. Whenever a CALL type is made, the max allowed gas that is sent along to the child 63/64ths of the current gas.

[dguido]

Thanks for the code review. We filed a few issues yesterday related to testing and plan to address them in this release cycle. In particular, we think that adding support for the Constantinople changes will take only a day or two and should be in soon.

#1163
#1164
#1165
#1166
#1167
#1168

[feliam]

Hi holiman . Thank you or this. We are determined to up our correctness game so this is very welcome. I gave it a pass trying to address this issues.
1,2) FIXED. JUMPDEST, This was a known omission. #1172
3) Fixed here. #117
4) I'm researching why it should not be immediately deleted.. Will fix
5) Fixed here: #1180
6) Hopefully already correct. Need tests. We check that it does not send more than the source balance via a unsigned cmp

manticore/manticore/platforms/evm.py

Line 2258 in 2a4d62a

enough_balance = Operators.UGE(src_balance, value)

7) Not implemented. Also refunds are not implemented. Working on it...

We hope all this gets superseded by running the official XML tests.