Try Echidna in every challenge from The Ethernaut CTF

[ggrieco-tob]

Review every challenge from The Ethernaut CTF, to see which ones can be solve automatically using Echidna.

A plan to proceed:

1. Report back the results here for discussion.
2. Create a markdown with the properties and config files required for each challenge.
3. In case of failing to solve some of the, identify potential issues and how they could solved with new features or fixes.

Bonus: identify usability issues.

[elopez]

I've been trying to complete this CTF with Echidna for the last week or two, here's a recap of my findings so far:

#	Name	Solved	Echidna	Filed issues
01	Fallback	Yes	:muscle:
02	Fallout	Yes	:muscle:
03	Coin Flip	Yes	:muscle:
04	Telephone	Yes	:mag:
05	Token	Yes	:muscle:
06	Delegation	Yes	:mag:
07	Force	Yes	:mag:
08	Vault	N/A	-
09	King	WIP	-
10	Re-entrancy	Yes	:mag:
11	Elevator	Yes	:muscle:
12	Privacy	N/A	-
13	Gatekeeper One	Yes	:muscle:
14	Gatekeeper Two	Yes	:mag:	crytic/echidna#453
15	Naught Coin	Yes	:muscle:
16	Preservation		-
17	Recovery	N/A	-
18	MagicNumber	N/A	-
19	Alien Codex	WIP	-	crytic/echidna#440, crytic/slither#450
20	Denial	Yes	:muscle:	crytic/echidna#442
21	Shop	Yes	:mag:	crytic/echidna#446

Echidna reference:

• :muscle:: Echidna breaks the invariant by itself or mostly by itself
• :mag:: Echidna merely verifies that some given code breaks the provided invariant

I have marked some levels as 'N/A' - these are levels that I felt were out of scope for a tool like Echidna. If you want to see the contracts I used to solve them, you can check out my repo at https://github.com/elopez/echidna-ethernaut

[ggrieco-tob]

@elopez can you re-run this with the latest master revision and update the table?

[smonicas]

@elopez can you re-run this with the latest master revision and update the table?

Tried some solutions with the following configuration:

• Echidna 1.7.2
• Solidity 0.6.12
• openzeppelin-contracts 3.0.0

? = Not tested

#	Name	Solved	Echidna	Filed issues
01	Fallback	Yes	💪
02	Fallout	Yes	💪
03	Coin Flip	Yes	💪
04	Telephone	Yes	🔍
05	Token	Yes	💪
06	Delegation	Yes	🔍
07	Force	Yes	🔍
08	Vault	?
09	King	?
10	Re-entrancy	Yes	🔍
11	Elevator	Yes	💪
12	Privacy	?
13	Gatekeeper One	Yes	💪
14	Gatekeeper Two	Yes	🔍
15	Naught Coin	Yes*	💪
16	Preservation	?
17	Recovery	?
18	Magic Number	?
19	Alien Codex	?
20	Denial	Yes	💪
21	Shop	Yes	🔍

* It needs to edit "player" name variable in test.sol otherwise with solidity 0.6.12 fails to compile "identifier already declared"

EDIT: Updated with more solutions tested.

[smsunarto]

Continuing where @smonicas left off

#	Name	Solved	Echidna	Filed issues
01	Fallback	Yes	💪
02	Fallout	Yes	💪
03	Coin Flip	Yes	💪
04	Telephone	Yes	🔍
05	Token	Yes	💪
06	Delegation	Yes	🔍
07	Force	Yes	🔍
08	Vault	?
09	King	?
10	Re-entrancy	?
11	Elevator	?
12	Privacy	?
13	Gatekeeper One	?
14	Gatekeeper Two	?
15	Naught Coin	?
16	Preservation	?
17	Recovery	?
18	Magic Number	?
19	Alien Codex	?
20	Denial	?
21	Shop	?

Documentation observation/note:

• Had some confusion on why Echidna is fuzzing imported contract for a while, might be helpful to point out the usage of --contract parameter.

[man715]

I was going through this and got stuck on on 01-Fallback. It appears that the code has changed since the last time this has been attempted. The Fallback.sol contract is now using the receive fallback function which echidna 2.0.1 does not catch therefore the test never fails. However, if I change the receive function to be function receive() or fallback() then the test fails.

[ggrieco-tob]

Good catch. There is fix coming in https://github.com/crytic/echidna/pull/722 but it depends on a slither printer (which I think it was already released). Btw, if you are interesting in working in this issue, please let us know, we definitely want to complete as much examples as possible and move everything into building secure contract.

[man715]

Yeah, I'm working through these but I'm pretty new to the whole space. I'm sure what the original table was indicating between what the :muscle: and the :mag: though. I'm creating my own version based off the original and will be more than happy to help out as time allows.

[ggrieco-tob]

@elopez worked on the original table, he can clarify this next week

[elopez]

Hi! Here's a expanded reference of the original table:

• 💪: Echidna breaks the invariant by itself or mostly by itself. The echidna-specific code needed contains an echidna property to represent the CTF "win" condition, and Echidna finds the (series of) calls that break the contract via fuzzing. Example: Fallout test contract; it extends the CTF contract and only adds a single echidna property.
• 🔍: Echidna merely verifies that some given code breaks the provided invariant. The code needed contains an echidna property as well as extra functions and any auxiliary contracts required to execute the attack to solve the exercise. Example: Gatekeeper Two test contract; it has helper contracts and an extra function to trigger the attack, as well as an echidna property that represents the CTF "win" condition. When echidna triggers the attack and then runs the property, it will confirm that the attack was successful.

Solutions of the ":muscle:" style are more interesting, but sometimes these exercises are not that easily solvable with a fuzzer. The "🔍" style solutions were good practice for me and lead to discovering some bugs in echidna so I think they're valuable as well 😄

[man715]

Hi! Here's a expanded reference of the original table:

• muscle: Echidna breaks the invariant by itself or mostly by itself. The echidna-specific code needed contains an echidna property to represent the CTF "win" condition, and Echidna finds the (series of) calls that break the contract via fuzzing. Example: Fallout test contract; it extends the CTF contract and only adds a single echidna property.
• mag: Echidna merely verifies that some given code breaks the provided invariant. The code needed contains an echidna property as well as extra functions and any auxiliary contracts required to execute the attack to solve the exercise. Example: Gatekeeper Two test contract; it has helper contracts and an extra function to trigger the attack, as well as an echidna property that represents the CTF "win" condition. When echidna triggers the attack and then runs the property, it will confirm that the attack was successful.

Solutions of the "muscle" style are more interesting, but sometimes these exercises are not that easily solvable with a fuzzer. The "mag" style solutions were good practice for me and lead to discovering some bugs in echidna so I think they're valuable as well smile

Thank you. This helps clear up the classifications.

[ggrieco-tob]

Hi @man715, just wondering was the state of the testing of Echidna in The Ethernaut? Are you blocked by some issue?

[man715]

Hey @ggrieco-tob I have not had much time. I hope to get back to it this weekend.

[man715]

Here is what I have so far. I'm going at this with the assumption that an individual may not know how to solve the challenge before running Echidna.

#	Name	Solved with Echidna	Echidna	Filed Issue	Notes
01	Fallback	Yes	:muscle:
02	Fallout	Yes	:muscle:
03	Coin Flip	No	:no_entry_sign:		The fuzzer does potentially lead you down the right path for solving this issue as it does cause the invariant to fail on 10 consecutive tries with time/block delays. However, in my testing it does not help discern what delay will give consistent predictable results. One thing to note is that the solution to this problem is not using a delay but instead to use the block hash to determine if the coin flip result will be heads or tails.
04	Telephone	Yes	:mag:
05	Token	Yes	:muscle:
06	Delegation	Yes	:mag:	https://github.com/crytic/echidna/issues/764
07	Force	N/A	:no_entry_sign:		Not applicable to a fuzzer.
08	Vault	N/A	:no_entry_sign:		Not applicable to a fuzzer.
09	King	N/A	:no_entry_sign:		Not applicable to a fuzzer.
10	Re-entrancy	Yes	:mag:
11	Elevator	N/A	:no_entry_sign:		Not applicable to a fuzzer.
12	Privacy	N/A	:no_entry_sign:		Not applicable to a fuzzer.
13	Gatekeeper One	No	:no_entry_sign:		For Echidna to break this contract, it would need to randomize the amount of gas being sent.
14	Gatekeeper Two	No	:no_entry_sign:		For Echidna to be able to solve this challenge, it would have to be able to randomize the inputs for a constructor.
15	Naught Coin	Yes	:muscle:
16	Preservation	N/A	:no_entry_sign:		Not applicable to a fuzzer.
17	Recovery	N/A	:no_entry_sign:		Not applicable to a fuzzer.
18	MagicNumber	N/A	:no_entry_sign:		Not applicable to a fuzzer.
19	Alien Codex	No	:no_entry_sign:		Not applicable to a fuzzer. The only way that this could be solved is if you could specify a value that would be fuzzed (the sender's address) and it randomly puts it in various parts of an array. Lastly, echidna would need to be able to expand an array to wrap around the length of the storage space 2^256 - 1. I don't think this is a feasible expectation.
20	Denial	N/A	:no_entry_sign:		Not applicable to a fuzzer.
21	Shop
22	Dex	N/A	:no_entry_sign:		Not applicable to a fuzzer.
23	Dex Two
24	Puzzle Wallet
25	Motorbike
26	DoubleEntryPoint

Reference:

• :muscle:: Echidna breaks the invariant by itself or mostly by itself. The echidna-specific code needed contains an echidna property to represent the CTF "win" condition, and Echidna finds the (series of) calls that break the contract via fuzzing. Example: Fallout test contract; it extends the CTF contract and only adds a single echidna property.
• :mag:: Echidna merely verifies that some given code breaks the provided invariant. The code needed contains an echidna property as well as extra functions and any auxiliary contracts required to execute the attack to solve the exercise. Example: Gatekeeper Two test contract; it has helper contracts and an extra function to trigger the attack, as well as an echidna property that represents the CTF "win" condition. When echidna triggers the attack and then runs the property, it will confirm that the attack was successful.
• :no_entry_sign:: Echidna could not conclusively suggest an issue or provide a solution to the challenge

You can see my short writeups here

[ggrieco-tob]

This is great. The only suggestion I have so far is to include some comment on why Echidna cannot run in each example with :no_entry_sign:

[man715]

This is great. The only suggestion I have so far is to include some comment on why Echidna cannot run in each example with no_entry_sign

I've updated the table. If anything is incorrect with my assumptions, please let me know and I can go back and try testing again.

[glarregay-tob]

For completeness:

#	Name	Solved with Echidna	Echidna	Filed Issue	Notes
01	Fallback	Yes	:muscle:
02	Fallout	Yes	:muscle:
03	Coin Flip	No	:no_entry_sign:		The fuzzer does potentially lead you down the right path for solving this issue as it does cause the invariant to fail on 10 consecutive tries with time/block delays. However, in my testing it does not help discern what delay will give consistent predictable results. One thing to note is that the solution to this problem is not using a delay but instead to use the block hash to determine if the coin flip result will be heads or tails.
04	Telephone	Yes	:mag:
05	Token	Yes	:muscle:
06	Delegation	Yes	:mag:	https://github.com/crytic/echidna/issues/764
07	Force	N/A	:no_entry_sign:		Not applicable to a fuzzer.
08	Vault	N/A	:no_entry_sign:		Not applicable to a fuzzer.
09	King	N/A	:no_entry_sign:		Not applicable to a fuzzer.
10	Re-entrancy	Yes	:mag:
11	Elevator	N/A	:no_entry_sign:		Not applicable to a fuzzer.
12	Privacy	N/A	:no_entry_sign:		Not applicable to a fuzzer.
13	Gatekeeper One	No	:no_entry_sign:		For Echidna to break this contract, it would need to randomize the amount of gas being sent.
14	Gatekeeper Two	No	:no_entry_sign:		For Echidna to be able to solve this challenge, it would have to be able to randomize the inputs for a constructor.
15	Naught Coin	Yes	:muscle:
16	Preservation	N/A	:no_entry_sign:		Not applicable to a fuzzer.
17	Recovery	N/A	:no_entry_sign:		Not applicable to a fuzzer.
18	MagicNumber	N/A	:no_entry_sign:		Not applicable to a fuzzer.
19	Alien Codex	No	:no_entry_sign:		Not applicable to a fuzzer. The only way that this could be solved is if you could specify a value that would be fuzzed (the sender's address) and it randomly puts it in various parts of an array. Lastly, echidna would need to be able to expand an array to wrap around the length of the storage space 2^256 - 1. I don't think this is a feasible expectation.
20	Denial	N/A	:no_entry_sign:		It must be solved via a contract.
21	Shop	N/A	:no_entry_sign:		It must be solved via a contract.
22	Dex	No, but doable.	:question:		Actually, this should be solvable by echidna. It is a very specific sequence, but given enough time, a fuzzer should break it. See this gist for the relevant contract/config.
23	Dex Two	N/A	:no_entry_sign:		It needs a crafted ERC20 contract to be deployed, and then a sequence of calls should be made. The sequence could be inferred by Echidna, but the contract has to be manually created by knowing the solution.
24	Puzzle Wallet	N/A	:no_entry_sign:		It does not require a contract to be deployed, but requires some hand crafted calldata and a specific sequence of calls.
25	Motorbike	N/A	:no_entry_sign:		It must be solved via a contract.
26	DoubleEntryPoint	N/A	:no_entry_sign:		It must be solved via a contract.
27	Good Samaritan	N/A	:no_entry_sign:		It must be solved via a contract.

[ggrieco-tob]

Thanks to everyone that contributed here. I believe we can close this issue. There are not enough challenge to solve with a fuzzer in the current ethernaut (perhaps in some old version). Perhaps Dex Two can be added to building secure smart contracts.