5 ms·

>Everything is terrible because the fundamental tools we use are, still, so flawed that when used they inevitably craft terrible things. This applies to softwar

by jasode 10y ago

>Everything is terrible because the fundamental tools we use are, still, so flawed that when used they inevitably craft terrible things. This applies to software [...] like the $150 million Ethereum DAO catastrophe. [...] >In principle, code can be proved correct with formal verification. Formal verification is not applicable to the DAO hack that lead to some humans to decide on forking the blockchain. Correctness in that example was in the eye of the beholder and from the perspective of the hacker that received the digital currency, it would have been formally verified as "correct".

pron 10y ago
I don't know the details, but I doubt this is true. In this case, correctness was "in the eye of the beholder" simply because they decided that the code is the contract. But when you formally verify, you can specify a set of safety properties, each usually very simple, and expressed in a line or two. Of course, you could miss a critical property, but it's very likely that you'd add at least some sanity properties that would catch most heists like this (e.g., "no more than 2% of the money can end up in the same account", or something like that).
- jasode 10y ago
  >, but it's very likely that you'd add at least some sanity properties that would catch most heists like this (e.g., "no more than 2% of the money can end up in the same account", or something like that). And then new Solidity programming code that moves 1.9999% of the money into a single account gets passed. The hacker who exploited the 2% threshold to his advantage thinks it's formally verified as "correct." The people who "lost" their money thinks it wasn't "correct." Add new verification "rules" in an attempt to close a loophole, wait for the next exploit. Rinse and repeat. Solidity programming code all by itself can't serve as the ultimate authority for smart contracts.
  - pron 10y ago
    I think you'd agree that a 2% heist is better than a 60% heist. BTW, I don't advocate automatic contracts (personally I think the whole premise is dumb and misunderstands what a contract is), nor do I claim that formal verification is easy. It takes practice to know what to verify, at what level, and how to trust the results. But if it is used properly, it can really help.
    - jasode 10y ago
      >I think you'd agree that a 2% heist is better than a 60% heist. Sure, but I was talking about a much more rigorous standard than "2% better than 60%" because the author Jon Evans wrote: ""In principle, code can be proved _correct _ with formal verification."" I'm not sure he understands what "correct" actually means. If Mr Evans is framing "correct" in the sense of corresponding to a spec (see ahelwer's excellent comment as an example), it still doesn't solve how everybody else determines how Ethereum to behaving "correctly". (E.g. the code passed the spec checker, but it's still judged as incorrect.) Those are 2 different levels of correctness and formal verification algorithms has limited power to solve the "human judgement of correctness".
      - pron 10y ago
        > and formal verification algorithms has limited power to solve the "human judgement of correctness". Yes, but formal methods are no more limited than any other approach, and can come closer to the ideal than anything else -- for a price. BTW, we do not usually speak of "formal verification algorithms", just as we do not usually speak of "programming algorithms" or "testing algorithms". Formal verification is a human process, akin (and complementary) to programming or testing. The general idea is that the developers express the properties they'd like the program to have in a few short formal sentences, and then the program is proven (or verified in some other way) to conform with that specification. Nothing can prevent the problem of humans failing to express what they really mean. In fact, this is a problem with contracts more than anything else, because contracts need to accommodate many contingencies, which is why I think that the whole notion of machine contracts is rather foolish. But the technical point is that the specific problem with Ethereum's heist was very clearly one of a program not conforming to (an informal) spec, that its creators had in mind.
Animats 10y ago
As I've commented before, the trouble with Etherium contracts is that they're Turing-complete executable code. You don't need or want Turing-complete contracts. Contracts should have been something more declarative and more readable, such as a decision table.
- pron 10y ago
  Turing completeness is a red herring in this case. Even FSMs are not feasibly verifiable in general, so both the richest computational model and the most limited can only be feasibly verified in specific cases. Some properties can make verification easier or harder, but Turing completeness or lack thereof is not among them. Insofar language or representation can help, some classes of simple bugs can be prevented with the right language, and a formalism that captures how people think of contracts may help, too (e.g. behavioral programming: http://www.wisdom.weizmann.ac.il/~bprogram/ http://www.wisdom.weizmann.ac.il/~bprogram/) If anything, the problem is that contracts are a very complicated thing in the first place. Even rich formalisms would likely fail to account for all cases you want a contract to cover.
  - Animats 10y ago
    If you can handle purchases, loans, negotiable bills of lading, equity investments, and derivatives, you probably have the important use cases covered. Trying to support transactions of types not in standard business textbooks is excess functionality leading to bugs.
    - woah 10y ago
      The dao hack was the result of a textbook concurrency error, similar to errors that can result from not using database transactions. Crippling the language is not the answer. Just look at code that works with Bitcoin. It is convoluted beyond belief. Read the Lightning whitepaper. It's 60 pages of complex hacks to accomplish something that can be explained in 5 minutes (if you don't have to jump through the Bitcoin hoops), and implemented in a few hundred lines of ethereum code.
ahelwer 10y ago
Software correctness does not work like that. The DAO code as written allowed the theft, yes, and indeed was fully correct with regard to its specification - that is, itself. Formal specification would involve writing safety properties in a higher-level language, and a machine-checked proof that the Solidity code enforced these properties. This ensures correctness of the Solidity code subject to correctness of the proof checker, execution model equivalence with reality, consistency of ZFC, etc. etc. As you pointed out below, the safety properties validated could be irrelevant, poorly-formed, or (as a whole) incomplete. This is true, and also insurmountable - the chain of correctness has to start somewhere. Right now we have only an idea in someone's head, then Solidity code. The gap between the two is enormous and equivalence unverifiable. A higher-level spec greatly reduces the size of this gap and will catch the vast majority of bugs.
- jasode 10y ago
  > writing safety properties in a higher-level language, >This is true, and also insurmountable - the chain of correctness has to start somewhere. Exactly! We can shift the "correctness" test to correspond with the spec of the hypothetical higher language. But, we haven't actually solved for universal correctness as it corresponds with how humans would ultimately decide what's correct. In other words, the following function can be (trivially) formally verified: int increment_by_one(int x) { return x+1;} If int is signed 32-bits, one could brute force the tests for all 4,294,967,295 possible inputs. If x happens to be 2,147,483,647 and depending on the higher-level spec, one could define "correct" to abort with an error, or simply wrap around to a negative number. However, the standard of "correctness" for Ethereum is much higher than that. Let's say there's an unwanted event called Humans Will Decide To Fork Ethereum Because Of Unforseen Solidity Behavior which we'll abbreviate as HWDTFEBOUSB. I contend the following static checker that correctly returns TRUE or FALSE is impossible to write: bool HWDTFEBOUSB(string Solidity_code) In the context where you mentioned "insurmountable", I believe we are using the same frame of reference and are in agreement. Is my insistence on universal correctness an unfair standard? I don't think so because Ethereum creators wanted the programming code in "smart contracts" to be the ultimate and final arbiter. No follies of human judgement or politics to "pollute" the transactions. If that's the goal, just using a higher level language as a specification language for formal verification engines is not enough.

by jasode 10y ago

pron 10y ago

I don't know the details, but I doubt this is true. In this case, correctness was "in the eye of the beholder" simply because they decided that the code is the contract. But when you formally verify, you can specify a set of safety properties, each usually very simple, and expressed in a line or two. Of course, you could miss a critical property, but it's very likely that you'd add at least some sanity properties that would catch most heists like this (e.g., "no more than 2% of the money can end up in the same account", or something like that).

jasode 10y ago
>, but it's very likely that you'd add at least some sanity properties that would catch most heists like this (e.g., "no more than 2% of the money can end up in the same account", or something like that). And then new Solidity programming code that moves 1.9999% of the money into a single account gets passed. The hacker who exploited the 2% threshold to his advantage thinks it's formally verified as "correct." The people who "lost" their money thinks it wasn't "correct." Add new verification "rules" in an attempt to close a loophole, wait for the next exploit. Rinse and repeat. Solidity programming code all by itself can't serve as the ultimate authority for smart contracts.
- pron 10y ago
  I think you'd agree that a 2% heist is better than a 60% heist. BTW, I don't advocate automatic contracts (personally I think the whole premise is dumb and misunderstands what a contract is), nor do I claim that formal verification is easy. It takes practice to know what to verify, at what level, and how to trust the results. But if it is used properly, it can really help.
  - jasode 10y ago
    >I think you'd agree that a 2% heist is better than a 60% heist. Sure, but I was talking about a much more rigorous standard than "2% better than 60%" because the author Jon Evans wrote: ""In principle, code can be proved _correct _ with formal verification."" I'm not sure he understands what "correct" actually means. If Mr Evans is framing "correct" in the sense of corresponding to a spec (see ahelwer's excellent comment as an example), it still doesn't solve how everybody else determines how Ethereum to behaving "correctly". (E.g. the code passed the spec checker, but it's still judged as incorrect.) Those are 2 different levels of correctness and formal verification algorithms has limited power to solve the "human judgement of correctness".
    - pron 10y ago
      > and formal verification algorithms has limited power to solve the "human judgement of correctness". Yes, but formal methods are no more limited than any other approach, and can come closer to the ideal than anything else -- for a price. BTW, we do not usually speak of "formal verification algorithms", just as we do not usually speak of "programming algorithms" or "testing algorithms". Formal verification is a human process, akin (and complementary) to programming or testing. The general idea is that the developers express the properties they'd like the program to have in a few short formal sentences, and then the program is proven (or verified in some other way) to conform with that specification. Nothing can prevent the problem of humans failing to express what they really mean. In fact, this is a problem with contracts more than anything else, because contracts need to accommodate many contingencies, which is why I think that the whole notion of machine contracts is rather foolish. But the technical point is that the specific problem with Ethereum's heist was very clearly one of a program not conforming to (an informal) spec, that its creators had in mind.

Animats 10y ago

As I've commented before, the trouble with Etherium contracts is that they're Turing-complete executable code. You don't need or want Turing-complete contracts. Contracts should have been something more declarative and more readable, such as a decision table.

pron 10y ago
Turing completeness is a red herring in this case. Even FSMs are not feasibly verifiable in general, so both the richest computational model and the most limited can only be feasibly verified in specific cases. Some properties can make verification easier or harder, but Turing completeness or lack thereof is not among them. Insofar language or representation can help, some classes of simple bugs can be prevented with the right language, and a formalism that captures how people think of contracts may help, too (e.g. behavioral programming: http://www.wisdom.weizmann.ac.il/~bprogram/ http://www.wisdom.weizmann.ac.il/~bprogram/) If anything, the problem is that contracts are a very complicated thing in the first place. Even rich formalisms would likely fail to account for all cases you want a contract to cover.
- Animats 10y ago
  If you can handle purchases, loans, negotiable bills of lading, equity investments, and derivatives, you probably have the important use cases covered. Trying to support transactions of types not in standard business textbooks is excess functionality leading to bugs.
  - woah 10y ago
    The dao hack was the result of a textbook concurrency error, similar to errors that can result from not using database transactions. Crippling the language is not the answer. Just look at code that works with Bitcoin. It is convoluted beyond belief. Read the Lightning whitepaper. It's 60 pages of complex hacks to accomplish something that can be explained in 5 minutes (if you don't have to jump through the Bitcoin hoops), and implemented in a few hundred lines of ethereum code.

ahelwer 10y ago

Software correctness does not work like that. The DAO code as written allowed the theft, yes, and indeed was fully correct with regard to its specification - that is, itself. Formal specification would involve writing safety properties in a higher-level language, and a machine-checked proof that the Solidity code enforced these properties. This ensures correctness of the Solidity code subject to correctness of the proof checker, execution model equivalence with reality, consistency of ZFC, etc. etc. As you pointed out below, the safety properties validated could be irrelevant, poorly-formed, or (as a whole) incomplete. This is true, and also insurmountable - the chain of correctness has to start somewhere. Right now we have only an idea in someone's head, then Solidity code. The gap between the two is enormous and equivalence unverifiable. A higher-level spec greatly reduces the size of this gap and will catch the vast majority of bugs.

jasode 10y ago
> writing safety properties in a higher-level language, >This is true, and also insurmountable - the chain of correctness has to start somewhere. Exactly! We can shift the "correctness" test to correspond with the spec of the hypothetical higher language. But, we haven't actually solved for universal correctness as it corresponds with how humans would ultimately decide what's correct. In other words, the following function can be (trivially) formally verified: int increment_by_one(int x) { return x+1;} If int is signed 32-bits, one could brute force the tests for all 4,294,967,295 possible inputs. If x happens to be 2,147,483,647 and depending on the higher-level spec, one could define "correct" to abort with an error, or simply wrap around to a negative number. However, the standard of "correctness" for Ethereum is much higher than that. Let's say there's an unwanted event called Humans Will Decide To Fork Ethereum Because Of Unforseen Solidity Behavior which we'll abbreviate as HWDTFEBOUSB. I contend the following static checker that correctly returns TRUE or FALSE is impossible to write: bool HWDTFEBOUSB(string Solidity_code) In the context where you mentioned "insurmountable", I believe we are using the same frame of reference and are in agreement. Is my insistence on universal correctness an unfair standard? I don't think so because Ethereum creators wanted the programming code in "smart contracts" to be the ultimate and final arbiter. No follies of human judgement or politics to "pollute" the transactions. If that's the goal, just using a higher level language as a specification language for formal verification engines is not enough.