4 ms·

I hate to be that guy but you are vastly underestimating the challenge of formally verifying these software systems. Blockchains are highly adversarial, open so

by Taek 6y ago

I hate to be that guy but you are vastly underestimating the challenge of formally verifying these software systems. Blockchains are highly adversarial, open source, and doing a lot of innovation. Innovation which means that nobody has ever tried to verify that type of system before. Model checkers can tell you thinks like 'there are no underflows' and 'these two pieces of code are identical', but if you want to know whether there is no arbitrage or front-running, you're well past the capabilities of the state of the art. It's not merely a matter of spending $500k on CI and auditing. And then you've got a separate issue, which is that the space is super competitive and moves extremely fast. If you spend 6 weeks getting your new contract audited, you may well miss the window where people will care about the project you launched. I don't think this is a healthy culture, but it is one that many teams are trying to compete in. And therefore they ARE willing to bet millions of dollars without taking any time to audit, because the expected value of deploying faster is higher than the expected value of deploying more safely. For projects that are comfortable moving more slowly, formal verification IS a big focus, and the cryptocurrency industry has been a material driving force in many security related technologies such as reproducible builds (Gitian), reproducible bootstrapping (Guix), and software verification methodologies.

lmeyerov 6y ago
For background, I've built verifiers for harder languages, reviewed papers for crypto systems, seen the inside of crypto operations & crypto security startups, and help build software for adversarial, investigative, & high performance scenarios. I'm not an expert in blockchain stuff, but I'm also not unfamiliar with the software challenges. * I would agree that paying consultants to audit contracts is prohibitively expensive. It's the equivalent of paying pen testers to do your unit testing & security engineering - that's a costly way to do your basics * I disagree that model checkers can't check for stuff like front-running. It's not textbook, but close: the first papers on model checkers were specifically temporal logic for stuff like ordering issues. That was ~35 years ago! Contracts are similar in size, and both computers + solvers have gotten exponentially better. For my day job, we do TLFOPS for $0.20/hr, in Python. * Reproducible builds, bootstrapping, etc. are real... but the 20%, and skipping the 80% I'm talking about. Verifiable VM IRs + verifiable contract lang subsets + contracts verified against them. Yes, we've seen sw supplychain attacks against some projects. More than that? Buggy contracts, buggy contract libs, & buggy blockchains. I get that crypto startup people don't know this stuff, but you can hire 1-2 devs (= $500K) that can. Even if verifying against full abstraction is likely out of reach due to the security mess that is the ETH VM & friends, chiseling out subsets and running the model checking equiv of fuzzers isn't hard. The status quo of not doing it makes it look like an industry of folks not running unit tests before pushing to prod. (See: article.) It's not that hard. As more money gets into any company here, my expectations go higher, even if that industry's haven't.
- literallycancer 6y ago
  How do you check for front running? What if your checker tells you that you can't fix it just by changing your own code?
  - lmeyerov 6y ago
    I'm unclear what level you're asking this at. -- Modeling: You start with basics like using the small universe assumption to bound checking to X transactions. I'd expect most front running to show up as small cycles here, so the typical case is a super small X. Later, you might get into a time cost semantics to better tune what you consider interesting, but almost no one in the crypto space is at the level of modeling maturity. I'd predict a team's time is way better spent building up a stdlib of contract checks, verified contract helpers, & whitebox attack heuristics/guides. -- Modeling II: Also, in verification, it's way better (ex: realizes more of the ROI) to verify the program has the properties you want ("money goes from a->b without getting stuck"). You can dream up individual attacks and model those one by one ("front-running where ..."), but then you potentially miss some, or some aspect of one. That's basically the difference between verification and testing. You still do stuff like check sample scenarios & individual attacks, but that's more about testing the verification conditions & model fidelity. -- Fixes: A good (while still cheap & easy) checker gives you summarized examples of attacks. Likewise, it makes it interactive, so you can tune what you consider in/out of scope. More R&D-level verifiers suggest patches (verification and synthesis are two sides of the same coin), but that's not necessary. If your idea sucks or the attack is unavoidable, the verifier isn't the problem, and if you decide to still proceed with the now proven-bad idea, you can at least now price the risk in.
    - literallycancer 6y ago
      In the article the attacker simply pays a higher fee to have their call executed first. How does verification help you in this case? It sounds a bit like it would just tell you that your design sucks and you need to change it, but that's not really helpful if it does that for all designs you can come up with. I'm not convinced you can spend 500k and make the problem go away. If it turns out the problem can only be fixed by changing the underlying platform, rather than your contracts, you will spend years talking to stakeholders and advocating for the necessary changes. Which you still have to come up with yourself. Unless your solver somehow finds the correct solution? Another reason why that budget is suspect is that you'd have to develop most of that from scratch. There certainly isn't an existing set of mature tools like there might be for verifying properties of C++ code. Unless you make the problem go away, you are not going to be better off hiring people. Front runners let one know there is a problem just as well as a verification consultant. Proving that an attack is unavoidable might at least save some time. Proving that a specific solution doesn't work doesn't really help you find the correct one (?)
sterlind 6y ago
There should actually be a big market for formal verification tools: malicious users can use them to find and exploit buggy contracts. I imagine this will happen after the low-hanging fruit (the front-runners described in this article) is gone. Providing formal security proofs may be forever out of reach, but if the tools get expressive eventually it'll be a battle of who can throw the most CPU at the solver, to the point where no cost incentive remains. Either way, it will spur developers to use these tools before their attackers do.
- 3np 6y ago
  Runtime Verification (no affiliation, just know some people who have worked with or for them) are working on tools and providing services for things like this https://runtimeverification.com/ https://runtimeverification.com/

by Taek 6y ago

lmeyerov 6y ago

For background, I've built verifiers for harder languages, reviewed papers for crypto systems, seen the inside of crypto operations & crypto security startups, and help build software for adversarial, investigative, & high performance scenarios. I'm not an expert in blockchain stuff, but I'm also not unfamiliar with the software challenges. * I would agree that paying consultants to audit contracts is prohibitively expensive. It's the equivalent of paying pen testers to do your unit testing & security engineering - that's a costly way to do your basics * I disagree that model checkers can't check for stuff like front-running. It's not textbook, but close: the first papers on model checkers were specifically temporal logic for stuff like ordering issues. That was ~35 years ago! Contracts are similar in size, and both computers + solvers have gotten exponentially better. For my day job, we do TLFOPS for $0.20/hr, in Python. * Reproducible builds, bootstrapping, etc. are real... but the 20%, and skipping the 80% I'm talking about. Verifiable VM IRs + verifiable contract lang subsets + contracts verified against them. Yes, we've seen sw supplychain attacks against some projects. More than that? Buggy contracts, buggy contract libs, & buggy blockchains. I get that crypto startup people don't know this stuff, but you can hire 1-2 devs (= $500K) that can. Even if verifying against full abstraction is likely out of reach due to the security mess that is the ETH VM & friends, chiseling out subsets and running the model checking equiv of fuzzers isn't hard. The status quo of not doing it makes it look like an industry of folks not running unit tests before pushing to prod. (See: article.) It's not that hard. As more money gets into any company here, my expectations go higher, even if that industry's haven't.

literallycancer 6y ago
How do you check for front running? What if your checker tells you that you can't fix it just by changing your own code?
- lmeyerov 6y ago
  I'm unclear what level you're asking this at. -- Modeling: You start with basics like using the small universe assumption to bound checking to X transactions. I'd expect most front running to show up as small cycles here, so the typical case is a super small X. Later, you might get into a time cost semantics to better tune what you consider interesting, but almost no one in the crypto space is at the level of modeling maturity. I'd predict a team's time is way better spent building up a stdlib of contract checks, verified contract helpers, & whitebox attack heuristics/guides. -- Modeling II: Also, in verification, it's way better (ex: realizes more of the ROI) to verify the program has the properties you want ("money goes from a->b without getting stuck"). You can dream up individual attacks and model those one by one ("front-running where ..."), but then you potentially miss some, or some aspect of one. That's basically the difference between verification and testing. You still do stuff like check sample scenarios & individual attacks, but that's more about testing the verification conditions & model fidelity. -- Fixes: A good (while still cheap & easy) checker gives you summarized examples of attacks. Likewise, it makes it interactive, so you can tune what you consider in/out of scope. More R&D-level verifiers suggest patches (verification and synthesis are two sides of the same coin), but that's not necessary. If your idea sucks or the attack is unavoidable, the verifier isn't the problem, and if you decide to still proceed with the now proven-bad idea, you can at least now price the risk in.
  - literallycancer 6y ago
    In the article the attacker simply pays a higher fee to have their call executed first. How does verification help you in this case? It sounds a bit like it would just tell you that your design sucks and you need to change it, but that's not really helpful if it does that for all designs you can come up with. I'm not convinced you can spend 500k and make the problem go away. If it turns out the problem can only be fixed by changing the underlying platform, rather than your contracts, you will spend years talking to stakeholders and advocating for the necessary changes. Which you still have to come up with yourself. Unless your solver somehow finds the correct solution? Another reason why that budget is suspect is that you'd have to develop most of that from scratch. There certainly isn't an existing set of mature tools like there might be for verifying properties of C++ code. Unless you make the problem go away, you are not going to be better off hiring people. Front runners let one know there is a problem just as well as a verification consultant. Proving that an attack is unavoidable might at least save some time. Proving that a specific solution doesn't work doesn't really help you find the correct one (?)

sterlind 6y ago

There should actually be a big market for formal verification tools: malicious users can use them to find and exploit buggy contracts. I imagine this will happen after the low-hanging fruit (the front-runners described in this article) is gone. Providing formal security proofs may be forever out of reach, but if the tools get expressive eventually it'll be a battle of who can throw the most CPU at the solver, to the point where no cost incentive remains. Either way, it will spur developers to use these tools before their attackers do.

3np 6y ago
Runtime Verification (no affiliation, just know some people who have worked with or for them) are working on tools and providing services for things like this https://runtimeverification.com/ https://runtimeverification.com/