3 ms·

Some of these bugs are crazy: > Prodigal contracts. In Figure 6, we give an example of a prodigal contract. The function 'tap' seems to lock Ether because the

by gwern 9y ago

Some of these bugs are crazy: > Prodigal contracts. In Figure 6, we give an example of a prodigal contract. The function 'tap' seems to lock Ether because the condition at line 4, semantically, can never be true. However, the compiler optimization of Solidity allows this condition to pass when an input greater than 20 bytes is used to call the function 'tap'. Note, on a byte-code level, the EVM can only load chunks of 32 bytes of input data. At line 3 in 'tap' the first 20 bytes of 'nickname' are assigned to the global variable 'prev' , while neglecting the remaining 12 bytes. The error occurs because EVM at line 4, correctly nullifies the 12 bytes in 'prev', but not in 'nickname'. Thus if 'nickname' has non-zero values in these 12 bytes then the inequality is true. This contract so far has lost 5.0001 Ether to different addresses on real Ethereum blockchain. Whaaa?

shoo 9y ago
So this was Figure 6: bytes20 prev; function tap(bytes20 nickname) { prev = nickname; if (prev != nickname) { msg.sender.send(this.balance); } } It sounds like with our buggy-compiler-optimisation hat on, nickname might be a value with more than 20 bytes, and the line `prev = nickname` is really doing something closer to `prev := truncate_to_20_bytes(nickname)`. And maybe under the hood a bytes20 is encoded as a fixed-length value of 32 bytes with 12 trailing zeros. Then `prev != nickname` is comparing their representations as full fixed-length arrays of 32 bytes. http://solidity.readthedocs.io/en/develop/types.html#fixed-size-byte-arrays http://solidity.readthedocs.io/en/develop/types.html#fixed-s... From http://solidity.readthedocs.io/en/develop/bugs.html http://solidity.readthedocs.io/en/develop/bugs.html it reads as if this was bug "CleanBytesHigherOrderBits" fixed in "0.3.3". So I guess this is just a compiler bug, but on the other hand perhaps it's a bit of a "language smell" that we're writing code in a language that is obsessed with counting how many bytes are in each variable - it isn't super surprising that there are going to be defects related to lower-level memory things that aren't superficially obvious from the code. edit: the Solidity page on security considerations mentions formal verification http://solidity.readthedocs.io/en/develop/security-considerations.html#formal-verification http://solidity.readthedocs.io/en/develop/security-considera... > Using formal verification, it is possible to perform an automated mathematical proof that your source code fulfills a certain formal specification. The specification is still formal (just as the source code), but usually much simpler. That kind of thing doesn't sound like it would have helped here, as the defect doesn't appear to be in the program itself, but in the translation of the problem from solidity into the EVM. it looks like there's at least one person looking into if it is possible to do formal verification that would include the translation from solidity to EVM : https://github.com/pirapira/ethereum-formal-verification-overview https://github.com/pirapira/ethereum-formal-verification-ove...
- deleted 9y ago
  [deleted]

by gwern 9y ago

shoo 9y ago

So this was Figure 6: bytes20 prev; function tap(bytes20 nickname) { prev = nickname; if (prev != nickname) { msg.sender.send(this.balance); } } It sounds like with our buggy-compiler-optimisation hat on, nickname might be a value with more than 20 bytes, and the line `prev = nickname` is really doing something closer to `prev := truncate_to_20_bytes(nickname)`. And maybe under the hood a bytes20 is encoded as a fixed-length value of 32 bytes with 12 trailing zeros. Then `prev != nickname` is comparing their representations as full fixed-length arrays of 32 bytes. http://solidity.readthedocs.io/en/develop/types.html#fixed-size-byte-arrays http://solidity.readthedocs.io/en/develop/types.html#fixed-s... From http://solidity.readthedocs.io/en/develop/bugs.html http://solidity.readthedocs.io/en/develop/bugs.html it reads as if this was bug "CleanBytesHigherOrderBits" fixed in "0.3.3". So I guess this is just a compiler bug, but on the other hand perhaps it's a bit of a "language smell" that we're writing code in a language that is obsessed with counting how many bytes are in each variable - it isn't super surprising that there are going to be defects related to lower-level memory things that aren't superficially obvious from the code. edit: the Solidity page on security considerations mentions formal verification http://solidity.readthedocs.io/en/develop/security-considerations.html#formal-verification http://solidity.readthedocs.io/en/develop/security-considera... > Using formal verification, it is possible to perform an automated mathematical proof that your source code fulfills a certain formal specification. The specification is still formal (just as the source code), but usually much simpler. That kind of thing doesn't sound like it would have helped here, as the defect doesn't appear to be in the program itself, but in the translation of the problem from solidity into the EVM. it looks like there's at least one person looking into if it is possible to do formal verification that would include the translation from solidity to EVM : https://github.com/pirapira/ethereum-formal-verification-overview https://github.com/pirapira/ethereum-formal-verification-ove...

deleted 9y ago
[deleted]