Stream contract formal verification with certora

Summary

Formal verification of Stream contract with certora

Vulnerability Detail

N/A

Impact

Formal verification can significantly increase security of the protocol. Execution of all rules can done with certora:

bash certora/scripts/verifyStream.sh

Code Snippet

Certora specification for Stream contract: https://github.com/sherlock-audit/2022-11-nounsdao/blob/main/certora/specs/Stream.spec#L1-L221

1.SanityCheck ✓

rule sanityCheck() {
    ...
}

2. Recipient balance should never exceed remaining balance ✓

{ remainingBalance >= recipientBalance }
op;
{ remainingBalance >= recipientBalance }

3. Solvency - Token balance should be bigger or equal to remainingBalance ✓

{ remainingBalance <= token.balanceOf(contract) }
op;
{ remainingBalance <= token.balanceOf(contract) }

4. Recipient balance is correctly vested over time ✓

getRecipientBalance() => elapsed * tokenAmount() / duration;

5. Integrity of withdraw ✓

{ recipientBalanceBefore = USDC.balanceOf(recipient())
  contractBalanceBefore = USDC.balanceOf(currentContract)
  remainingBalanceBefore = remainingBalance }
withdraw(amount)
{ recipientBalanceBefore == USDC.balanceOf(recipient() + amount)
  contractBalanceBefore  USDC.balanceOf(currentContract) - amount
  remainingBalanceBefore = remainingBalance - amount}

6. Withdraw all remainingBalance when stopTime passed ✓

{ timestamp > stopTime && remainingBalanceBefore = remainingBalance }
withdraw(remainingBalance)
{ remainingBalance = 0 }

7. Integrity of cancel ✓

cancel()
{ remainingBalance == 0 && token.balanceOf(contract) == 0 }

8. Integrity of rescueERC20 ✓

{ remainingBalanceBefore = remainingBalance && balanceBefore = token.balanceOf(contract) }
rescueERC20()
{ remainingBalanceBefore == remainingBalance && balanceBefore == token.balanceOf(contract) }

9. Integrity of ratePerSecond ✓

ratePerSecond()
{ !REVERTS }

10. Integrity of balanceOf ✓

balanceOf()
{ !REVERTS }

11. Withdraw should revert after cancel was called ✓

cancel(e)
{ withdraw(e) => REVERTED }

Tool used

Certora

Recommendation

It is recommended to use formal verification of the protocol.

sherlock-audit / 2022-11-nounsdao-judging

reassor - Stream contract formal verification with certora #69