In web3, we have a number of fuzzing tools like foundry's fuzz & invariant tests and Trail of Bits Echidna.
But what are the purposes of symbolic execution tools like manticore and maat?
Fuzz testing still seems to execute code, so I'm not sure I understand the categorical difference between fuzzing and symbolic execution.
Fuzzing & Symbolic execution accomplish similar goals of finding cases where code breaks, but have tradeoffs in speed vs. precision, and take very different approaches.
Fuzzing: Much faster to do, but less precise.
Symbolic Execution: Much slower to do, but more precise.
Let's look at a practical example to understand the difference between these two.
We will state with an example where fuzz testing can shine.
pragma solidity ^0.8.16;
contract VulnerableContractOne {
function func_one(int128 x) public {
if (x == -20) {
revert(); // BUG
}
}
}
(Yes,func_one could be restricted to pure, but the current foundry tester was having a hard time reading the function from the ABI as a pure function)
In our contract above, we can clearly see that entering -20 as an input parameter to func_one will result in a revert, which we will say is where our bug is.
Approaching this from a foundry fuzz/invariant test we can write a fuzz or invariant test that will throw pseudo-random values at this function until it finds an area that will break it.
// SPDX-License-Identifier: UNLICENSED
pragma solidity ^0.8.16;
import "forge-std/Test.sol";
import "forge-std/StdInvariant.sol";
import "../contracts/VulnerableOne.sol";
contract VulnerableOneTest is StdInvariant, Test {
VulnerableOne public vulnerableOne;
function setUp() public {
vulnerableOne = new VulnerableOne();
targetContract(address(vulnerableOne));
}
// Our Fuzz Test (stateless fuzz test)
function testShouldNeverRevert(int128 x) public {
vulnerableOne.funcOne(x);
}
// Our Invariant Test (stateful fuzz test)
function invariant_shouldNeverRevert() public {
assert(true);
}
}
And in our foundry.toml we can set the config:
[fuzz]
runs = 1000
seed = '0x3e8'
include_storage = true
include_push_bytes = true
[invariant]
runs = 2000
depth = 15
fail_on_revert = true
To run one of the two tests alone, we can do one of the following to run that single respective test:
forge test -m testShouldNeverRevert
forge test -m invariant_shouldNeverRevert
You can learn more about the difference between fuzz tests and invariant tests here, but the synopsis is that fuzz tests are the process of providing random data as inputs during testing to break something.
Foundry fuzz tests are known as stateless fuzzing. Where each "run" of a fuzz test (like our testShouldNeverRevert) is independent.
Foundry invariant tests are known as stateful fuzzing. Where each "run" of an invariant test consists of many function calls where the state of the system is contained. Ie, if storage is changed, then storage persists between function calls until a run has completed. You can increase the number of function calls by adjusting the depth in foundry.toml. The larger the depth the more function calls the test will make.
For the rest of this post, I will refer to foundry's fuzz tests as "stateless fuzzing test" and invariant tests as "stateful fuzzing test"
If we run either one of our tests, we will see that we are able to find the bug of supplying -20 as an input parameter. Foundry can be a little intelligent with the random values it supplies to try, it'll look at storage of the contract and other values to try to find a bug.
Output of forge test -m testShouldNeverRevert:
Running 1 test for test/VulnerableOne.t.sol:VulnerableOneTest
[FAIL. Reason: EvmError: Revert Counterexample: calldata=0x5cee85beffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffec, args=[-20]] testShouldNeverRevert(int128) (runs: 899, μ: 5561, ~: 5561)
Test result: FAILED. 0 passed; 1 failed; finished in 46.05ms
With seed = '0x3e8' in our foundry.toml we will always get this output.
However, our forge test -m invariant_shouldNeverRevert can give different outputs.
Either:
Running 1 test for test/VulnerableOne.t.sol:VulnerableOneTest
[PASS] invariant_shouldNeverRevert() (runs: 1000, calls: 15000, reverts: 0)
Test result: ok. 1 passed; 0 failed; finished in 1.01s
Or something like:
[FAIL. Reason: EvmError: Revert]
[Sequence]
sender=0x000000000000000000000000000000003e5e3c23 addr=[contracts/VulnerableOne.sol:VulnerableOne]0x5615deb798bb3e4dfa0139dfa1b3d433cc23b72f calldata=funcOne(int128), args=[-170141183460469231731687303715884104505]
sender=0xe5b327aeb092428856e2b70d9a0a0bfa7ca794fb addr=[contracts/VulnerableOne.sol:VulnerableOne]0x5615deb798bb3e4dfa0139dfa1b3d433cc23b72f calldata=funcOne(int128), args=[-170141183460469231731687303715884104438]
sender=0x000000000000000000000000000000000000007f addr=[contracts/VulnerableOne.sol:VulnerableOne]0x5615deb798bb3e4dfa0139dfa1b3d433cc23b72f calldata=funcOne(int128), args=[170141183460469231731687303715884105726]
sender=0x00000000000000000000000000000000000000ce addr=[contracts/VulnerableOne.sol:VulnerableOne]0x5615deb798bb3e4dfa0139dfa1b3d433cc23b72f calldata=funcOne(int128), args=[-170141183460469231731687303715884105504]
sender=0x00000000000000000000000000000000000000ce addr=[contracts/VulnerableOne.sol:VulnerableOne]0x5615deb798bb3e4dfa0139dfa1b3d433cc23b72f calldata=funcOne(int128), args=[-170141183460469231731687303715884103908]
sender=0x00000000000000000000000000000000000000af addr=[contracts/VulnerableOne.sol:VulnerableOne]0x5615deb798bb3e4dfa0139dfa1b3d433cc23b72f calldata=funcOne(int128), args=[-20]
With our stateful fuzz test, we can see it took a few calls in a single run to find -20.
In any case, we were able to very quickly find the edge case of the bug in this. However, we got a little lucky. Fuzzing tries random values, and if you change the number of runs to something much less like 10, it's highly likely foundry wouldn't have found our edge case.
Now, let's try to approach finding this bug using symbolic execution. Symbolic execution is the process of exploring the state paths of a program given different inputs to arrive at a mathematical expression that describes the system.
Let's look at that another way.
To do symbolic execution, we'd want to take our function and replicate it as a mathematical expression.
Something like the following (not actual code)
x > -2**128 && x < 2**128 // type constraints on x
if(x == 231) break // conditional
assert(x) // check for not reverting
You could then take your model and place it into an SMT Solver like z3.
Once you have a model, the math to prove the assumptions becomes much easier, since math is either correct or not.
The solidity compiler comes pre-built with an SMTChecker which under the hood does this process.
The SMTChecker looks for assert commands to break, so in a test we could update our file:
pragma solidity ^0.8.16;
contract VulnerableContractOne {
function func_one(int128 x) public {
if (x == -20) {
assert(false);
revert(); // BUG
}
assert(true);
}
}
And solidity will attempt to convert this solidity code into a mathematical expression and look for the path to break the asserts.
We can run the SMT Checker on this solidity code like so:
solc VulnerableOne.sol --model-checker-targets all --model-checker-engine all
And you'll get an output like:
Warning: CHC: Assertion violation happens here.
Counterexample:
x = (- 20)
Transaction trace:
VulnerableContractOne.constructor()
VulnerableContractOne.func_one((- 20))
--> VulnerableOne.sol:7:13:
|
7 | assert(false);
| ^^^^^^^^^^^^^
This tells us it found out that -20 breaks the asserts. This is also an example of formal verification where we used math to prove or disprove a model works in an expected way. We've proven that the model can revert, when we expect the model to never revert.
In our symbolic execution example we were able to find exactly the breaking path by converting our solidity to math, whereas in our fuzzing we just threw random values at it until we got the correct value.
Writing fuzz tests are much quicker and mentally easier than making sure our symbolic execution tests are correct, as there is a lot more to think about.
Now let's update the code to be a little tricker:
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.16;
contract VulnerableContractOne {
function func_one(int128 x) public {
if (x / 4 == -2022) {
assert(false);
revert(); // BUG
}
assert(true);
}
}
If we run this in a foundry fuzz tester, it MAY find the right value, but more often than not the random attempts it makes won't find the value that sustains this.
We can update our SMTChecker test:
pragma solidity ^0.8.16;
contract VulnerableContractOne {
function func_one(int128 x) public {
if (x / 4 == -2022) {
assert(false);
revert(); // BUG
}
assert(true);
}
}
Running our SMTChecker results in this:
Warning: CHC: Assertion violation happens here.
Counterexample:
x = (- 8088)
Transaction trace:
VulnerableContractOne.constructor()
VulnerableContractOne.func_one((- 8088))
--> VulnerableOne.sol:7:13:
|
7 | assert(false);
| ^^^^^^^^^^^^^
And instantly gets the correct path for our issue.
This is because the SMTChecker models out the code, and then tries to break assumptions based on the path.
In this example, it was relatively trivial to get our symbolic tests up and going, but getting these correct for more complicated projects where more complicated invariants need to hold make writing these a much more time laborious process.
Some more clever tactics have sprung up such as hybrid fuzzing where fuzz attempts are fed into a symbolic execution framework that tries to model the system to get smarter with future inputs, as opposed to just continuing to do random attempts.