Exercise 2

This exercise requires completing exercise 1.

Table of contents:

• Exercise 2
  • Targeted contract
  • Testing access control
    • Goals
  • Solution

Join the team on Slack at: https://slack.empirehacking.nyc/ #ethereum

Targeted contract

We will test the following contract, token.sol:

pragma solidity ^0.8.0;

contract Ownable {
    address public owner = msg.sender;

    function Owner() public {
        owner = msg.sender;
    }

    modifier onlyOwner() {
        require(owner == msg.sender);
        _;
    }
}

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;
    }
}

Testing access control

Goals

• Assume pause() is called at deployment, and the ownership is removed.
• Add a property to check that the contract cannot be unpaused.
• When Echidna finds the bug, fix the issue and retry your property with Echidna.

The skeleton for this exercise is (template.sol):

pragma solidity ^0.8.0;

import "./token.sol";

/// @dev Run the template with
///      ```
///      solc-select use 0.8.0
///      echidna program-analysis/echidna/exercises/exercise2/template.sol
///      ```
contract TestToken is Token {
    constructor() {
        pause(); // pause the contract
        owner = address(0); // lose ownership
    }

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

Solution

The solution can be found in solution.sol.