Versions Compared

Key

  • This line was added.
  • This line was removed.
  • Formatting was changed.

...

List of Main Issues Discovered

Severity: Critical

Issue:

Significant loss of system assets

Description:

In the case of withdrawal between rounds, one can withdraw the same liquidity certificate for unlimited number of times, thus draining the system. Furthermore, that liquidity certificate does not have to be under our ownership - anybody can withdraw a certificate even if they do not own it.

Mitigation:

At the end of the withdrawal between rounds process, the The used liquidity certificate is now being burned, and the sender’s ownership of that liquidity certificate is being verified.

Severity: High

Issue:

Denial of service of the system

Rule:

Burnable tokens must not exceed total supply

Description:

A user can mark multiple times his liquidity certificate for withdrawal, causing wrong interpretation of assets to free. This can cause the round end process to revert, leaving the system in a denial of service state.

Mitigation:

signalWithdrawal() now reverts when it is given a liquidity certificate that has already signaled exit.

Severity: Low

Issue:

Unsafe casts from uint to int

Description:

The functions openPosition() and closePosition() perform unsafe casts of amount from uint to int. An overflow can lead to unexpected behavior, including wrong changes to the contract internal state.

Mitigation:

The requirement int(amount) > 0 was added to _canDoTrade().

Severity: Low

Issue:

Wrong revert reason

Description:

In liquidateExpiredBoard(), the for loop that removes the board from the list of live boards is for (uint i = liveBoards.length - 1; i >= 0; i--) and since i is of type uint, the condition i >= 0 will always pass. Then if the board is not in the list of live boards, the i-- operation after the last loop iteration will cause a revert due to underflow, instead of reverting in the later require(popped) statement.

A similar issue occurs when the system is between rounds. In this case, there will also be a revert due to underflow, this time in the loop initialization line uint i = liveBoards.length - 1, because the list of live boards would be empty.

Mitigation:

The for loop was modified to for (uint i = 0; i < liveBoards.length; i++).

Severity: Low

Issue:

Ignoring return value from Synthetix.exchange

Description:

Does not handle the case when the call fails

Mitigation:

Fixed

Severity: Recommendation

Issue:

“Buying” options for zero cost

Description:

Due to additional fees the system may evaluate certain options to Zero value, and is willing to buy those options for Zero cost. We recommend refraining from Zero cost trades.

...

    1. ✔️ indicatesthe rule is formally verified on the latest commit.

    2. We write ✔️* when the rule was verified on a simplified version of the code (or under some assumptions). 

    3. ✔️x indicates that the rule was violated at some version of the code.

  1. (blue star) indicates the rule was violated under the current tested version of the code.

  2. ✍ indicates the rule is not yet formally specified.

  3. 🔁 indicates the rule is postponed (<due to other issue, low priority?>) .

  4. We use Hoare triples of the form {p} C {q}, which means that if the execution of program C starts in any state satisfying p, it will end in a state satisfying q. In Solidity, p is similar to require, and q is similar to assert. 

The syntax {p} (C1 ~ C2) {q} is a generalization of Hoare rules, called relational properties. {p} is a requirement on the states before C1 and C2, and {q} describes the states after their executions. Notice that C1 and C2 result in different states. As a special case, C1~op C2, where op is a getter, indicating that C1 and Cresult in states with the same value for op.

...

  1. Tokens to burns at end of round cannot be more than the total supply ✔️x

    Anchor
    tokensBurnableVsTotalSupply
    tokensBurnableVsTotalSupply

    The total amount of tokens signal to withdraw is less than the total tokens supplied.

    Code Block
    tokensBurnableForRound() ≤ totalTokenSupply() 

  2. Change to only one certificateID ✔️
    Each operation changes at most one certification.

    Code Block
    { certificateId1  certificateId2 ∧ 
      cId1Before = getCertificateIdLiquidity(certificateId1) ∧
      cId2Before = getCertificateIdLiquidity(certificateId2) } 
      op  
    { ¬ (cId1Before ≠ getCertificateIdLiquidity(certificateId1) ∧
      cId2Before ≠ getCertificateIdLiquidity(certificateId2) )
    }  

  3. Either withdraw or signal withdraw, can’t do both ✔️
    At any given state, a certification id can be either signaled to withdraw or withdrew, not both.

    Code Block
    { block.timestamp > 0 }
        r1 = signalWithdrawal(certificateId) ~  r2 = withdraw(b,certificateId)
    { !(r1 ∧ r2) }

  4. Validity of rounds

    1. Creating a board results in a valid board id ✔️

      Code Block
      { }
          boardId = createOptionBoard(e, args)  
      { boardIdExists(boardId) } 

    2. Opening a new round results in non zero live boards ✔️

      Code Block
      { getLiveBoardsLength() = 0 } 
          createOptionBoard(e, args);
      { getLiveBoardsLength() > 0 }

    3. While in a round all boards created are to be closed by the end of the round ✔️

      Code Block
      { }
        boardId = createOptionBoard(e, args) ⇒
      { getOptionBoardExpiry(boardId) ≤ getMaxExpiryTimestamp() }

    4. The system can reach the in-between rounds state ✔️

      Code Block
      { getLiveBoardsLength() = 1 }     
        liquidateExpiredBoard(e, boardId);      
      { getLiveBoardsLength() = 0 }

    5. Integrity of the end of a round ✔️

      Code Block
      getLiveBoardsLength() = 0 ⇒ getBlockTimestamp(e) > getMaxExpiryTimestamp()

  5. Validity of Live boards

    1. Integrity of live boards representation ✔️

      Code Block
      ( index < getLiveBoardsLength()  ∧   boardId = getLiveBoard(index) ) ⇒
              ( getOptionBoardId(boardId) == boardId ∧ 
              getOptionBoardExpiry(boardId) > 0 ) 

    2. Uniqueness of board id ✔️

      Code Block
      getLiveBoard(i) = getLiveBoard(j) ⇒ i = j

    3. No empty boards ✔️

      Code Block
      getLiveBoardsLength() > i ⇒ getListingLength(i) > 0

  6. Validity of listing ✔️

    Code Block
    getOptionBoardListingId(boardId, i) = listingId ⇒ 
            getOptionListingBoardId(listingId) = boardId

  7. Can’t open position with listing id who's board was liquidated 🔁

  8. Once opening a position, one can close the position 🔁

  9. One can not open an opposite position to an existing one 🔁

  10. Validity of pricing

    1. Increase in implied volatility necessarily increase the option price 🔁

    2. Decrease in time to expiration necessarily decrease the option price 🔁

...