A Guide to Crafting Robust Invariants

Thinking about invariant types can be useful, as it allows you to expand upon the common and most obvious properties of your protocol.

In this guide, we will present some tips and tricks for creating robust invariants.

1. How to Define Good Invariants?

Defining good invariants usually begins with the process of characterizing clear and concise system properties in plain English. These will later be translated into Solidity for effective testing. Finally, after running a fuzzer or formal verification tool, an iterative process is used to break these invariants and investigate the issues to fix bugs and improve the codebase.

2. Types of Invariants

Thinking about invariant types can be useful, as it allows you to expand upon the common and most obvious properties of your protocol. Sometimes, invariants can be directly extracted from the code or the system specification. Other times, it is necessary to think more abstractly about which properties should hold. These categories can aid in this process, as they allow for a repeatable methodology that can be used to expand the list of invariants to test against the system.

2.1. Functional-level Invariants:

1. These invariants are stateless and can be tested in isolation.

2. Example: Associative property of addition in a contract.

3. How: Inherit the target contract, create a function, call the targeted function, and use "assert" to check the property.
   
   

Example Code:

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

2.2. System-level Invariants

1. High-level properties focus on the entire system.

2. These invariants are usually stateful.

3. Unlike other property types, high-level properties don't target specific elements, but aim to cover the entire system's functionality.

4. 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 both 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 lets users query whether their balance complies with the high-level property.

2.3. Valid States

1. Valid states are the translation of the program's state machine into reachable paths. 

2. They play a crucial role in preventing unwanted states.

3. 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 platformLogout() 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.
  
  

2.4. State Transitions

1. State transitions ensure changes occur in the correct order and conditions, maintaining the integrity of the system's state machine.

2. Transitions are verified to occur only against specific function calls, variable values, or elapsed time, preventing undesired state changes.

3. The correctness of transitions guarantees a systematic state machine, where each change follows the predefined sequence without deviations.

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

2.5. Variable Transitions

1. This verification ensures, similarly to state transitions, that variables change consistently.

2. Some variables should exhibit monotonic behavior, changing in a specific manner (e.g., non-decreasing) as the system progresses.

3. Different variables may have distinct change patterns, with some required to change only in specific directions for the system's coherence.

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

2.6. Unit Test

1. Unit tests isolate and verify specific functions or portions of code, ensuring they operate correctly.

2. Each unit test targets a distinct functionality, allowing developers to identify and fix issues at a granular level.

3. Unit tests define expected behavior for individual functions, checking if they meet predefined criteria.

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

Key Takeaways:

• 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 a fuzzer such as Echidna.

• The fuzzing process is iterative. Define invariants, write them in Solidity, and run a fuzzer such as Echidna. If invariants break, investigate and refine. Continuous improvement is key to enhancing the security of smart contracts.

• Functional-level invariants, which are stateless and can be tested in isolation, and system-level invariants, which rely on the deployment of the entire system, should be considered based on the specific requirements of the smart contract.

Was it useful? Help us to improve!

With your feedback, we can improve the letter. Click on a link to vote:

• 👍 That helped me. Thanks

• 😐 Meh - was ok.

• 👎 Not interesting to me.