In Echidna Exercise 5 with echidna-test version 2.0.2 no bug found

Analyzing contract: /damn-vulnerable-defi/contracts/unstoppable/UnstoppableEchidna.sol:UnstoppableEchidna
echidna_testFlashLoan:  passed! 🎉

Unique instructions: 3001
Unique codehashes: 4
Corpus size: 14
Seed: -5156005997475524194

But according to assignment should be something like this

echidna_testFlashLoan: failed!💥  
  Call sequence:
    transfer(0x62d69f6867a0a084c6d313943dc22023bc263691,1296000)

The proposed solution fails to work when there is a modifier shadowing (which solidity does not report). To avoid this, could be a good idea to use canonical_name of the modifier ('Owned.onlyOwner()'), instead of the full_name.

Once crytic/echidna#344 is merged, we need to add an example showing how it works

On a high-level, there are two approaches to write properties:

• Targeted: I want to test a specific behavior of a function and want my analyzer to focus only one a particular piece of code
• General: I want X to be always true, no matters the target's context

We need a section that discusses this and highlights the difference with examples.

The proposed solution fails to work when the exercise is made a little harder, using the following contract:

contract Coin{

    address owner = msg.sender;

    mapping(address => uint) balances;


    // _mint must not be overriden
    function _mint(address dst, uint val) internal{
        require(msg.sender == owner);
        balances[dst] += val;
    }

    function mint(address dst, uint val) public{
        _mint(dst, val);
    }

}

contract MyCoin is Coin{

    event Mint(address, uint);

    function _mint(address dst, uint val) internal{
        balances[dst] += val;
        emit Mint(dst, val);
    }

}

contract MyCoin2 is MyCoin{

    function set(address dst, uint val) internal{
        balances[dst] = val;
    }
    
}

contract MyCoin3 is Coin{

    function set(address dst, uint val) internal{
        balances[dst] = val;
    }
}

contract MyCoin4 {
   
    function _mint(address dst, int val) public{}

}

contract NotCoin {
    address notowner;
    function _mint(address dst, uint val) internal{}


}

Running the solution results in this output:

$ python3 solution.py 
Error, MyCoin overrides _mint
Error, MyCoin2 overrides _mint
Error, MyCoin3 overrides _mint

However, MyCoin3 should not be detected as overriding the _mint function.

https://crytic.io/ supports now Echidna, we need a walkthrough example on how it works.

We can convert our blogpost to a checklist: https://blog.trailofbits.com/2018/04/06/how-to-prepare-for-a-security-audit/

And we can add a couple of blockchain-specific points

Echidna is having a lot of options and features, and it's difficult to remember where to find everything in the doc. We could have a small summary of the most common question somewhere (building-secure-contract, or Echidna readme]

On the top of my head, the frequent questions can be answered with:

What else?

Related

• #74
• #79

I am referring to this tutorial: https://github.com/crytic/building-secure-contracts/blob/master/program-analysis/echidna/end-to-end-testing.md
I follow all the instructions in the tutorial, however, the test result I get is "passed", rather than "failed"

The test contract:

The init file created by Etheno when running the unit test:

The echidna config file:

Final result:

the latest echidna release uses a different command line to specify the target contract. Instead of:

$ echidna-test contract.sol MyContract

it uses:

$ echidna-test contract.sol --contract MyContract

We should update the echidna information to match this.

There are a couple of risks that we can add:

• Risks associated with tokens that have external calls where the function id is controlled
• Decimals is not always 18
• Risks associated with rebalancing tokens

We have to review past audits to see what else is missing

• If you fuzz a parameter that is expected to have only some values, use %:

function f(uint index) public{
   index = `index%2`
   if (index == 0) {...}
   elif (index == 1) {...}
}

• To fuzz an arbitrary array length, you can use a push/pop approach (explain why?):

uint my_array[]

function push(uint a) public{
  my_array.push(a)
}

function pop() public{
  my_array.pop()
}

Over the years we wrote a lot of technical blogposts. We should list everything in a page to increase their visibility

• EIP-3675
• EIP-4399

• https://blog.trailofbits.com/2020/08/17/using-echidna-to-test-a-smart-contract-library/
• https://github.com/search?q=%22function+echidna_%22&type=Code
• Some of our public reports: https://github.com/trailofbits/publications

ethcc, dappcon, or devcon (tbd)

This would speed-up many analyses that do not require the detectors/gas consumption.

We could add a section "tips to optimize scripts", or something like that, that will explain how to just disable the gas, etc

This https://github.com/crytic/building-secure-contracts/blob/master/learn_evm/eips_forks.md, but for BSC/Avalanche, etc..

Similar to what we did with #148

Basically I was trying to replace Truffle with Hardhat in this example (https://github.com/crytic/building-secure-contracts/blob/master/program-analysis/echidna/end-to-end-testing.md), since Hardhat can offer multiple solc version support when compiling.

So the contracts I am using is the same as those in the drizzle-box example. Etheno can successfully record the transaction and then I tried using Echidna to run the end to end test. But there is error occuring:

I searched in Echidna and Crytic-compile repo and found the similar issues:
Echidna:
crytic/echidna#631
crytic-compile:
crytic/crytic-compile#164
crytic/crytic-compile#236

Then I checked my build-info file and I found it's located in the artifacts/build-info directory, there's only one build info json file. So I am wondering why crytic-compile output the "No such file or directory: 'artifacts/build-info'" error, since I did not make any special directory for the build info json file.

May I ask if there's any special argument needs to be added to the yaml config file? I tried to modify the cryticArgs option, but the same error occured, my config file hardhat.yaml shows below:

In arithmetic_overflow note the range of possible values in Cairo language is defined as (-P/2, P/2). That is the range if we consider felt as a signed number. We can use values greater than P/2, but then we treat felt as an unsigned number and the range is [0, P). Whether the felt is a signed or unsigned number in Cairo is a matter of interpretation, and it practically depends on which comparison/math functions we use on those felts.
An example of a different interpretation of the range of felt can be shown with comparison functions:

• is_le compares two felts interpreted as signed numbers, so in range (-P/2, P/2)
• is_le_felt compares two 'felts' interpreted as unsigned numbers, so in range [0, P)

The incorrect_felt_comparison note describes the issue with comparing felts, but there is also another issue with comparing felts using listed functions. assert_le is a good choice to compare members of a Uint256 struct, because they are in range [0, 2**128), but it is insecure to compare arbitrary felts with assert_le. assert_le(a, b) practically checks if b - a < 2**128, and not if any a is lesser than b. In fact, we can have a large value as a such that a > b, but because the subtraction operation is mod P the output from b - a < 2**128 would still be true. Example below shows an example where a is a large number, but assertion function does not throw an error:
assert_le(3618502788666131213697322783095070105282824848410658236509717448704103809026, 0), where value of a is less than P but higher than 0. This issue can be mitigated with using the assert_le_felt, which interprets compared felts in range [0, P).

Please kindly consider adding this to the existing notes for Cairo devs' knowledge.

https://github.com/crytic/building-secure-contracts/blob/master/program-analysis/echidna/how-to-test-a-property.md#initiate-a-contract claims that:

• 0x00a329c0648769A73afAc7F9381E08FB43dBEA72 is the caller of the constructor
• 0x00a329C0648769a73afAC7F9381e08fb43DBEA70 is the caller of other functions

However, it's just the opposite if you test it with an Ownable contract:

contract TestToken is Ownable {
    address echidna_caller = 0x00a329c0648769a73afac7f9381e08fb43dbea70;
    // address echidna_caller = 0x00a329c0648769a73afac7f9381e08fb43dbea72; <- this works
    constructor() public{
      balances[echidna_caller] = 10;
      // owner becomes 0x00a329c0648769a73afac7f9381e08fb43dbea70 here
    }
    function echidna_no_ownership() public view returns (bool) {
      return owner != echidna_caller; //fails
    }
  }

slither-flat can be useful, in particular through the conversion of external to public. We need a walkthrough example.

Hi,
I have tried to follow the exercise 7 of the Echidna Tutorial. As I have not been able to make Echidna find the bug by following the tutorial, I started digging where I went wrong. What I did is the following:

1. Deploying the SideEntranceLenderPool contract following the deploy script failed with insufficient funds for intrinsic transaction cost error; I needed to either decrease ETHER_IN_POOL or “donate” some funds from another account to the deployer. (I guess this step is not relevant to the bug though).

2. As the proposed solution here did not find the bug so I tried to debug. During debugging I found out that if I deployed the contract by the deploy script, only the ContractCreated event was generated by Etheno in the init.json. So, I modified the deploy script to have also FunctionCall event included in the init.json file by adding the following lines to the deploying script:

const depositTx = await pool.deposit({ value: ETHER_IN_POOL }); 
await depositTx.wait(1);

I did that because I assumed that the initial deposit to the contract might not be included in the init.json and thus the Echidna cannot break the invariant assert(address(pool).balance >= initialPoolBalance) as the pool balance is already zero.

Then I tried to run Echidna again by:

# start docker
sudo docker run -it --rm -v $PWD:/src trailofbits/eth-security-toolbox

# select compiler
solc-select use 0.8.7

# either run echidna on tutorial case:
npx hardhat clean && npx hardhat compile --force && echidna-test /src --contract E2E --config /src/contracts/side-entrance/echidna-etheno/config-tutorial.yaml

# or run echidna on my solution:
npx hardhat clean && npx hardhat compile --force && echidna-test /src --contract EchidnaEthenoSideEntranceLenderPool --config /src/contracts/side-entrance/echidna-etheno/config.yaml

Both last two commands returns:

echidna-test: VM failed for unhandled reason, Query <EVM.Query: fetch contract 0x000000000000000000636F6e736F6c652e6c6f67>. This shouldn't happen. Please file a ticket with this error message and steps to reproduce!

I tried to describe full details into a readme in my repo (see here).

Environment:

WIN11
WSL2
echidna is run in docker
etheno as binary
hardhat

ERC20 vs SafeIERC20

We haven't updated not so smart contract in a while: https://github.com/crytic/not-so-smart-contracts

We could merge its content here, and refresh it

• How to setup Echidna in a github action
• What values to set in seqLen / testLimit
• etc..

This guideline from September 2020 states that solidity 0.7 is too new to be used:

Solidity 0.7 is too young to be used in production and needs time to mature.
The slither documentation states something else

There seems to be an argument by the solidity developer team to use the most recent major release, as it usually has less bugs than previous version.

Proposal
Update the doc to the newest recommended version and explain why for example ^0.8 is too you to be used in production.

To show how to generate the initial corpus with Etheno using the unit tests

Show how to init Echidna with a truffle and embark test suite: https://github.com/crytic/echidna/wiki/Testing-Truffle-projects-with-Echidna

We can take the approach used in the ENS script: https://gist.github.com/feliam/ec8b9aa102055948524838ffe0a09769

https://www.youtube.com/watch?v=EUl3UlYSluU

Code size

• External function (and when it works)
• Using internal calls instead of modifiers
• How to split a large contract into smaller component
• ...

Transaction gas cost

• Local variables instead of multiple storage read
• ...

interface Target{
    function my_func(uint);
}

contract TestBytecodeOnly{
    Target t;

    constructor() public{
        address target_addr;
        bytes memory target_bytecode = hex"..."; // init bytecode

        uint size = target_bytecode.length;

        assembly{
            target_addr := create(0, 0xa0, size) // todo improve the hardcoded 0xa0 value
        }
        t = Target(target_addr);
    }


    function test(unit input) public {
        uint ret = t.my_func(input);
        assert( ret != 0);
    }
}

This pattern can be used to test contracts without the source code, or vyper contracts that require some initilization.

Another example is to do differential fuzzing between vyper and solidity.

Both the Echidna Wiki and the CLI help do not mention all the properties available to the user nor they explain what these properties mean.

An important example is sender vs psender.

Reference of config file properties.

https://manticore.readthedocs.io/en/latest/verifier.html

https://blog.trailofbits.com/2020/07/12/new-manticore-verifier-for-smart-contracts/

We could revisit https://github.com/crytic/building-secure-contracts/tree/master/program-analysis/echidna, to have a common part that will work for both Echidna/manticore-verifier, and then advanced tutorials that would nightlight the specificities of each tool

Based on the token integration checklist, we could create a list of deployment tokens, and show their risks and edge cases

Understand some smart contract addresses may be reusable with the introduction of the CREATE2 opcode. That is, they can self destruct and be redeployed to the same address: https://blocking.net/8282/wisps-the-wonderful-world-of-create2/

Hi,

I am trying to run some assertion testing with Echidna 2.0 by using the examples provided in the docs :

pragma solidity 0.5.11;

contract Incrementor {
    uint256 private counter = 2**200;

    function inc(uint256 val) public returns (uint256) {
        uint256 tmp = counter;
        counter += val;
        assert(tmp <= counter);
        return (counter - tmp);
    }
}

config file :

checkAsserts: true

When running echidna-test incrementor.sol --config config.yaml I get a the following warning Warning: unused option: checkAsserts and the following message echidna-test: No tests found in ABI

Why isn't echidna detecting any test ?

i can't understand this.

• What sections to focus
• What areas to master
• What questions readers should be able to answer

Etc...

The plugin allows in-depth control over the operations that are executed.

A good example the CFG builder from @feliam: https://github.com/trailofbits/manticore/blob/466a44efa0467aeac80e5423d03eae2c0b23e1cb/manticore/ethereum/plugins.py#L222-L296

We need an exercise that shows how to create a plugin. For example:

• Hook an external call to an Oracle contract, and returns a constrained symbolic value (ex: value > 100, and value < 1,000)

/data/echidna/examples/solidity/basic# echidna-test flags.sol --config config.yaml
Segmentation fault

https://github.com/crytic/evm-opcodes

https://github.com/crytic/building-secure-contracts/blob/master/program-analysis/echidna/how-to-test-a-property.md#initiate-a-contract

There are some specific addresses in Echidna:

• 0x00a329c0648769A73afAc7F9381E08FB43dBEA72 which calls the constructor.
• 0x10000, 0x20000, and 0x00a329C0648769a73afAC7F9381e08fb43DBEA70 which randomly calls the other functions.

When i checked the owner of the contract using an echidna property, the owner of the contract is 0x00a329C0648769a73afAC7F9381e08fb43DBEA70. Not 0x00a329c0648769A73afAc7F9381E08FB43dBEA72.

Should this readme be updated?
Or am i misunderstanding something?

I can create a pull request for this if needed.