3 ms·

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 wo

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 (?)

lmeyerov 6y ago
A couple things here didn't make sense to me: * $500K / develop from scratch is too expensive: Nope! I actually hedged by ~10X :) In reality, I'd advocate building successively better verifiers as more & more money flows through, with the first solid prototype being $20K-$50K. One good MS/PhD student in the verification community can build a decent toolkit over a summer (= $20-50K). The reason is that tools like those I mentioned earlier are intentionally language-agnostic and part of 15+ year movement of building out lightweight generic toolkits for this stuff. Think of it like a CI system: you get most bang for the buck by building out basic unit tests early on, and as your system becomes worth more $, get into integration testing, and one day, chaos engineering. Same for different levels of verifiers. * Some problems are inherent to all designs...yet you're better off hiring people? That doesn't make sense to me. What are the expensive per-contract outside people going to do if they can't fix the bug? That's worst of both worlds! When a verifier flags the issue, if a team can't figure out a fix, at least now they can now mitigate the risk (e.g., shut it off, only put in so much money, get insurance, hedge/diversify, monitor for the exploit happening, ..). My broader statement is verification tech is increasingly accessible and building out some of it for an org deploying contracts is similar to a utility co building out monitoring or a software shop building out CI. Not for the weekend coder, but should be basic engineering for a professional shop.

lmeyerov 6y ago

A couple things here didn't make sense to me: * $500K / develop from scratch is too expensive: Nope! I actually hedged by ~10X :) In reality, I'd advocate building successively better verifiers as more & more money flows through, with the first solid prototype being $20K-$50K. One good MS/PhD student in the verification community can build a decent toolkit over a summer (= $20-50K). The reason is that tools like those I mentioned earlier are intentionally language-agnostic and part of 15+ year movement of building out lightweight generic toolkits for this stuff. Think of it like a CI system: you get most bang for the buck by building out basic unit tests early on, and as your system becomes worth more $, get into integration testing, and one day, chaos engineering. Same for different levels of verifiers. * Some problems are inherent to all designs...yet you're better off hiring people? That doesn't make sense to me. What are the expensive per-contract outside people going to do if they can't fix the bug? That's worst of both worlds! When a verifier flags the issue, if a team can't figure out a fix, at least now they can now mitigate the risk (e.g., shut it off, only put in so much money, get insurance, hedge/diversify, monitor for the exploit happening, ..). My broader statement is verification tech is increasingly accessible and building out some of it for an org deploying contracts is similar to a utility co building out monitoring or a software shop building out CI. Not for the weekend coder, but should be basic engineering for a professional shop.