Happy to contribute! Appreciate the OpenZeppelin team's commitment and efforts to raise the security bar!
Hope to see more ERC4626 vaults adopting these property tests! Please let me know if anyone needs help with that!
Follow
Daejun Park
@daejunpark
web3 security + formal methods ; prev director of formal verification ; phd ; views == mine
daejunpark.github.ioJoined August 2009
Daejun Park’s Tweets
***
As a reminder, none of the above is investment, business, legal, or tax advice. Please see a16z.com/disclosures for more important information, including a link to a list of our investments.
4
Show this thread
The property tests (with documentation and examples) are publicly available in our Github repository. We welcome your feedback and contributions!
github.com/a16z/erc4626-t
Read more in our post:
1
6
Show this thread
3. If your vault has to diverge from the standard, we recommend clearly documenting the non-standard behaviors, so that others can properly handle these deviations when integrating with your vault. Please note that this should be considered as a last resort.
2
7
Show this thread
2. We also suggest reviewing our properties to cross check your understanding of the standard requirements, and adjust your implementation if there is any unintentional discrepancy.
1
10
Show this thread
We hope our properties help, along with action items for those who are developing/integrating ERC4626 vaults:
1. We recommend running our property tests against your vaults. They will quickly find issues if there are any clear violations of the standard.
1
10
Show this thread
These properties can be executed by providing specific input values (for unit testing), many random inputs (for fuzz testing), or symbolic values (for symbolic execution and formal verification). It can also be run locally or against a mainnet fork (for integration testing).
1
7
Show this thread
To help detect standard violations that may break integrations or lead to vulnerabilities down the road, we’ve written ERC4626 standard properties.
Specifically, we wrote them in the form of property-based tests (in Foundry) to make the properties executable (and thus testable).
1
9
Show this thread
Although these discrepancies were not exploitable per se, they may become vulnerable when integrated to other systems that expect only the standard behaviors. This will make vault integration much harder, potentially neutralizing the efforts and motivation behind standardization.
1
7
Show this thread
Some emitted an inconsistent Deposit event that is different from what was actually minted.
To our surprise, some vaults never minted on the spot at all; instead, they just put the mint requests into a queue, and process them later in a batch as a separate transaction.
1
7
Show this thread
Unfortunately, we found several ERC4626 vaults on the mainnet which don’t conform to the standard.
For example, some vaults failed to mint the exact number of shares requested by the mint() function, although the standard explicitly requires this:
eips.ethereum.org/EIPS/eip-4626#
1
2
6
Show this thread
We believe ERC4626 vaults will become an important building block for DeFi, and it is desired that vaults follow the standard. (You may recall past issues caused by non-standard ERC20 tokens, e.g, Tether USD’s missing-return problem.)
1
10
Show this thread
We released ERC4626 standard property tests to help vault builders catch discrepancies in subtle, easy-to-miss details of the standard requirements.
Code: github.com/a16z/erc4626-t
Post: a16zcrypto.com/generalized-pr
What is it, why does it matter, & some actionable insights: 👇🧵
17
67
209
Show this thread
Check out this brand-new Z3 online guide (built by and his interns this summer!) if you want to learn what's running under the hood of web3 formal verification tools,
6
13
51
In formal methods:
- safety property: "nothing bad happens"
- liveness property: "something good eventually happens"
In web3:
- safety property: "funds never stolen"
- liveness property: "funds never locked"
4
6
4/ And, if such assumptions were made explicit, and a storage monitor was deployed to check if the assumptions still hold whenever the contract state is updated, the mistake would have been caught when it was made 41 days ago:
1
2
Show this thread
4/ And, if such assumptions were made explicit, and a storage monitor was deployed to check if the assumptions still hold whenever the contract state is updated, the mistake would have been caught when it was made 41 days ago:
1
Show this thread
3/ So, when the contract was developed or audited, the devs or auditors would have to assume that `confirmAt[0x0] == 0` must always hold, which I think is a reasonable assumption on operating the contract (otherwise, the message validation logic would be broken.)
1
3
Show this thread
2/ First, note that the contract code is not necessarily buggy and it wasn’t the auditor’s fault either, but it was due to a mistake made in a routine upgrade:
Quote Tweet
12/ tl;dr a routine upgrade marked the zero hash as a valid root, which had the effect of allowing messages to be spoofed on Nomad. Attackers abused this to copy/paste transactions and quickly drained the bridge in a frenzied free-for-all
Show this thread
1
2
Show this thread
1/ The Nomad incident reminded me of “storage monitoring,” which I have been thinking about. 🧵
👇
Quote Tweet
1/ Nomad’s bridge got owned in a similar manner to Qubit’s QBridge. An insecure configuration of the bridge caused a specific path to allow any transaction sent. The error is inside the Replica’s “process” function.
Show this thread
1
5
17
Show this thread