Find the repo here: [GitHub] Solidity Properties.

On February, 27^th 2023, Trail of Bits (ToB) released reusable properties for common solidity contracts. It includes 168 properties for ERC20 and ERC721tokens, ERC4626 vaults, and the ABDKMath64x64 fixed-point library. These properties are designed to detect vulnerabilities, ensure adherence to relevant standards, and provide educational guidance for writing invariants.

The ToB suite can be used with Echidna, a fuzzer for testing solidity smart contracts. It utilizes a smart approach to generate customized inputs based on the source code. However, as it relies on fuzzing techniques, the inputs are still randomly generated. As a test-based methodology, fuzz testing cannot guarantee the complete absence of bugs

“Program testing can be used to show the presence of bugs, but never to show their absence!” ― Edsger W. Dijkstra

Perhaps most debilitating is that Echidna’s efficiency in identifying bugs is directly proportional to computational power and time. The variance in detection time, ranging from immediate to 30 hours or more, without guaranteeing bug identification, highlights significant resource dependency.

In contrast to fuzzing, symbolic testing is a formal verification methodology that can selectively generate required input data using SMT solvers like Z3, CVC5, and others. Therefore, if a symbolic test passes, we can formally verify that the property under test is truly satisfied.

Show, Don't Tell

We are utilizing Ethereum's symbolic tester, hevm, to successfully perform symbolic testing in this endeavor. The capability of hevm to interface with SMT solvers allows us to formally reason about smart contract properties and prove the presence or absence of vulnerabilities.

To provide a small illustration of such symbolic tests, we have:

function setUp() public {

      token = new MyERC20("ERC20Token", "ERC20Token", 10 ** 18);

}

function prove_Approve(address spender, uint256 amount) public {

      if(msg.sender != address(0) && spender != address(0)) {

            bool success = token.approve(spender, amount);

            assert(success);

            assert(token.allowance(msg.sender, spender) ==  amount);

       } else revert();

}

In the previous code fragment, the prefix prove (in prove_Approve) activates hevm's symbolic execution engine to verify an expected positive behavior, instead of fuzzing (prefix check directs hevm to run a fuzzer). And the revert() function in the else branch ensures that hevm does not incorrectly report a passing test without actually verifying the assertions!

Formal verification of Solidity functions requires testing both(!) expected positive behaviors and potential negative behaviors involving reverts. While positive symbolic tests can verify intended functionality, detecting revert conditions also needs negative symbolic tests. For the previous code example, two negative symbolic tests could be derived to verify for revert scenarios:

function proveFail_ApproveWhenSenderIsZero(address spender, uint256 amount) public {

      if(msg.sender == address(0)) {

            bool success = token.approve(spender, amount);

       } else revert();

}

function proveFail_ApproveWhenSpenderIsZero(address spender, uint256 amount) public {

      if(spender == address(0)) {

            bool success = token.approve(spender, amount);

       } else revert();

}

In the previous code, there is no need to call vm.expectRevert() because proveFail in hevm automatically searches for reverts in all branches. This is why a revert() is included in the else branch—to ensure hevm catches any potential revert in that path. And this is also needed by hevm's heuristic algorithms like in the positive behavior.

Notable Features

We have developed and tested symbolic tests to formally verify common properties for the following solidity contracts:

• ERC20: 27 symbolic tests;

• ERC721: 21 symbolic tests;

• ERC1155: 12 symbolic tests.

Last updated: Dec 8 2023

What's Next

• ERC4626

If you are interested in formally verifying your system, don’t hesitate to contact us at info@lindylabs.net!