VM failed for unhandled reason

[0xharold]

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

[0xharold]

As a follow-up of this task I would like to ask you several questions related to the topic itself:

• Is there any chance to solve this task without using the Etheno? For instance, the solution could look similar to a naive-receiver task. Unfortunately, I have not been able to solve this problem (without usage of etheno) - you can take a look here.
• Could Echidna find the vulnerability even though we were not aware of the bug? The solution here is imho influenced by knowledge of the bug itself. Does any more general solution/approach exist? Why would I use Echidna if I already know the bug in advance?
• What is the purpose of setEnableWithdraw and setEnableDeposit? Would not that function without these setters as well?

[rappie]

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).

Interesting. Does this also happen when you run npx hardhat run scripts/deploy.js (without localhost) ?

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.

I believe this is because of a known issue which should be fixed in this branch: https://github.com/crytic/etheno/tree/rc-1

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!

Can you try this using the latest version of echidna? https://github.com/crytic/echidna/releases/tag/v2.0.3

Is there any chance to solve this task without using the Etheno? For instance, the solution could look similar to a naive-receiver task. Unfortunately, I have not been able to solve this problem (without usage of etheno) - you can take a look here.

I'm not sure, maybe someone else can chime in here. Personally I always use etheno because I like this approach.

Could Echidna find the vulnerability even though we were not aware of the bug? The solution here is imho influenced by knowledge of the bug itself. Does any more general solution/approach exist? Why would I use Echidna if I already know the bug in advance?

Actually, I solved the challenge using this approach without knowing the solution in advance! 😄

What is the purpose of setEnableWithdraw and setEnableDeposit? Would not that function without these setters as well?

These are used to let echidna search for the right function calls in the flash loan callback function (execute()). If you're not familiar with flashloans and/or callbacks, take a look here: https://uniswapv3book.com/docs/milestone_3/flash-loans/

Thanks for your questions/feedback. Good luck!

[glarregay-tob]

Hello Lubos, you can try the modified solution in this PR to avoid the use of Etheno.
Regarding your second bullet point, the idea is that you need to know the contract's invariants and create the properties based on them. You might know the bug, but not its presence in the contract, so you create a property to check it. Does that make sense?

[anishnaik]

To add to @glarregay-tob's and @rappie's points, the provided invariant basically checks whether there is a way for the system to lose funds, which there should not be at the end of an atomic flash loan. So, yes, you knew the bug so it seems trivial. But in general, the property says "the system should not lose funds" which is a strong property that should hold for a flash loan system.

[0xharold]

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).

Interesting. Does this also happen when you run npx hardhat run scripts/deploy.js (without localhost) ?

Nope, it happens only if Etheno (Ganache) is running.

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.

I believe this is because of a known issue which should be fixed in this branch: https://github.com/crytic/etheno/tree/rc-1

Nice, I upgraded etheno to 0.3.1 and it seems to be fixed! Thanks!

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!

Can you try this using the latest version of echidna? https://github.com/crytic/echidna/releases/tag/v2.0.3

I used the latest version of Echidna (v2.0.3) and unfortunately it keeps returning the same error.

What is the purpose of setEnableWithdraw and setEnableDeposit? Would not that function without these setters as well?

These are used to let echidna search for the right function calls in the flash loan callback function (execute()). If you're not familiar with flashloans and/or callbacks, take a look here: https://uniswapv3book.com/docs/milestone_3/flash-loans/

I see now. We want to have every possible combination of function call(s) in the callback to be checked by Echidna. Thanks!

[0xharold]

@glarregay-tob thank you very much for the solution provided.
@glarregay-tob and @anishnaik thank you for the explanation. It is much clearer for me now.

[rappie]

Nope, it happens only if Etheno (Ganache) is running.

This might be because the default balance of the signers is too low. You could try adding --balance 10000 (as a seperate arg, not inside --ganache-args)

I used the latest version of Echidna (v2.0.3) and unfortunately it keeps returning the same error.

Then I recommend creating an issue on the echidna repo if you still want to continue this path with using etheno.

[0xharold]

@glarregay-tob
I went through your solution (thank you again) and unfortunately it fails with echidna-test: Calling the setUp() funciton failed (revert, out-of-gas, sending ether to an non-payable constructor, etc.). Any idea why?

[glarregay-tob]

Ah, yes, my mistake, sorry. The contractBalance parameter in config.yaml should be 1000 ether instead of 10000. This is the msg.value passed to the constructor, and as it is, it will make it revert because of the require statement.
The PR file is now fixed, please try and let me know if it works now.

[0xharold]

@glarregay-tob thank you!

[0xharold]

To have answers to all my questions there is the last one which remains to be resolved:

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!

When I used etheno to generate the init.json file there was @hardhat/console.sol library imported in the contract to be deployed which was causing the problem (see here ). To fix this, I just removed this import and run etheno again. Credit to @ggrieco-tob who pointed that out on the Slack.

[gustavo-grieco]

Interestingly enough 636F6e736F6c652e6c6f67 seems to be ASCII for console.log. We need to provide something there to avoid this crash.