Summary
Docs mention the redistribution mechanism as:
When ETH value as collateral drops precipitously and the TAPP has low amounts of zETH, all orderbooks have the same mechanism in place to save the asset peg by always allowing execution of margin calls. Instead of freezing the market upon the first instance of an under-collateralized shortRecord, the unbacked asset debt is socialized over every shortRecord in proportion to each position's ercDebt balance. As long as the CR of the entire system is above 1, this allows market operations to continue indefinitely and undisturbed unless:
1. The DAO steps in and freezes/dissolves the market
2. The max ercDebtRate is reached (uint64 max ~18.45x)
ercDebtRate is calculated as ercDebt[socialized] / (ercDebt[Asset] - ercDebt[socialized]) and is written to every shortRecord record to modify each position's ercDebt amount. This functions in the same manner as yield rate, but affects the asset debt instead of zETH.
However due to division before multiplication, protocol could socialize less ercDebt than what actually needs to be socialized, and hence the protocol can face a loss.
Vulnerability Details
ercDebtRate is updated in the code here:
File: contracts/facets/MarginCallPrimaryFacet.sol
202 function _performForcedBid(
203 MTypes.MarginCallPrimary memory m,
204 uint16[] memory shortHintArray
205 ) private {
206 uint256 startGas = gasleft();
207 uint88 ercAmountLeft;
208
...
...
...
229 m.short.ercDebt = uint88(
230 m.ethDebt.div(_bidPrice.mul(1 ether + m.callerFeePct + m.tappFeePct))
231 );
232 uint96 ercDebtSocialized = ercDebtPrev - m.short.ercDebt;
233 @>
234 @> s.asset[m.asset].ercDebtRate +=
235 @> ercDebtSocialized.divU64(s.asset[m.asset].ercDebt - ercDebtPrev);
236 }
237
...
...
...
L234-L235 are of the form:
Now to update the ercDebt, updateErcDebt() is called which does the following on L290:
File: contracts/libraries/LibShortRecord.sol
283 function updateErcDebt(address asset, address shorter, uint8 shortId) internal {
284 AppStorage storage s = appStorage();
285
286 STypes.ShortRecord storage short = s.shortRecords[asset][shorter][shortId];
287
288
289 uint64 ercDebtRate = s.asset[asset].ercDebtRate;
290 @> uint88 ercDebt = short.ercDebt.mulU88(ercDebtRate - short.ercDebtRate);
291
292 if (ercDebt > 0) {
293 short.ercDebt += ercDebt;
294 short.ercDebtRate = ercDebtRate;
295 }
296 }
Which is equivalent to:
uint88 ercDebt = a * (x/y - b);
where `a` is 'short.ercDebt', `b` is 'short.ercDebtRate' and x/y is the 's.asset[asset].ercDebtRate' (also known as `ercDebtRate` from the previous function).
It should ideally be:
uint88 ercDebt = (a * (x - (b * y))) / y;
which is equivalent to:
uint88 ercDebt = (short.ercDebt.mulU88(ercDebtSocialized_Numerator - (short.ercDebtRate.mulU64(ercDebtSocialized_Denominator)))).divU64(ercDebtSocialized_Denominator);
Here, the following two values need to be propogated from MarginCallPrimaryFacet.sol#L235 so that they can be used in the formula above:
ercDebtSocialized_Numerator = ercDebtSocialized
ercDebtSocialized_Denominator = s.asset[m.asset].ercDebt - ercDebtPrev
Impact
If there are 1000 short records across which an unbacked-asset-debt needs to be socialized, such precision loss could result in the protocol socializing less ercDebt than expected to each one of them, and hence bear a loss at the end of it as some debt will still remain. (The socialized debts across 1000 shorts will not add up to be equal to the unbacked-asset-debt).
Tools Used
Manual inspection
Recommendations
As shown in the calculations above, store ercDebtSocialized_Numerator & ercDebtSocialized_Denominator in storage variables so that they can be used later for correct calculation.
