search

ArdanaLabs / audit

0 stars 0 forks source link

["pile"] No Money For Nothing (NMFN) #5

Closed quinn-dougherty closed 2 years ago

quinn-dougherty commented 2 years ago

Description

NMFN is an intuitively desirable, if a little obvious, property. We do not want people to be able to arbitrarily withdraw assets.

Deliverable

There are a few ways to approach this

  1. Enumerating people who think they're clever but ultimately get blocked
  2. Informally state and prove a NMFN theorem (perhaps a warmup for formally doing it later)
  3. Assume NMFN property of stableswap and prove that the delta between DanaSwap and Stableswap preserves the property
    • Model dex as a game; correlate different sequences of play with eachother, see if that implies the payoffs correlate. See bisimulation

Notes

An approach to the predicate: show that any transaction does not decrease the liquidity token value of the dex. Finite enumeration of the ways the value of the dex could be decreased.

quinn-dougherty commented 2 years ago

NMFN is really a family of properties.

infinite minting

no validation in minting policy leads to someone outside of the schema minting tokens without validation.

Cardano does not guarantee against this.

Benjmhart commented 2 years ago

specifically infinite mint could be relevant for LP tokens.

additionally, we might consider any trade that results in one-sided extraction (or disproportionate extraction) to violate NMFN properties.

finally the LP providers themselves might be able to gain disproportionate benefit relative to the volume of their Liquidity provided to the protocol and the activity on a given trading pair, this would constitute a NMFN violation as well.

quinn-dougherty commented 2 years ago

The extent to which this is covered in audit is a comment about future work in src/postamble/fv.md

In the future, we may reopen this issue and put it on the cross-repo fv board