เฉลย echidna exercise 3

โอเค มาลุยกัน

มาเริ่มจาก code ที่ต้อง test กันก่อน

// SPDX-License-Identifier: AGPL-3.0
pragma solidity ^0.8.0;

import "./token.sol";

contract MintableToken is Token {
    int256 public totalMinted;
    int256 public totalMintable;

    constructor(int256 totalMintable_) {
        totalMintable = totalMintable_;
    }

    function mint(uint256 value) public onlyOwner {
        require(int256(value) + totalMinted < totalMintable);
        totalMinted += int256(value);

        balances[msg.sender] += value;
    }
}

โอเค เป็น token ที่ mint ได้ และมี cap การ mint

// SPDX-License-Identifier: AGPL-3.0
pragma solidity ^0.8.0;

/// @notice The issues from exercise 1 and 2 are fixed.

contract Ownable {
    address public owner = msg.sender;

    modifier onlyOwner() {
        require(msg.sender == owner, "Ownable: Caller is not the owner.");
        _;
    }
}

contract Pausable is Ownable {
    bool private _paused;

    function paused() public view returns (bool) {
        return _paused;
    }

    function pause() public onlyOwner {
        _paused = true;
    }

    function resume() public onlyOwner {
        _paused = false;
    }

    modifier whenNotPaused() {
        require(!_paused, "Pausable: Contract is paused.");
        _;
    }
}

contract Token is Ownable, Pausable {
    mapping(address => uint256) public balances;

    function transfer(address to, uint256 value) public whenNotPaused {
        balances[msg.sender] -= value;
        balances[to] += value;
    }
}

นอกจากนั้นยังมี owner ได้ transfer ได้ และ pause ได้

โดยเค้าจะให้ template การ test มาเป็น

// SPDX-License-Identifier: AGPL-3.0
pragma solidity ^0.8.0;

import "./mintable.sol";

/// @dev Run the template with
///      ```
///      solc-select use 0.8.0
///      echidna program-analysis/echidna/exercises/exercise3/template.sol --contract TestToken
///      ```
contract TestToken is MintableToken {
    address echidna = msg.sender;

    // TODO: update the constructor
    constructor(int256 totalMintable) MintableToken(totalMintable) {}

    function echidna_test_balance() public view returns (bool) {
        // TODO: add the property
    }
}

เอาละ เค้าบอกใบ้มาว่าให้ test ค่า balance

งั้นมาเริ่มกันจาก property (invariant)

balance ของ account ใดๆต้องไม่เกิน cap mint

จะได้เป็น

function echidna_test_balance() public view returns (bool) {
    return balances[msg.sender] <= uint256(totalMintable) && totalMintable > 0;
}

โดยเนื่องจาก type ของ totalMintable เป็นคนละ type กับ balances จึงต้อง cast type

และ totalMintable ไม่ควรน้อยกว่า 0 จึงกำหนดเป็น invariant

โอเคมาลองรันกัน

เราจะเจอ error ที่ constructor ไม่มีค่าเข้าไป

echidna: Constructor arguments are required: [("totalMintable",int256)]

โดยแก้ได้โดยการใช้ etheno ช่วยไม่ก็เอา param ออกจาก constructor

เราเลือกอย่างหลังละกัน

จะได้เป็น

// SPDX-License-Identifier: AGPL-3.0
pragma solidity ^0.8.0;

import "./mintable.sol";

/// @dev Run the template with
///      ```
///      solc-select use 0.8.0
///      echidna program-analysis/echidna/exercises/exercise3/template.sol --contract TestToken
///      ```
contract TestToken is MintableToken {
    address echidna = msg.sender;

    // TODO: update the constructor
    constructor() MintableToken(100) {}

    function echidna_test_balance() public view returns (bool) {
        return balances[msg.sender] <= uint256(totalMintable) && totalMintable > 0;
    }
}

จะได้ผลลัพธ์คือ invariant not hold

เราจะได้ว่า step to reproduce คือ

1. ทำการ mint ด้วยค่าที่สูงมากๆ

โดยเมื่อค่านี้ cast ไปเป็น int256 จะทำให้ค่าติดลบ ทำให้ผ่าน

function mint(uint256 value) public onlyOwner {
require(int256(value) + totalMinted < totalMintable);

มาได้ เนื่องจาก -5 + 0 < 100

จากนั้นเมื่อ balances เพิ่มขึ้น ตัวค่านี้จะทำให้ balance เกิน 100 ไปนั่นเอง

balances[msg.sender] += value;

2. การโอนน่าจะไม่จำเป็นละ แต่ตัว fuzzer ก็เพิ่มมาให้ละนะ

โอเค ประมาณนี้

Referrence

building-secure-contracts/program-analysis/echidna/exercises at master ·…