3 ms·

I can't imagine running (or investing) in a software-based company here without also having an automatic model checking layer for verifying all runs + 24/7 moni

I can't imagine running (or investing) in a software-based company here without also having an automatic model checking layer for verifying all runs + 24/7 monitoring for disabling any live contract. If you're going to put $10M+, years of your life, and who knows how much customer money into this, why not spend $500K of it so you're running with the blockchain equiv of CI testing? You'd be able to deploy faster, with more confidence and less stress, and fewer of these weird midnight Europe phone calls. Viable model checkers for basic software contracts existed since the 80's, and the modern incarnations are insanely powerful (Z3, ...) + quite approachable (Rosette, ...). They're used to tackle software verification problems magnitudes harder than "money can only go from here to there in this tiny software contract": race detection in distributed file systems, bugs in hardware circuits, security holes in big javascript libraries, etc. I think of these same not-very-secret tools every time I see one of these articles, and yet the engineering fails keep happening. A few teams deploy tech here, including built on the above, but it seems like most do not. I'd say mind-blowing, but at this point... mind-numbing? I do appreciate the author being frank about how bad the status quo is. EDIT: To give a sense of this -- the same people will talk about meticulous cold storage key exchanges with someone always being there to watch, driving into the desert for bootstrapping secrets, and then for their actual operations, deploy unverified contracts.

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.
schoen 6y ago
> the same people will talk about meticulous cold storage key exchanges with someone always being there to watch, driving into the desert for bootstrapping secrets, and then for their actual operations, deploy unverified contracts Although they, or their predecessors, didn't necessarily do the former in the first few years of Bitcoin. Lots of exchanges, including the very biggest, were compromised and robbed. Maybe there's a cycle where particularly terrible outcomes help to create a new consensus on basic safety precautions.
tenuousemphasis 6y ago
You can validate your contract all you want, but if it matters in which order executions matter, you're still subject to the whims of the underlying blockchain.
- lmeyerov 6y ago
  That's something you can verify and fix, or decide to otherwise include in your risk calc. But yep, after looking at the hoops verification folks are having to jump through to run safe contracts on insecure blockchain VMs, maybe doing something else with your $ can also make sense.

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.

schoen 6y ago

> the same people will talk about meticulous cold storage key exchanges with someone always being there to watch, driving into the desert for bootstrapping secrets, and then for their actual operations, deploy unverified contracts Although they, or their predecessors, didn't necessarily do the former in the first few years of Bitcoin. Lots of exchanges, including the very biggest, were compromised and robbed. Maybe there's a cycle where particularly terrible outcomes help to create a new consensus on basic safety precautions.

tenuousemphasis 6y ago

You can validate your contract all you want, but if it matters in which order executions matter, you're still subject to the whims of the underlying blockchain.

lmeyerov 6y ago
That's something you can verify and fix, or decide to otherwise include in your risk calc. But yep, after looking at the hoops verification folks are having to jump through to run safe contracts on insecure blockchain VMs, maybe doing something else with your $ can also make sense.