This exercise requires completing exercise 1 and exercise 2.
Table of contents:
Join the team on Slack at: https://slack.empirehacking.nyc/ #ethereum
We will test the following contract token.sol:
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;
}
}
Consider the following extension of the token (mintable.sol):
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;
}
}
The version of token.sol contains the fixes from the previous exercises.
- Create a scenario where
echidna (tx.origin)
becomes the owner of the contract at construction, andtotalMintable
is set to 10,000. Remember that Echidna needs a constructor without arguments. - Add a property to check if
echidna
can mint more than 10,000 tokens. - Once Echidna finds the bug, fix the issue, and re-try your property with Echidna.
The skeleton for this exercise is template.sol:
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
}
}
This solution can be found in solution.sol.