A minimal token

Minimal token code

Token code

MinimalToken.sol

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;

/// @title A minimal ERC-20 style token
contract MinimalToken {

    mapping(address => uint256) public balanceOf;
    mapping(address => mapping(address => uint256)) public allowances;
    uint256 public totalSupply;

    function transfer(address recipient, uint256 amount) public returns (bool) {
        _transfer(msg.sender, recipient, amount);
        return true;
    }

    function transferFrom(
        address sender,
        address recipient,
        uint256 amount
    ) public returns (bool) {
        uint256 currentAllowance = allowances[sender][msg.sender];
        require(currentAllowance >= amount, "Transfer exceeds allowance");

        _approve(sender, msg.sender, currentAllowance - amount);
        _transfer(sender, recipient, amount);

        return true;
    }

    function _transfer(
        address sender,
        address recipient,
        uint256 amount
    ) internal {
        require(recipient != address(0), "Transfer to zero address");

        uint256 senderBalance = balanceOf[sender];
        require(senderBalance >= amount, "Transfer exceeds balance");

        balanceOf[sender] = senderBalance - amount;
        balanceOf[recipient] += amount;
    }

    function approve(address spender, uint256 amount) public returns (bool) {
        _approve(msg.sender, spender, amount);
        return true;
    }

    function _approve(
        address owner,
        address spender,
        uint256 amount
    ) internal {
        allowances[owner][spender] = amount;
    }

    function deposit(uint256 amount) public payable {
        require(msg.value >= amount, "Insufficient eth");
        require(msg.sender != address(0), "Depositing to zero address");
        balanceOf[msg.sender] += amount;
        totalSupply += amount;
    }
}

---

Invariants

1. Property: Address zero has no balance.

   /// @title Adress zero has no balance
   invariant noBalanceAddressZero()
       balanceOf(0) == 0;
   

2. Property: Total supply is not greater than ETH balance (solvency).

   /// @title Total supply not greater than ETH balance
   invariant tokenSolvency()
       nativeBalances[currentContract] >= totalSupply();
   

Task 7: Fix the bug

• Run the invariants using the config MinimalToken.conf.

• The results will indicate a violation.

• Fix the problem and rerun.

• Results link: rule report.

Solution

• The violation of the invariant tokenSolvency occurs when the token deposits to itself, that is the token itself is the msg.sender.

• To prevent this behavior, we use a Solidity require statement, in MinimalTokenFixed.sol.

• Here is the report using the fixed code: solution report.

--- /home/docs/checkouts/readthedocs.org/user_builds/certora-presentations/checkouts/latest/basic/src/MinimalToken.sol
+++ /home/docs/checkouts/readthedocs.org/user_builds/certora-presentations/checkouts/latest/basic/src/MinimalTokenFixed.sol
@@ -57,6 +57,7 @@
     function deposit(uint256 amount) public payable {
         require(msg.value >= amount, "Insufficient eth");
         require(msg.sender != address(0), "Depositing to zero address");
+        require(msg.sender != address(this), "Depositing to self");
         balanceOf[msg.sender] += amount;
         totalSupply += amount;
     }