search

nevillegrech / gigahorse-toolchain

A binary lifter and analysis framework for Ethereum smart contracts
Other
296 stars 61 forks source link

prevent symbolic_value from saturating integers #42

Closed snf closed 12 months ago

snf commented 2 years ago

This tackles a miss-optimization from Solidity that generates code like this:

    0xa50x31: va5V31 = MLOAD va3V31(0x40)
    0xa60x31: va6V31(0x1f) = CONST 
    0xa80x31: va8V31(0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe0) = NOT va6V31(0x1f)
    0xa90x31: va9V31 = ADD va8V31(0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe0), va5V31
    0xaa0x31: vaaV31 = MLOAD va9V31

with the intention of dereferring (ptr - 0x20). This causes Variable_SymbolicValue to saturate the integer instead of returning the right offsets.

The proposed modification to gigahorse is detecting if the integer gets saturated and make the number negative. Open to other potential solutions.

sifislag commented 2 years ago

Hi @snf, Thanks for the PR, will check it out and let you know what I think.

sifislag commented 2 years ago

Can you point me to the contract you're looking at? I know its a frequently seen code pattern, I just want to be working on a common example.

snf commented 2 years ago

Thanks for having a look, I'm on leave but I'll get a testcase as my current one is too big to use as such.