Thoughts on better invariants

invariant_thoughts.md

"Instant DSR" Pot attack

This is a tough one. In general, it's always theoretically possible to get a "free lunch" off the DSR. E.g. if Jug.drip is not being called very frequently, it's trivial. It usually depends, however, on the behavior of the other market participants. The reason this bug was a big deal was that it was exploitable regardless of the behavior of others. So we need an invariant that doesn't just detect a "free lunch", but one that detects an easily-obtainable "free lunch". Ideally, one shouldn't have to specify in too much detail the behavior of other participants for detection. The current property just checks that Pot.join is not called in a block without Pot.drip being called first. A slightly more sophisticated check would be as follows:

"If, during a block, Vat.dai[address(Pot)] increases, it should not increase by more than the amount one would get if Pot.drip were called immediately at the start of the block, once Pot.join and Pot.exit calls are adjusted for."

This would at least not rely on looking for specific sequences of function calls. It essentially expresses the idea that any new dai joined into the Pot must "wait its turn" before accruing interest. It's still rather narrow, and doesn't totally get at the core of the problem (risk-free dai earning).

End+Pot attack

Currently, we detect this by seeing if Pot.file("dsr", _) is called after End.cage() is called. A somewhat improved check would be: "Does Pot.chi change after End.cage() is called?" This is a little more general, as it gets closer to the heart of the matter: dai in the Pot should no longer earn interest after ES is triggered.

Flip+End attack

It's very tricky to detect this at the level of the flip auction itself. Basically, you need to know some history because

1. the system itself doesn't keep records (e.g. past bids on auctions)
2. the accounting values one might look at (e.g. Vat.dai[address(Vow)], the surplus) are affected by many different things I don't have a proof that it's impossible to detect bad flip auctions purely from accounting values, but... I spent enough time thinking about it that I decided it would be more fruitful to move on to other things. As far as detecting the exploit against the End, it's hard to do that w/o false positives. The recently added "Debt Constant After Thaw" will detect this, albeit with potential false positives. Arguably, there's really a flaw in the End here: thawing should completely disable anything that creates/destroys dai. (Including End.skip().) Of course, even with that change, the bug could still be exploited before thaw is called, just slightly less effectively. Need to think more about this.

Flap+End attack

After talking about it in the call, the nice behavior of Flap (holding on to both dai and MKR until deal is called for each auction) allows some invariants to be described (see comments below).

In terms of how KMCD is presented, we came up with the following properties which are likely true over the given Trace Generator:

AddGenerator ( ( ( GenFlapKick
                 | GenFlapTick
                 | GenFlapTend
                 | GenFlapDeal
                 ) *
               )
             ; GenEndCage
             ; ( ( GenFlapTick
                 | GenFlapYank
                 ) *
               )
             )

Properties:

vat.dai(Flap) - sumOfAllLots >= 0
Gem.MKR(Flap) - sumOfAllBids >= 0

// If Flap.deal event adjusts `constant` appropriately:
sum(Gem.MKR.balances without Flap) + sumOfAllBids == constant // (deals are handled accordingly)

sum(Gem.MKR.balances without Flap) + sumOfAllBids <= Gem.MKR.totalSupply

this might also be a corresponding property for dai and lots:

sum(Vat.dai.balances without Flap) + sumOfAllLots <= Vat.debt