> 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.
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.
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
> 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 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.
smart contracts cannot make use of information from the outside world (unless of course, fed from a single centralized party).
There has been some work on taking the median of multiple oracles, requiring oracles to post collateral that will be forfeited if they disagree too much with the others, and using attested hardware (SGX) to make oracles more auditable.
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.
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.
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.
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.
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.
A smart contract, once published, cannot be amended.
Not entirely true. You can have storage variable pointing to an external contract which contains the logic, and this variable can be updating after deployment.
Correct, but it's only the case if one has thought of this scenario in advance and cared to instrument the contract with this indirection via mutable state. That said, this logic will still be fixed once the contract is deployed.
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
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.
> 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?