3 ms·

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

by 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.
- ahelwer 10y ago
  Ah, I see what you mean. The fork would break the execution model/reality equivalence and thus (possibly) invalidate the verified properties. It could also modify the Solidity code itself, as in the DAO fork. Formal verification still provides benefit here: the proposed changes are easy to check for backwards-compatibility breakage prior to the fork, providing a valuable political tool to either oppose the change or require a rider contract code fix in the fork. I do think your requirement of universal correctness is unfair. We can rightfully criticize the naivete or misleading marketing of Ethereum, but the system isn't valueless despite its limitations, and formal verification enables us to capture more of that value.

by ahelwer 10y ago

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.

ahelwer 10y ago
Ah, I see what you mean. The fork would break the execution model/reality equivalence and thus (possibly) invalidate the verified properties. It could also modify the Solidity code itself, as in the DAO fork. Formal verification still provides benefit here: the proposed changes are easy to check for backwards-compatibility breakage prior to the fork, providing a valuable political tool to either oppose the change or require a rider contract code fix in the fork. I do think your requirement of universal correctness is unfair. We can rightfully criticize the naivete or misleading marketing of Ethereum, but the system isn't valueless despite its limitations, and formal verification enables us to capture more of that value.