A Guide on Crafting Robust Invariants with Echidna

Stay ahead with web3’s largest news aggregator in security, blockchain, DeFi, and threat intel on hacks, vulnerabilities, security tools, podcasts, and events.

Writing Invariants using Echidna

Introduction:

Effective fuzzing begins with meticulous system initialization. From straightforward setups to more complex configurations, proper initialization is paramount for robust security testing. Harness tools like Ethene and leverage unit test frameworks to streamline the process, setting the stage for comprehensive smart contract security assessments.

How to Define Good Invariants?

Begin with clear and concise English invariants.Translate these invariants into Solidity for effective testing.Keep it manageable; start small and iterate for complexity.

Fuzzing Process:

Define invariants, write them in Solidity, and run Echidna.If invariants break, investigate the issues thoroughly.Once invariants pass, loop back to step 1 for continuous improvement.

Functional-level Invariants:

These invariants are stateless and can be tested in isolation.Example: Associative property of addition in a contract.How: Inherit the target contract, create a function, call the targeted function, and use “assert” to check the property

Example Code in Solidity:

contract TestTokenTransfer is TokenTransfer {
function test_secure_transfer(uint amount, address recipient) public {
assert(secure_transfer(amount, recipient) == secure_transfer(amount, recipient));
}
}

System-level Invariants :

Rely on the deployment of a large system or the entire system.These invariants are usually stateful.Example: Ensuring a user’s balance is less than the total supply.

Example Code in Solidity:

contract TestTokenBalance is TokenBalance {
address validator = msg.sender;
constructor() public {
balances[validator] = 10000;
}
function test_balance() public {
assert(balances[validator] <= 10000);
}
}

Valid State :

Valid states are the foundation of a system’s integrity, setting the allowed values for its variables.

They are crucial in preventing unintended issues and ensuring the system behaves as intended, steering clear of critical bugs.

Developers depend on valid states to guide a system’s workflow, guaranteeing expected outcomes and averting unplanned glitches.Enforcing a single valid state at any time maintains system order, preventing confusion and ensuring a smooth, predictable workflow.Recognizing and handling valid states proactively mitigates risks in software development, fostering the creation of robust and reliable systems.Example: Consider a web application handling user authentication. Valid states in this scenario include “User Not Authenticated,” “User Authenticated,” and “User Session Expired.” If the system unintentionally allows a user to access authenticated features without proper authentication, it could lead to a security breach. Enforcing valid states ensures that the user is always in one of these states, preventing unauthorized access and potential vulnerabilities.

Example Code in Solidity:

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;

contract UserAuthentication {

enum UserState {NotAuthenticated, Authenticated, SessionExpired}
UserState public userState;

constructor() {
// Initialize the contract with the user in a non-authenticated state
userState = UserState.NotAuthenticated;
}
modifier onlyInState(UserState _state) {
require(userState == _state, "Invalid state transition");
_;
}
function authenticateUser() external onlyInState(UserState.NotAuthenticated) {
// Logic to authenticate the user
// For simplicity, let's just change the state to Authenticated
userState = UserState.Authenticated;
}
function performLogout() external onlyInState(UserState.Authenticated) {
// Logic to log out the user
// For simplicity, let's just change the state to NotAuthenticated
userState = UserState.NotAuthenticated;
}
function simulateSessionExpiry() external onlyInState(UserState.Authenticated) {
// Simulate session expiry
// For simplicity, let's just change the state to SessionExpired
userState = UserState.SessionExpired;
}
}

Observation:

The contract UserAuthentication has an enumeration UserState representing the valid states: NotAuthenticated, Authenticated, and SessionExpired.The userState variable keeps track of the current state of the user.The onlyInState modifier ensures that certain functions can only be called when the user is in a specific state, preventing unintended state transitions.Functions like authenticateUser, performLogout, and simulateSessionExpiry showcase how the system transitions between valid states based on specific actions.

State Transitions :

Valid state transitions ensure changes occur in the correct order, maintaining the integrity of the system’s state machine.Transitions are verified to occur only under specific conditions, such as function calls or elapsed time, preventing undesired state changes.The correctness of transitions guarantees a systematic state machine, where each change follows the predefined sequence without deviations.Example: Let’s consider a task management system, transitions between states like “To-Do,” “In Progress,” and “Completed” are controlled by task updates and completion criteria.

Example Code in Solidity:

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;

contract TaskManagement {
enum TaskState { ToDo, InProgress, Completed }
TaskState public taskState;
constructor() {
// Initialize the contract with the task in the "To-Do" state
taskState = TaskState.ToDo;
}
modifier onlyInState(TaskState _state) {
require(taskState == _state, "Invalid state transition");
_;
}
function startTask() external onlyInState(TaskState.ToDo) {
// Logic to start the task
taskState = TaskState.InProgress;
}
function completeTask() external onlyInState(TaskState.InProgress) {
// Logic to complete the task
taskState = TaskState.Completed;
}
}

Observation:

The TaskManagement contract represents a task with states “To-Do,” “In Progress,” and “Completed.”The onlyInState modifier ensures that functions like startTask and completeTask are only callable when the task is in the correct state, preventing invalid transitions.This example demonstrates how state transitions can be enforced in a Solidity smart contract, ensuring a systematic flow of states.

Variable Transitions

This verification ensures that variables change consistently, following a specified pattern throughout the system’s life cycle.Some variables should exhibit monotonic behavior, changing in a specific manner (e.g., non-decreasing) as the system progresses.Different variables may have distinct change patterns, with some required to change only in specific directions for the system’s coherence.Example: A variable tracking the number of transactions should be non-decreasing, ensuring accurate and sequential recording of transactions.

Example Code in Solidity:

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;

contract SystemTransaction {
uint256 public totalTransactions;
mapping(address => uint256) public userBalances;
function deposit(uint256 amount) external {
// Logic for deposit operation
totalTransactions++;
userBalances[msg.sender] += amount;
}
// Additional function to illustrate a non-decreasing variable
function getTotalTransactions() external view returns (uint256) {
return totalTransactions;
}
// Additional function to illustrate balance consistency
function getUserBalance(address user) external view returns (uint256) {
return userBalances[user];
}
}

Observation:

The SystemTransaction contract showcases variables like totalTransactions and userBalances.The deposit function increments the totalTransactions variable and increases the balance of the user making the deposit.The additional functions ( getTotalTransactions and getUserBalance ) allow querying the current state of these variables to observe their transitions over time.This example demonstrates how variable transitions can be verified and controlled in a Solidity smart contract, ensuring consistency and adherence to predefined patterns.

High-level Properties

High-level properties focus on the entire system from the users’ viewpoint, ensuring holistic behavior and outcomes.Unlike other property types, high-level properties don’t target specific elements (state, variable, or transition) but aim to cover the entire system’s functionality.High-level properties address the overall user experience, ensuring that users’ interactions result in expected outcomes and that the system behaves coherently.Example: Consider an e-commerce platform, a high-level property might assert that any purchase transaction should deduct the correct amount from the buyer’s account and add it to the seller’s account without creating or destroying assets.

Example Code in Solidity:

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;

contract EbankApp {
mapping(address => uint256) public userBalances;
uint256 public totalFunds;
function deposit(uint256 amount) external {
// Logic for deposit operation
totalFunds += amount;
userBalances[msg.sender] += amount;
}
function transfer(address to, uint256 amount) external {
// Logic for fund transfer
require(userBalances[msg.sender] >= amount, "Insufficient funds");

userBalances[msg.sender] -= amount;
userBalances[to] += amount;
}
// Additional function to illustrate high-level property
function checkFundsLimitation() external view returns (bool) {
return userBalances[msg.sender] <= totalFunds;
}
}

Observation:

The EbankApp contract manages user balances and total funds, simulating a simplified bank system.The deposit function increases the user’s balance and the total funds of the bank.The transfer function allows users to transfer funds between accounts, ensuring that the transfer doesn’t exceed the user’s balance and adheres to the high-level property of limiting individual user balances to the total funds of the bank.The checkFundsLimitation function allows users to query whether their balance complies with the high-level property.

Unit Test:

Unit tests isolate and verify specific functions or portions of code, ensuring they operate correctly.Each unit test targets a distinct functionality, allowing developers to identify and fix issues at a granular level.Unit tests define expected behavior for individual functions, checking if they meet predefined criteria.Example: For a mathematical function, a unit test might check that the function correctly performs operations like addition, subtraction, multiplication, and division under various scenarios.

Example Code in Solidity:

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;

contract MathOperations {
function add(uint256 a, uint256 b) external pure returns (uint256) {
return a + b;
}
function multiply(uint256 a, uint256 b) external pure returns (uint256) {
return a * b;
}
function authenticate(string memory username, string memory password) external pure returns (bool) {
// Simulated authentication logic
return keccak256(abi.encodePacked(username)) == keccak256(abi.encodePacked("exampleUser")) &&
keccak256(abi.encodePacked(password)) == keccak256(abi.encodePacked("examplePassword"));
}
}

Observation:

The MathOperations contract includes functions for addition, multiplication, and authentication.Unit tests for the add and multiply functions would validate that they correctly perform mathematical operations.Another unit test might focus on the authenticate function, confirming its behavior when provided with correct and incorrect credentials.

Contract Function: YourTokenContract.sol

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;

contract YourTokenContract {

uint8 public decimals = 18;
mapping(address => uint256) public balances;
constructor() {
// Assuming some initial tokens are minted to the contract deployer
balances[msg.sender] = 1000000 * (10**decimals);
}
function makeTransaction(uint tokens) public payable {
_validate_transaction(tokens, msg.value);
_mint(msg.sender, tokens);
}
function _mint(address recipient, uint tokens) internal {
// Mint the specified number of tokens to the recipient
balances[recipient] += tokens;
}
function _validate_transaction(uint desired_tokens, uint wei_sent) internal view {
uint required_wei_sent = (desired_tokens / 10) * decimals;
require(wei_sent >= required_wei_sent, "Insufficient Ether sent for the desired tokens");
}

}

Invariant Scenario(template.sol): If wei_sent is zero, desired_tokens must be zero

// SPDX-License-Identifier: AGPL-3.0
pragma solidity ^0.8.0;
import "./YourTokenContract.sol";

contract TestYourTokenContract is YourTokenContract {
// Now we are in a state where the test contract is no longer the owner of the system.
function assert_no_free_tokens(uint desired_amount) public {
require(desired_amount > 0);
_validate_transaction(desired_amount, 0);
assert(false); // this should never be reached.
}
}

Target Contract: YourTokenContract.sol

YourTokenContract.sol contains the main functionality related to token transactions. It includes the makeTransaction function, which is responsible for validating and minting tokens based on the provided parameters.

Test Contract Code: TestYourTokenContract.sol

TestYourTokenContract.sol is a testing contract specifically designed to test the assert_no_free_tokens function in YourTokenContract.sol. It creates an instance of YourTokenContract and includes a test case for the assert_no_free_tokens function.

Echidna Version:

Terminal Command to Run:

echidna template.sol - contract TestYourTokenContract - test-mode assertion

Output:

Observation:

In the example contract function makeTransaction, we simulate a token transaction scenario. The internal function _validate_transaction ensures that the transaction adheres to certain rules, such as validating the amount of Ether sent against the desired number of tokens. Specifically, it checks if the sent Ether is equal to or exceeds the calculated required amount based on the desired tokens.

Let’s examine the invariant scenario we want to test: If wei_sent is zero, desired_tokens must be zero. This means that if no Ether is sent in the transaction, the desired number of tokens should be zero as well. To enforce this invariant, we’ve created the function assert_no_free_tokens. In this function, we first ensure that desired_amount is greater than zero, as it represents the fuzzable value set by Echidna. We then invoke the _validate_transaction function with the given desired_amount and zero for wei_sent. Finally, we add an assert(false) statement, ensuring this line is never reached, as the invariant should hold.

When Echidna runs the test, it explores various scenarios, including cases where no Ether is sent (wei_sent is zero), and evaluates whether the desired tokens are appropriately set to zero in such instances. If the invariant is violated, the assert(false) statement is triggered, indicating a failure in upholding the specified condition. This process allows developers to identify and rectify potential vulnerabilities related to the relationship between the amount of Ether sent and the desired tokens in the smart contract.

Properly initializing systems for fuzzing is crucial. Whether through simple or complex initialization procedures, developers must ensure that the smart contract environment is conducive to thorough testing.Invariants serve as the foundation of smart contract security. Crafting them involves starting with clear English statements, translating them into Solidity, and iteratively testing them using Echidna.The fuzzing process is iterative. Define invariants, write them in Solidity, and run Echidna. If invariants break, investigate and refine. Continuous improvement is key to enhancing the security of smart contracts.Echidna retains tests through coverage tracking, corpus management, educated fuzzing decisions, mutation techniques, splicing for diversity, and smart randomness. This ensures that the fuzzer builds on previous tests to explore new and potentially vulnerable areas of the code.

developers armed with a solid understanding of invariants and the capabilities of Echidna can significantly enhance the security posture of their smart contracts. By embracing a proactive and iterative approach, they can identify and rectify vulnerabilities, fostering the development of robust and secure blockchain solutions.

Securing smart contracts is a critical undertaking, and the establishment of robust invariants is a key element in this process. Echidna, with its automated testing capabilities, provides developers with a powerful tool to ensure the integrity and security of Ethereum contracts. Through this guide, we’ve navigated the process of crafting solid invariants, initializing systems for effective fuzzing, and leveraging Echidna’s features to their full potential.

Sign up today to stay informed about the newest trends in smart contract security

For more information: https://web3secnews.substack.com