Invariant Checks Gone Wrong

When I first learned about @brockjelmore's FREI-PI pattern, it broke my brain.

Throughout the time spent verifying the solidity code's correctness by hand and with tests, I never really thought that I was allowed to add more code that contributed nothing to functionality. Input verification was a must as we had no control over user input, but beyond that, adding more verifications never really crossed my mind. After all, that's what tests were for.

Once familiar with FREI-PI¹, I incorporated it everywhere possible. A core invariant check was applied to every externally available function. During audits, the invariant check seemed to prevent most edge cases that would typically result in critical or high vulnerabilities.

However, during this process, I discovered unfortunate side effects of invariant checks. They could result in the protocol being bricked, accidentally or intentionally, due to its failure to pass the invariant check. In other words, it actually introduced security vulnerabilities, while trying to prevent them.

The Impact

Following are examples from the amkt-v2 internal audit:

1. Broken invariant check due to fmul precision loss (opens in a new tab)

Functions in FixedPoint.sol such as fmul will always round down according to the scalar, leading to precision loss. The problem occurs due to the fact that invariantCheck and issue expect the user to bring the exact same units, without accounting for this precision loss. Because of this, what was collateralized at at issuance time t=0 may no longer be collateralized by t=1, depending on how much precision was lost at t=0.

The problem was observed while fuzzing random jitters in between issuance, and was most prominent in assets with lower number of decimals, as they are most heavily impacted by the precision loss.

This PR includes two proposed improvements:

1. Add 1 to realUnit when calculating underlyingAmount for issue. This ensures that even with any precision loss, the resulting amount is guaranteed to be greater than what invariantCheck might expect at t=0. It's important to note that this addition may not be the theoretical minimum required of the protocol upon issuance. However, it is extremely simple in complexity and solves the problem at hand effectively.
2. Add 1 to amountIncludingIntradayInflation when calculating underlyingAmount for issue. This is not necessary to address the issue and may not be required in any future scenarios. However, we should prefer to round up in favor of the protocol whenever there's possibility of precision loss.

2. fmul rounding in Bounty quote leading to broken invariant check (opens in a new tab)

Similar to #1 (opens in a new tab), fulfilling a bounty can run into an invariant check revert under certain circumstances, due to the fact Bounty uses a diff of the units * supply to calculate ins/outs, whereas the invariant check uses units * supply to calculate invariant. This means there could be a rounding down that exists in bounty quote that doesn't exist in invariant, and vice versa.

In #1 (opens in a new tab), the difference in token supply causes the mismatch. This time, the difference in units causes the mismatch.

Both share the same root cause, which is precision loss while performing fixed point math. Precision is crucial in invariant checks, as even a minimal difference could cause a failure. Extensive fuzzing identified these issues, which we promptly addressed by requiring users to slightly round up their collateral, yet these were issues even world-class auditors overlooked.

Under specific circumstances, these issues could have bricked functionalities, leading to negligible consequences or potential exploitation by adversaries.

However, those vulnerabilities did not compare to the possible vulnerabilities that could have been introduced without the enforcement of invariant checks. Precision loss favoring the user becomes a common attack vector for critical vulnerabilities. At the very least, our invariant checks ensured the protocol's full collateralization at all times.

For the most part, FREI-PI is an incredibly effective pattern to adopt, as it likely reduces the severity of potential critical vulnerabilities. Just make sure your invariants are actually invariants!