Security

Audit and formal verification

Between January 8 and April 30, a team of six engineers reviewed and formally validated the key components of the dnft smart contract. The work includes the development of smart contract and formal verification of multi mortgage Dai.

The scope of work includes:

Formal verification of core smart contract

Code review of core smart contract

Numerical error analysis

Code review of peripheral smart contract (under development)

The report also has a "design opinion" part, and we strongly recommend that we get an in-depth technical understanding of some people's choice in DNFT.

Problems to be considered when building on dnft

When dnft is integrated into another chain system, special attention must be paid to avoid security vulnerabilities, operational approaches and potential financial losses.

As a preliminary note: Smart contract integration can be performed at two levels: directly using a pair of contracts, or through a router. Direct interaction provides the most flexibility, but requires the most work to get it right. Mediated interactions provide more limited capabilities, but stronger security guarantees.

There are two main categories of risk with DNFT. The first involves so-called "static" errors. These may include sending too many tokens (or requesting too few tokens) during the exchange, or allowing the transaction to stay in the memory pool long enough so that the sender’s price expectations are no longer accurate.

These errors can be resolved by fairly simple logical checks. Performing these logical checks is the main purpose of the router. People who interact directly with the pair must perform these checks themselves (in the library).

The second category is "dynamic" risk, which involves runtime pricing. Because Ethereum transactions take place in an adversarial environment, smart contracts written naively can and will be used for profit. For example, suppose a smart contract checks the ratio of assets in the DNFT pool and trades with it at runtime. Assume that the ratio represents the "fair" or "market" price of these assets. In this case, it is very susceptible to manipulation. A malicious actor can, for example, trivially insert naive transactions before and after the transaction (so-called "sandwich" attacks), resulting in smart contract transactions at a very bad price, profiting from the dealer’s fees, and then Return the contract to their original state, all at low cost. (An important caveat is that these types of attacks can be mitigated by trading in high-liquidity pools or trading in low-value.)

The best way to prevent these attacks is to introduce price predictors. Oracle is any device that returns the required information, in this case, the spot price of a pair. The best "oracle" is simply an off-chain observation of the current price by the trader, which can be passed into the transaction as a security check. This strategy is most suitable for retail trading venues, where users initiate transactions in their own name. However, in general, a credible price observation is not available (for example, in a multi-step, programmatic interaction involving DNFT). Without price oracles, these interactions would be forced to trade on DNFT at any (potentially manipulated) interest rate.