4 ms·

Finding the Greedy, Prodigal, and Suicidal Contracts at Scale

121 points by Alex3917 9y ago

rrggrr 9y ago
I believe this is the problem that Quantstamp is trying to address with their audit service: https://quantstamp.com/auditrequest/ https://quantstamp.com/auditrequest/
lifeisstillgood 9y ago
Holy moly what? Billions (?) of dollars in contracts that basically the coder screwed up. so this is interesting. A Lawyer who effectively writes an infinite loop in legalese has a lot of issues. More than it seems the coders who write the Ether contract which means we will start seeing changes that may be - the death of the no warranty warranty - Escape hatches in every smart contract (perhaps well-known addresses have specific values and contract is voided) - The slow professionalisation of software I mean there is nothing stopping two people writing and acting under a terribly written contract. but when it goes badly they have to take it to professional "coders" (lawyers) who work out how to unfuck it. this sounds a of like that
- deleted 9y ago
  [deleted]
- nefitty 9y ago
  There are going to be a lot of opportunities in this space. People who begin mastering the relevant skills now will have an outsized influence within a decade or less. We need capable and intelligent folks working on these problems. The incentives are aligned as well, so I don't see what would stop developers from taking on these challenges besides stubbornness.
etaioinshrdlu 9y ago
It seems pretty clear to me that crypto-currencies and blockchain apps, as a technology, are quite unlike anything that have come before it, and fundamentally don't integrate well with the wider world of technology (at least right now). An obvious issue is that smart contracts cannot make use of information from the outside world (unless of course, fed from a single centralized party). Perhaps this can one day be worked around with some innovations from game theory, but I have not seen it. This demonstrates a lack of integration with the rest of humankind's technology. A smart contract, once published, cannot be amended. Let that sink in for a while. This breaks the most basic assumption people have about software companies: that they can be agile, move fast, push updates, and fix things. As far as I can tell, due to the halting problem, one can never actually prove that a sufficiently complex smart contract will not be explosively broken at some point in the future. (The fix for contracts being explosively broken is a hard fork, which only works if you are explosively broken enough to convince a global majority of the network to go along. Your own token probably isn't important enough.) Immutability provides a lot of interesting benefits of course, but let's not forget how explosively wrong it can go as well. It all seems like the kind of tech you wouldn't trust to a bunch of fast moving startups, many of which now have actual VC's invested in their outcomes and will put time pressure on them. It seems most of the HN crowd is well aware of this stuff. But I think it bears repeating, because man, this fishy odor is intense.
- gfodor 9y ago
  I don't see how the halting problem has anything to do with validating smart contracts. Ethereum burns gas as it runs and there's a gas limit so that is the solution to the problem wrt contracts that don't halt.
  - etaioinshrdlu 9y ago
    The risk is not that a contract will run forever, but that it may be intractable to exhaustively predict all possible outcomes or prove much of anything about a contract even given the computational time afforded to it.
    - gfodor 9y ago
      Sure, that isn't due to the halting problem though. It's certainly trivial to show that any solidity program running on the ethereum VM will halt. What you're saying is that the current ether VM languages don't have much in the way of formal proofs to support understanding their behavior, but that is an area of active work afaik and doesn't fall out from the halting problem.
      - readams 9y ago
        It actually is related to the halting problem. Rice's theorem is the directly relevant result though. Formal verification of more constrained systems is possible though.
        deleted 9y ago
        [deleted]
      - archgoon 9y ago
        Consider the following program (in pseudopython, not solidity) function transfer_on_counterexample(int n): # assume n is a counterexample until proven otherwise goldbach_counterexample = true # run through all numbers less than n for prime1 range(n): if is_not_prime(prime1): continue # do it again for another one for prime2 in range(n): if is_not_prime(prime2): continue # check if conjecture is satisfied if prime1 + prime2 == n: # this number does not refute the goldbach conjecture goldbach_counterexample = false return # didn't find p1+p2? goldbach's conjecture is false. # provide a finder's fee if goldbach_counterexample == true: transfer_ethereum() The above program is guaranteed to halt after about O(n^2 * sqrt(n)) (depending on how great the is_not_prime function is). However, it is unknown if there is any input that causes `transfer_ethereum` to be executed. So if I find a counterexample, I can compute how much gas I need to pay to win my finder's fee. So sure, it runs in finite time for a given input, but you have to guarantee it won't ever execute the transfer_ethereum function for all inputs if you want to ensure you never pay out. And that, in general, for a general program (even if guaranteed to halt) is equivalent to the halting problem. Now, I believe that solidity has an upperbound on the size of it's inputs, so the parameter space is bounded, and we return to your original argument that it is a large, but exhaustible, search space.
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...
jeisc 9y ago
Does this title to a scholarly paper read like a newspaper headline to anyone but me? The trading level of ethereum has remained unchanged after the publication of this document?

121 points by Alex3917 9y ago

I believe this is the problem that Quantstamp is trying to address with their audit service: https://quantstamp.com/auditrequest/ https://quantstamp.com/auditrequest/

lifeisstillgood 9y ago

Holy moly what? Billions (?) of dollars in contracts that basically the coder screwed up. so this is interesting. A Lawyer who effectively writes an infinite loop in legalese has a lot of issues. More than it seems the coders who write the Ether contract which means we will start seeing changes that may be - the death of the no warranty warranty - Escape hatches in every smart contract (perhaps well-known addresses have specific values and contract is voided) - The slow professionalisation of software I mean there is nothing stopping two people writing and acting under a terribly written contract. but when it goes badly they have to take it to professional "coders" (lawyers) who work out how to unfuck it. this sounds a of like that

deleted 9y ago
[deleted]
nefitty 9y ago
There are going to be a lot of opportunities in this space. People who begin mastering the relevant skills now will have an outsized influence within a decade or less. We need capable and intelligent folks working on these problems. The incentives are aligned as well, so I don't see what would stop developers from taking on these challenges besides stubbornness.

etaioinshrdlu 9y ago

It seems pretty clear to me that crypto-currencies and blockchain apps, as a technology, are quite unlike anything that have come before it, and fundamentally don't integrate well with the wider world of technology (at least right now). An obvious issue is that smart contracts cannot make use of information from the outside world (unless of course, fed from a single centralized party). Perhaps this can one day be worked around with some innovations from game theory, but I have not seen it. This demonstrates a lack of integration with the rest of humankind's technology. A smart contract, once published, cannot be amended. Let that sink in for a while. This breaks the most basic assumption people have about software companies: that they can be agile, move fast, push updates, and fix things. As far as I can tell, due to the halting problem, one can never actually prove that a sufficiently complex smart contract will not be explosively broken at some point in the future. (The fix for contracts being explosively broken is a hard fork, which only works if you are explosively broken enough to convince a global majority of the network to go along. Your own token probably isn't important enough.) Immutability provides a lot of interesting benefits of course, but let's not forget how explosively wrong it can go as well. It all seems like the kind of tech you wouldn't trust to a bunch of fast moving startups, many of which now have actual VC's invested in their outcomes and will put time pressure on them. It seems most of the HN crowd is well aware of this stuff. But I think it bears repeating, because man, this fishy odor is intense.

gfodor 9y ago
I don't see how the halting problem has anything to do with validating smart contracts. Ethereum burns gas as it runs and there's a gas limit so that is the solution to the problem wrt contracts that don't halt.
- etaioinshrdlu 9y ago
  The risk is not that a contract will run forever, but that it may be intractable to exhaustively predict all possible outcomes or prove much of anything about a contract even given the computational time afforded to it.
  - gfodor 9y ago
    Sure, that isn't due to the halting problem though. It's certainly trivial to show that any solidity program running on the ethereum VM will halt. What you're saying is that the current ether VM languages don't have much in the way of formal proofs to support understanding their behavior, but that is an area of active work afaik and doesn't fall out from the halting problem.
    - readams 9y ago
      It actually is related to the halting problem. Rice's theorem is the directly relevant result though. Formal verification of more constrained systems is possible though.
      - deleted 9y ago
        [deleted]
    - archgoon 9y ago
      Consider the following program (in pseudopython, not solidity) function transfer_on_counterexample(int n): # assume n is a counterexample until proven otherwise goldbach_counterexample = true # run through all numbers less than n for prime1 range(n): if is_not_prime(prime1): continue # do it again for another one for prime2 in range(n): if is_not_prime(prime2): continue # check if conjecture is satisfied if prime1 + prime2 == n: # this number does not refute the goldbach conjecture goldbach_counterexample = false return # didn't find p1+p2? goldbach's conjecture is false. # provide a finder's fee if goldbach_counterexample == true: transfer_ethereum() The above program is guaranteed to halt after about O(n^2 * sqrt(n)) (depending on how great the is_not_prime function is). However, it is unknown if there is any input that causes `transfer_ethereum` to be executed. So if I find a counterexample, I can compute how much gas I need to pay to win my finder's fee. So sure, it runs in finite time for a given input, but you have to guarantee it won't ever execute the transfer_ethereum function for all inputs if you want to ensure you never pay out. And that, in general, for a general program (even if guaranteed to halt) is equivalent to the halting problem. Now, I believe that solidity has an upperbound on the size of it's inputs, so the parameter space is bounded, and we return to your original argument that it is a large, but exhaustible, search space.

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...

jeisc 9y ago

Does this title to a scholarly paper read like a newspaper headline to anyone but me? The trading level of ethereum has remained unchanged after the publication of this document?