Questioning "shares roundtrip" properties

[aviggiano]

Hello,

I am implementing this test suite on a new ERC4626 project and am seeing some failing properties related to "shares roundtrip."

In particular, both test_RT_withdraw_deposit and test_RT_deposit_withdraw fail for an ERC4626 vault that holds shares in another ERC4626 vault. You can take a look at the code here.

I have added a concrete test scenario here.

Although this project has not been audited yet, which means the likelihood of it containing a real issue is higher than erc4626-tests containing an issue, I question if failing "share roundtrip" properties are a real problem.

In this particular case, it seems that due to how totalAssets is calculated (i.e., as convertToAssets(balanceOf) on the other vault we hold shares), you can indeed withdraw, then deposit and have more shares than what you started with.

However, if you later attempt to withdraw the new, larger amount of shares, you don't end up with more assets than what you started with. And I believe this is what matters. i.e., broken "assets roundtrip" (such as in test_RT_redeem_mint or test_RT_mint_redeem) means loss of funds, but broken "shares roundtrip" means a slippage that can happen when entering/exiting the vault (still not 100% clear to me though), which is not necessarily a vulnerability (?)

Thoughts?

[aviggiano]

After further investigation, I am confident that roundtrip properties relying on shares minted/burned are not generic for every ERC‑4626 vault and, when they fail, do not automatically constitute a security issue.

---

1 . The property under test

// s  = withdraw(a)
// s' = deposit(a)
// expect s' ≤ s
function prop_RT_withdraw_deposit(address caller, uint assets) public {
    vm.prank(caller); uint shares1 = vault_withdraw(assets, caller, caller);
    if (!_vaultMayBeEmpty) vm.assume(IERC20(_vault_).totalSupply() > 0);
    vm.prank(caller); uint shares2 = vault_deposit(assets, caller);
    assertApproxLeAbs(shares2, shares1, _delta_);
}

Intuitively, this property asserts:

Withdrawing a assets and depositing the same a assets should never give you more shares back than you just burned

---

2 . Why the property holds for vanilla OpenZeppelin vaults

Let

• $A$ = totalAssets()
• $S$ = totalSupply()
• $v = 10^{\texttt{decimalsOffset()}} \ge 1$ (it is 1 by default)
• $0< a \le A$ be the user's round‑trip amount.

OpenZeppelin implements

$$ \text{previewWithdraw}(a)=\left\lceil a\frac{S+v}{A+1}\right\rceil, \qquad \text{previewDeposit}(a)=\left\lfloor a\frac{S+v}{A+1}\right\rfloor. $$

---

2.1  Withdraw step

Let the ceiling rounding error be $\varepsilon_w\in[0,1)$:

$$ s = a \cdot r + \varepsilon_w $$

Where $r = \frac{S + v}{A + 1}$

After burning $s$ shares and transferring $a$ assets,

$$ S' = S - s,\qquad A' = A - a. $$

The new ratio is

$$ r' = \frac{S' + v}{A' + 1} = \frac{S - s + v}{A - a + 1} $$

Use $S+v = r(A+1)$:

$$ r' = r - \frac{\varepsilon_w}{A - a + 1} \le r $$

---

2.2  Deposit step

Now floor‑round with error $\varepsilon_d\in[0,1)$:

$$ s' = a \cdot r' - \varepsilon_d $$

Observe $r' \le r$
Combining the previous equations

$$ s' \le a \cdot r < a \cdot r + 1 \le s $$

so $s' \le s$ (strict whenever either rounding error is non‑zero).
That is exactly what the property asserts.

---

3 . Where the property breaks: wrapper vaults

In this scenario, the total assets held by the parent vault are the amount of shares from the child vault that can be converted to assets, which has a round down operation.

function totalAssets() public view override returns (uint256) {
    return childVault.convertToAssets(
        childVault.balanceOf(address(this))
    ); // <-- rounds DOWN
}

Because convertToAssets() floors, burning parent‑shares can reduce totalAssets() by more than simply $a$:

$$ A' = A - a + \Delta, \qquad \Delta < 0. $$

---

3.1  Ratio $r$ can go up

Re‑compute $r'$ with the perturbed denominator:

$$ r' = r \cdot \frac{A+1-a}{A+1-a+\Delta} - \frac{\varepsilon_w}{A+1-a+\Delta} $$

Because $\Delta&lt;0$ the fraction in front of $r$ exceeds 1, and the second term is bounded by $\tfrac1{A}$.

If $|\Delta|\ge 1$ we get $r' &gt; r$.

---

3.2  Minted shares exceed burned shares

With $r' &gt; r$ and using the previous equations:

$$ s' = a \cdot r' - \varepsilon_d > a \cdot r - \varepsilon_w - 1 \ge s - 1. $$

For inputs that pushes $s'$ above $s$, the test fails, yet no extra assets can be extracted: a future withdraw of the new $s'$ will still return $\le a$ assets.

---

4 . Why this is not a security issue

Failing the shares round‑trip does not let a user net more underlying assets. The effect is comparable to 'slippage" when wrapping another vault that uses rounding or fee logic.

---

5 . Suggested fix

• Replace the test with a more direct invariant that "user must not extract assets from the vault" with roundtrip operations, e.g.:

    function prop_RT_deposit_withdraw(address caller, uint assets) public {
        uint256 assetsBefore = vault_convertToAssets(IERC4626(_vault_).balanceOf(caller)) + IERC20(_underlying_).balanceOf(caller);
        if (!_vaultMayBeEmpty) vm.assume(IERC20(_vault_).totalSupply() > 0);
        vm.prank(caller); uint shares1 = vault_deposit(assets, caller);
        vm.prank(caller); uint shares2 = vault_withdraw(assets, caller, caller);
        uint256 assetsAfter = vault_convertToAssets(IERC4626(_vault_).balanceOf(caller)) + IERC20(_underlying_).balanceOf(caller);
        assertApproxLeAbs(assetsAfter, assetsBefore, _delta_);
    }

_{Note: roundtrip operations can lead to users extracting assets from the vault in cases where totalAssets rounds up, which is the case, for example, for Aave wrapper vaults. Due to WadRay math, the AToken balance of the vault can, depending on the liquidity index, round up or down, which may lead to 1 wei being extracted at each operation.}

[aviggiano]

Adding more context to illustrate how totalAssets decreased by more than the withdrawn amount due to rounding (using the same test case, now with more logs):

Logs:
  Bound result 11179
  setUpVault
                                   account         shares         assets
0x00000000000000000000000000000000000030b3    987_910_862    987_921_818
0x0000000000000000000000000000000000002367            587            587
0x0000000000000000000000000000000000001B08         13_632         13_632
0x0000000000000000000000000000000000002D7E          6_506          6_506

                                    SUM(_)    987_931_587    987_942_543
                                   total()    997_931_587    997_942_655

  Bound result 957625571
  withdraw
                                   account       shares       assets
0x00000000000000000000000000000000000030b3   30_295_911   30_296_246
0x0000000000000000000000000000000000002367          587          587
0x0000000000000000000000000000000000001B08       13_632       13_632
0x0000000000000000000000000000000000002D7E        6_506        6_506

                                    SUM(_)   30_316_636   30_316_971
                                   total()   40_316_636   40_317_083

  deposit
                                   account         shares         assets
0x00000000000000000000000000000000000030b3    987_910_864    987_921_817
0x0000000000000000000000000000000000002367            587            587
0x0000000000000000000000000000000000001B08         13_632         13_632
0x0000000000000000000000000000000000002D7E          6_506          6_506

                                    SUM(_)    987_931_589    987_942_542
                                   total()    997_931_589    997_942_654

1. During the wrapper vault initialization, the first user holds 987_910_862 shares, which correspond to 987_921_818 assets. At this point, totalAssets() returns 997_942_655.

2. When the user withdraws 957625571, they are left with 30_295_911 shares, representing 30_296_246 assets. After this withdrawal, totalAssets() returns 40_317_083. However, 997_942_655 - 957625571 == 40_317_084, meaning one asset is effectively lost due to rounding down in the totalAssets() computation.

3. When the user re-deposits 957625571, they receive 987_910_864 shares corresponding to 987_921_817 assets. At this point, totalAssets() returns 997_942_654, which is one less than the original value in step 1. Importantly, the shares and corresponding assets held by other users remain unchanged throughout the process.

[EFCCWEB3]

I've had a chance to review the 'shares roundtrip' properties discussion. My analysis confirms that issues with 'shares roundtrip' don't inherently constitute a security vulnerability if the underlying assets are not affected. My findings align with the perspective that these scenarios are more akin to slippage rather than a direct loss of funds.

I've also identified a separate critical vulnerability related to an inflation attack in a contract. This attack can lead to a significant loss of value for the first legitimate depositor. I've developed a proof of concept and a recommendation to mitigate this by ensuring initial shares are minted in the constructor.

[daejunpark]

@aviggiano Thanks for reporting this issue and providing a detailed analysis. I really appreciate it, everything makes sense!

I'm still thinking it over, but in the meantime, let me ask a few questions and bring up some additional discussion points:

We have the parameter __delta__ to handle some rounding errors in opposite directions. (Currently, delta must be an absolute value rather than a relative one.) I’m wondering if this value could be used to help mitigate the issue.

The suggested fix seems effective for covering this scenario. But I'm curious whether, in vaults with more complex accounting logic, some additional rounding errors during conversion to the asset might still break the new property. Any thoughts?

[daejunpark]

We have the parameter delta to handle some rounding errors in opposite directions. (Currently, delta must be an absolute value rather than a relative one.) I’m wondering if this value could be used to help mitigate the issue.

I modeled this in SMT, and __delta__ doesn't seem to work with either absolute or relative values. Let me know if you have a different idea.

[aviggiano]

@daejunpark Sorry for the late reply. These things are tricky to get your head around.

We have the parameter delta to handle some rounding errors in opposite directions. (Currently, delta must be an absolute value rather than a relative one.) I’m wondering if this value could be used to help mitigate the issue.

I don't think it is very good to use __delta__ different from 0 in general since in most cases it will just hide a vulnerability. Many vault hacks are caused by off-by-one errors, so the slightest misunderstood non-null amount can already mean a big issue, as these are usually amplified by repeated minting/burning or with flash loans. For example, if I set __delta__ to 1 and if a "assets roundtrip" breaks instead of a "shares roundtrip," then it will literally result in stealing of funds, and in some cases (not always) can lead to draining the whole vault.

The suggested fix seems effective for covering this scenario. But I'm curious whether, in vaults with more complex accounting logic, some additional rounding errors during conversion to the asset might still break the new property. Any thoughts?

Actually, I was able to find a real bug with the updated property, which was the case of a wrapper vault from Aave v3. Because of the WadRay math, where the rounding is not consistent, if the totalAssets calculation uses aToken.balanceOf, in some cases we can have $\Delta &gt; 0$ in the equation $A' = A - a + \Delta$, which means users can indeed gain assets from the vault with roundtrip operations. However, from my preliminary investigation, I believe this cannot be exploited by repeating the roundtrip, as the excess assets are not taken from the vault itself, but from the AToken balance which in some cases would give +1 up or +1 down, so when the user repeats this, it is similar to trying to extract 1 wei from Aave with a supply followed by a withdraw, which I believe can only be done once. So instead of just accepting a __delta__ of 1 here, I chose to use aToken.scaledBalanceOf in calculating the totalAssets and always round down. This breaks the old prop_RT_deposit_withdraw but not the revised/suggested one.

[daejunpark]

@aviggiano thanks again for sharing the details! i've opened pr #15 based on your suggestion. it adds the asset balance check to all roundtrip properties, and introduces a flag to optionally disable the shares comparison. i kept the shares comparison as optional (rather than removing it), because some vaults may prefer stricter behavior around share rounding errors. let me know if you have any feedback!