6 ms·

The important question is if you think it's possible to create impervious functions of ~100 lines of code. I tend to think that with modern formal verification

The important question is if you think it's possible to create impervious functions of ~100 lines of code. I tend to think that with modern formal verification systems this is a feasible goal. Otherwise you have to stick with closed-source security-through-obscurity and rely on legal reversal. This seems pretty weak to me, though - ex, if a stock exchange was hacked, sure you could reverse it legally, but the market disruption would take years to recover. Regardless of the specific nature of crypto, I think formally verifiable open systems are both achievable and a worthwhile goal.

mannykannot 8y ago
I am not sure what your position here is: that you can do whatever you want, or at least a lot of useful things, in ~100 lines of code? That if your software is broken down into functions no bigger that ~100 lines of code, and they have each been individually verified, then their composition has also been verified? Or something else? There is also the matter of verifying the platform itself.
- CryptoPunk 8y ago
  Regarding your last point, the platform itself can be fixed if it has any malfunctions. The issue is only with an application built on top of the platform malfunctioning while the platform operates exactly as it's supposed to. In that case there is no redress as the platform is for all intents and purposes immutable when it's working correctly.
  - mannykannot 8y ago
    You are seriously underestimating what it would take to verify the platform. We are not talking about just a few hundreds of lines of code here.
    - CryptoPunk 8y ago
      What I meant is that an error in the platform is not catastrophic, because in those cases, the blockchain can be paused, fixed, and if need be, rolled back. In other words, errors that occur due to malfunctions in the platform are reversible. Errors in applications built on top of it are not.
- xwvvvvwx 8y ago
  > There is also the matter of verifying the platform itself The Ethereum virtual machine has been formally verified. https://www.ideals.illinois.edu/handle/2142/97207 https://www.ideals.illinois.edu/handle/2142/97207
  - mannykannot 8y ago
    Thank you for bringing this to my attention. If I am following along correctly, it does not so much verify the deployed EVM as it provides a formal and executable semantics for an EVM that satisfies the test suite, and the authors demonstrate its use in finding some real-world problems, which is exactly the sort of thing that we want: "These properties make KEVM an ideal formal reference implementation against which other implementations can be evaluated. We proceed to argue for a semantics-first formal verification approach for EVM contracts, and demonstrate its practicality by using KEVM to verify practically important properties over the arithmetic operation of an example smart contract and the correct operation of a token transfer function in a second contract." From the paper, it seems that the latter example could have found a bug that caused problems in a deployed Ethereum contract.

mannykannot 8y ago

I am not sure what your position here is: that you can do whatever you want, or at least a lot of useful things, in ~100 lines of code? That if your software is broken down into functions no bigger that ~100 lines of code, and they have each been individually verified, then their composition has also been verified? Or something else? There is also the matter of verifying the platform itself.

CryptoPunk 8y ago
Regarding your last point, the platform itself can be fixed if it has any malfunctions. The issue is only with an application built on top of the platform malfunctioning while the platform operates exactly as it's supposed to. In that case there is no redress as the platform is for all intents and purposes immutable when it's working correctly.
- mannykannot 8y ago
  You are seriously underestimating what it would take to verify the platform. We are not talking about just a few hundreds of lines of code here.
  - CryptoPunk 8y ago
    What I meant is that an error in the platform is not catastrophic, because in those cases, the blockchain can be paused, fixed, and if need be, rolled back. In other words, errors that occur due to malfunctions in the platform are reversible. Errors in applications built on top of it are not.
xwvvvvwx 8y ago
> There is also the matter of verifying the platform itself The Ethereum virtual machine has been formally verified. https://www.ideals.illinois.edu/handle/2142/97207 https://www.ideals.illinois.edu/handle/2142/97207
- mannykannot 8y ago
  Thank you for bringing this to my attention. If I am following along correctly, it does not so much verify the deployed EVM as it provides a formal and executable semantics for an EVM that satisfies the test suite, and the authors demonstrate its use in finding some real-world problems, which is exactly the sort of thing that we want: "These properties make KEVM an ideal formal reference implementation against which other implementations can be evaluated. We proceed to argue for a semantics-first formal verification approach for EVM contracts, and demonstrate its practicality by using KEVM to verify practically important properties over the arithmetic operation of an example smart contract and the correct operation of a token transfer function in a second contract." From the paper, it seems that the latter example could have found a bug that caused problems in a deployed Ethereum contract.