3 ms·

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 (?)
  - 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.
zaphar 6y ago
If you can't fix it maybe you shouldn't deploy it. It's like knowing you have a bug that will result in a 50/50 chance of losing customers money. It would be irresponsible to deploy code like that.

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

zaphar 6y ago

If you can't fix it maybe you shouldn't deploy it. It's like knowing you have a bug that will result in a 50/50 chance of losing customers money. It would be irresponsible to deploy code like that.