SHshoo·Feb 20, 2018
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-s...
From 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 p
Read the rest
erhaps 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-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-ove...