🔒 Consider Adding Invariant Testing for ERC20, ERC721, and ERC4626

[engn33r]

When ERC4626 was added to snekmate, property tests from https://github.com/a16z/erc4626-tests were added. More recently, Trail of Bits wrote some property tests that are similar but could offer additional assurance https://github.com/crytic/properties.

I have not tested these property tests yet, but they may be worth adding here. But if the existing test coverage is strong, then these may not provide much benefit.

Thoughts on whether this might be useful to explore now that vyper support in echidna has improved?

[pcaversaccio]

Hey @engn33r, thanks for sharing this idea! Is there somewhere a comparison about the difference between both test properties? So, personally, I prefer very much to continue keeping a16z/erc4626-tests for the following reasons:

• It has awesome coverage when it comes to testing the standard requirements of a given ERC4626 implementation (🐍 snekmate contracts will serve as library modules, implementing the standard requirements eventually);
• Amongst others, OpenZeppelin and Solmate integrate the test suite and we haven't seen any attack yet on a vault implementing these invariant tests (somehow confirming, in black hat terms, the effectiveness of the implemented invariant tests). FWIW, I found a small inconsistency in Solmate's implementation however here;
• Also, the current test suite nicely tests for the inflation attack mitigation, and I also collaborated with OZ on this (see, e.g., here). So we got that covered as well already IMO;
• For symbolic testing of the contracts (including ERC20 and ERC721) I plan to implement Halmos (see 💥 Integrate 🐍 snekmate Contracts With Halmos #180);
• While I deem Echidna as very valuable, I challenge how it can substantially increase the current test coverage & given the current roadmap with Halmos;

Thougths?

[engn33r]

I can only point to the blog post overview of the tests at https://blog.trailofbits.com/2023/02/27/reusable-properties-ethereum-contracts-echidna/ but I will call in @bsamuels453 who probably can better speak to what the property tests enable.

[bsamuels453]

Echidna vs. Foundry

The big difference between Echidna and Foundry fuzzing is that Echidna uses stateful fuzzing and Foundry uses stateless fuzzing.

This means certain issues cannot be detected using Foundry fuzzing unless an explicit test case is built for the test case in mind. The recent Raft finance hack is a good example of a hack that likely could not be detected using Foundry fuzzing due to the necessity of chaining multiple bugs + calls together to create a property violation.

Another big difference worth calling out is that Echidna is coverage-guided and Foundry is not. Echidna will prefer picking corpus parameters that increase coverage as much as possible. This makes intuitive sense, but it's hard to truly measure the difference because of the stateful vs. stateless detail.

While Halmos is a very cool tool, I think it only makes sense as an extension of stateless fuzzing that compensates for Foundry's poor corpus selection. Halmos won't be able to detect issues that require specific state transitions that a stateful fuzzer can achieve.

a16z tests vs. crytic/properties

Because of the differences between each fuzzer, crytic/properties is written for stateful fuzzing. As I mentioned before, it's very challenging to qualitatively measure the difference between stateful and stateless fuzzing, but according to the math, stateful should be better.

I think the only test crytic/properties has that are clearly superior to a16z is the rounding direction detector, but it's a bit challenging to set up which may impede your use case.

Anyways, if there's any devops issues/friction you've experienced with integrating Echidna with your system, pls let me know so we can get issues filed.

[pcaversaccio]

I'm tracking this initiative here: #184. @engn33r is this something you would be interested in tackling yourself?

[engn33r]

I won't have time for the coming month, but I set a reminder on my calendar for late Dec to see if I can help out then

[bsamuels453]

sounds like you know what you're doing @pcaversaccio ; Was your talk at TrustX? Wanna look it up once it gets put online

[pcaversaccio]

@bsamuels453 well, at least I try my best, and I always listen to constructive feedback. But it doesn't imply of course that I will ever achieve 100% secure code for 🐍 snekmate 🙃. My talk was part of the Vyper day. They recorded it but haven't published it yet. Will post the link here once published. FWIW, I uploaded my slides here in the meantime https://pcaversaccio.com/assets/Vyper_Day_Snekmate_Presentation.pdf.

[pcaversaccio]

My talk can be found here. Unfortunately, the sound could be better, but hope you still like it.

[pcaversaccio]

Closing this discussion as I'm tracking the initiative now here: #184.

[pcaversaccio]

UPDATE: echidna-based property tests for the ERC20 and ERC721 contracts have been added via #239.