2 ms·

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

by 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.
    - jasode 10y ago
      Notice that sprinkled throughout your multiple comments, you're hedging your position to provide some wiggle room: "would catch _most_ heists like this" "2% heist is _better_ than a 60% heist" ", and can come _closer_ to the ideal than anything else" However, I wasn't talking about degrees on a continuum such as "most/better/closer". I suspect that your prudent avoidance of absolutist statements actually gets to the idea I'm trying to convey. To recap, Jon Evan's asserts that Solidity can be "proved _correct_". Well, that's a boolean TRUE/FALSE instead of range of bad-to-good outcomes. >Yes, but formal methods are no more limited than any other approach, and can come closer to the ideal than anything else I'm not disagreeing with that particular statement. I'm not saying formal verfication doesn't help. It does help! I'm saying it's misapplied to the word "correct" in the sense that a mass of Ethereum users would understand that word. We are talking about 2 different levels of correctness: A) rules correctness: proven "correct" in the sense formal specification and program verification. Yes, this can be done but it will always be incomplete in how it maps to humans' idea of what is ultimately correct. B) intention correctness: proven "correct" in the sense of Solidity working the way humans would interpret as correct (I recommend reading Brian Cantwell Smith's essay on "The Limits of Correctness"[1]) To put another way, there exists an (unknown) set of programs that simultaneously satisfies both properties: 1) passed the formal verification rules with zero errors 2) judged as working incorrectly by humans which leads to a fork/reversal The existence of such programs contradicts Mr Evans statement. >Ethereum's heist was very clearly one of a program not conforming to (an informal) spec, that its creators had in mind. No it isn't clear. It sparked a deep philosophical debate. Ethereum's creators had an informal spec of the "code _IS_ the contract" and not "the code is PROVISIONAL and humans forking the code is the ultimate contract". For a vocal subset of Ethereum users, the heist did conform to their (incomplete) spec! The word "incomplete" shouldn't be in parentheses because every finite specification is incomplete against unforseen hacks. [1]https://www.student.cs.uwaterloo.ca/~cs492/11public_html/p18-smith.pdf https://www.student.cs.uwaterloo.ca/~cs492/11public_html/p18...

by jasode 10y ago

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.
  - jasode 10y ago
    Notice that sprinkled throughout your multiple comments, you're hedging your position to provide some wiggle room: "would catch _most_ heists like this" "2% heist is _better_ than a 60% heist" ", and can come _closer_ to the ideal than anything else" However, I wasn't talking about degrees on a continuum such as "most/better/closer". I suspect that your prudent avoidance of absolutist statements actually gets to the idea I'm trying to convey. To recap, Jon Evan's asserts that Solidity can be "proved _correct_". Well, that's a boolean TRUE/FALSE instead of range of bad-to-good outcomes. >Yes, but formal methods are no more limited than any other approach, and can come closer to the ideal than anything else I'm not disagreeing with that particular statement. I'm not saying formal verfication doesn't help. It does help! I'm saying it's misapplied to the word "correct" in the sense that a mass of Ethereum users would understand that word. We are talking about 2 different levels of correctness: A) rules correctness: proven "correct" in the sense formal specification and program verification. Yes, this can be done but it will always be incomplete in how it maps to humans' idea of what is ultimately correct. B) intention correctness: proven "correct" in the sense of Solidity working the way humans would interpret as correct (I recommend reading Brian Cantwell Smith's essay on "The Limits of Correctness"[1]) To put another way, there exists an (unknown) set of programs that simultaneously satisfies both properties: 1) passed the formal verification rules with zero errors 2) judged as working incorrectly by humans which leads to a fork/reversal The existence of such programs contradicts Mr Evans statement. >Ethereum's heist was very clearly one of a program not conforming to (an informal) spec, that its creators had in mind. No it isn't clear. It sparked a deep philosophical debate. Ethereum's creators had an informal spec of the "code _IS_ the contract" and not "the code is PROVISIONAL and humans forking the code is the ultimate contract". For a vocal subset of Ethereum users, the heist did conform to their (incomplete) spec! The word "incomplete" shouldn't be in parentheses because every finite specification is incomplete against unforseen hacks. [1]https://www.student.cs.uwaterloo.ca/~cs492/11public_html/p18-smith.pdf https://www.student.cs.uwaterloo.ca/~cs492/11public_html/p18...