How can we make sure Web3 applications are more secure? Is there anything Web3 developers can do to make it easier to check their code? At Certora, we use a technique called formal verification to secure smart contracts and we have found that certain best practices when developing smart contracts can make it easier to formally verify code thereby making it more secure.

Formal verification is a technique for proving that a program behaves according to a specification. It is based on mathematical logic. Formal verification can be used in smart contracts to prove the absence of certain kinds of security vulnerabilities. This is important for decentralized finance applications where a lot of money is at stake and malicious attackers can take advantage of security loopholes to cause severe financial losses. We have developed the Certora Prover which is an open-source formal verification tool that targets security of smart contracts for blockchains like Stellar, Solana, and Ethereum.

Our experience formally verifying Rust smart contracts for Soroban and Solana has helped us identify what makes a Rust smart contract easy or difficult to verify. This blog post shares five best practices distilled from our observations to help Web3 developers write Rust smart contracts that are not only secure and readable, but also verifiable. 

Here is a short summary of the five best practices.

1. Keep Code Modular: break large functions into smaller components.
2. Use compiler’s exhaustiveness checks: be careful using wildcards when pattern matching.
3. Prefer simple data structures: use simple, flat data structures over ones with hashing behavior when possible.
4. Fewer states with trap values: design data types that make it impossible to have illegal states.
5. Separate core logic from effects: isolate pure logic from effectful operations and events.

Read along to see concrete examples illustrating them!

1. Keep Code Modular

It is well-known that modularity is a good software engineering practice as it makes code more readable and common components reusable. It turns out that modular code is also easier to verify! Splitting overly monolithic functions into smaller ones allows verification tools to reason about each piece independently. This not only improves readability but also makes specifications simpler and reusable.

Bad Example:

pub fn process_user_ops(
  env: &Env,
  protocol: &mut Protocol,
  user: &Address,
  op: UserOp
) -> bool {
    let mut state = UserState::load(env, user);
    let mut check_needed = false;

    match op.kind {
        OpType::Deposit => {
            let vault = protocol.get_vault(&op.asset);
            state.balance += op.amount;
            protocol.transfer_from_user(env, user, &vault, op.amount);
        }
        OpType::Withdraw => {
            let vault = protocol.get_vault(&op.asset);
            if state.balance >= op.amount {
                state.balance -= op.amount;
                protocol.transfer_to_user(env, user, &vault, op.amount);
            }
        }
        OpType::Borrow => {
            let market = protocol.get_market(&op.asset);
            state.debt += op.amount;
            protocol.transfer_to_user(env, user, &market, op.amount);
            check_needed = true;
        }
        OpType::Repay => {
            let market = protocol.get_market(&op.asset);
            let payment = op.amount.min(state.debt);
            state.debt -= payment;
            protocol.transfer_from_user(env, user, &market, payment);
        }
    }

    state.save(env, user);
    check_needed
}

Here, a single dispatcher-like method has all the logic for handling each type of user operation. This makes it difficult to write invariants and other properties for each operation separately.

Good example:

pub fn process_user_ops(
  env: &Env,
  protocol: &mut Protocol,
  user: &Address,
  op: UserOp
) -> bool {
    let mut user_state = UserState::load(env, user);
    let mut check_needed = false;

    match op.kind {
        OpType::Deposit => {
            handle_deposit(env, protocol, user, &mut user_state, &op);
        }
        OpType::Withdraw => {
            handle_withdraw(env, protocol, user, &mut user_state, &op);
        }
        OpType::Borrow => {
            handle_borrow(env, protocol, user, &mut user_state, &op);
            check_needed = true;
        }
        OpType::Repay => {
            handle_repay(env, protocol, user, &mut user_state, &op);
        }
    }

    user_state.save(env, user);
    check_needed
}

fn handle_deposit(
    env: &Env,
    protocol: &mut Protocol,
    user: &Address,
    state: &mut UserState,
    op: &UserOp,
) {
    let vault = protocol.get_vault(&op.asset);
    state.balance += op.amount;
    protocol.transfer_from_user(env, user, &vault, op.amount);
}

...

In this example, each operation has a separate handler and therefore can be specified and verified more easily.

2. Rely on the Compiler’s Exhaustiveness Checks Whenever Possible

Let’s refer to the above scenario of user operations again and consider the following OpType enum that has 4 variants and a function that checks whether an operation increases the user’s funds:

pub enum OpType {
    Deposit,
    Withdraw,
    Borrow,
    Repay
}

pub fn increases_user_funds(env: &Env, op: UserOp) -> bool {
    match op.kind {
      	OpType::Withdraw => true,
     	OpType::Borrow => true,
      	_ => false
    }
}

This code relies on the wildcard (_) to indicate that only Withdraw and Borrow can increase funds, and in all other cases, it must return false. But what happens when the enum is later changed to add another variant (e.g., Redeem), which also increases the user’s funds?

This way of writing the code has the risk that the developer can easily forget to change increases_user_funds to handle the new case. Now say that the developer has a property that checks that increases_user_funds returns true for the Redeem case. The property will fail in this scenario and the developer will end up spending extra time debugging the cause of failure, ultimately fixing the code.

All of this can be avoided by writing the code in a way that requires relying on the Rust compiler’s exhaustiveness check, which prevents the code from compiling without handling all the scenarios:

pub fn increases_user_funds(env: &Env, op: UserOp) -> bool {
    match op.kind {
      	OpType::Withdraw | OpType::Borrow => true,
      	OpType::Deposit | OpType::Repay => false,
    }
}

Now, when a new variant is added, the developer will be forced to think carefully and handle it the right way.

3. Use Simpler Data Structures When Possible

Think carefully before resorting to complex data structures like HashSet or BTreeMap. Does the workload really need it? They are tempting to use but reasoning about heap allocated data structures and hash functions is hard. When possible, it is best to use simpler, linear structures.

To show a concrete example, consider a function that checks whether a given Address is unique by looking through a small number of existing addresses. In this case, a linear scan of addrs suffices and is fast enough in practice for up to tens of elements and much easier to verify than code with hashing behavior.

fn is_unique (addrs: &Vec<Address>, addr: &Address) -> bool {
    !addrs.contains(addr)
} // worth using a Vec over a hashed data structure when addrs is a small collection

An associative map, sorted by the keys, is preferable even when the collection is big but does not require too many insertions. Of course there are workloads where hashed data structures are more efficient but smart contracts are often short lived and operate on small datasets. In these settings, the humble association list (a flat map) performs better and is also much easier for verification.

4. Minimize States with Trap Values by Construction

Sometimes, we end up with “flat” user-defined data types that have too many fields that can hold a “trap value” (e.g.,  None). These can be hard to keep track of, especially when one field has a “trap value” that affects what other fields may or may not be allowed to have a “trap value”. It requires the developer to think carefully about all the combinations and make sure that the program cannot be in a state where some optional field is wrongly left as None or allowed to be Some(...).

Bad example:

pub struct LoanPosition {
    pub user: Address,
    pub collateral_amount: Option<u64>,
    pub borrowed_amount: Option<u64>,
    pub liquidation_price: Option<u64>,
    pub interest_accrued: Option<u64>,
    pub closed_at: Option<Time>,
    pub status: LoanStatus,
}

pub enum LoanStatus {
    Open,
    InLiquidation,
    Closed,
}

Here, the fields collateral_amount, borrowed_amount, and interest_accrued don’t make sense for Closed loans. Similarly, closed_at only makes sense for Closed loans. This system design allows illegal states where status can be Closed, but borrowed_amount is Some(num) which should not be allowed.

Another way to design the system is shown below:

Good example:

pub struct LoanPosition {
    pub user: Address,
    pub state: LoanState,
}

pub enum LoanState {
    Open {
        collateral_amount: u64,
        borrowed_amount: u64,
        interest_accrued: u64,
        liquidation_price: u64,
    },
    InLiquidation {
        collateral_amount: u64,
        borrowed_amount: u64,
    },
    Closed {
        closed_at: Time
    }
}

Now, an Open loan must have the borrowed_amount field, and a Closed loan can only have a closed_at field. This approach makes the code easier to verify because there are fewer illegal states that the specification needs to worry about.

Developers should note, however, that there is a tradeoff between the choice of value representation and the ease of serialization and deserialization. Finally, using marker traits like AnyBitPattern or Pod (from the bytemuck crate) can also affect design decisions.

5. Separate Pure Logic from Effects and Error Handling

Code that mixes the core logic of a protocol with error handling code, effectful code (e.g., storage I/O), and event emissions poses a challenge for reasoning and verification. Separating out pure computations allows verification tools to focus on the logical behavior without tracking complex control flow.

This allows the pure functions to be verified on their own, with relatively more reusable properties, while the effectful parts can be verified for side-effect related properties and panic safety.

Bad Example:

pub fn borrow(env: &Env, protocol: &mut Protocol, user: &Address, amount: u64) {
    let mut account = Account::load(env, user);
    let market = protocol.get_market();
    let new_debt = account.debt + amount;

    if new_debt > market.max_borrow {
        panic_with_error!(env, Error::LimitExceeded);
    }

    account.debt = new_debt;
    protocol.transfer_to_user(env, user, &market.token, amount);
    env.events().publish(("borrow", user.clone()), amount);
    account.save(env, user);
}

This function mixes several different types of tasks: loading the state, computing the debt, error handling, the effectful operation of transferring the amount, and event emission.

Good Example:

pub fn borrow(env: &Env, protocol: &mut Protocol, user: &Address, amount: u64) {
    let mut account = Account::load(env, user);
    let market = protocol.get_market();

    match compute_borrow(account.debt, amount, market.max_borrow) {
        Ok(new_debt) => {
            account.debt = new_debt;
            protocol.transfer_to_user(env, user, &market.token, amount);
            env.events().publish(("borrow", user.clone()), amount);
            account.save(env, user);
        }
        Err(e) => panic_with_error!(env, e),
    }
}

fn compute_borrow(current_debt: u64, amount: u64, max: u64) -> Result<u64, Error> {
    let new_debt = current_debt + amount;
    if new_debt > max {
        Err(Error::LimitExceeded)
    } else {
        Ok(new_debt)
    }
}

In this version, the pure logic is separated into its own function, making it easier to write properties that check the logic itself. The wrapper function borrow is responsible for calling compute_borrow and handling effectful I/O operations and exceptions. 

This can also be generalized and applied at the contract level. For example, having a minimal contract that has the core protocol logic and a “wrapper” contract that has auxiliary logic that is not central to the protocol’s core functionality (e.g., interfacing, authorization, etc.,) makes it easy to verify the critical components in isolation.

Verification-Friendly Code is also Developer-Friendly Code

Writing smart contracts with verification in mind leads to code that is not only safer, but also easier to understand, test, and maintain. The act for writing a formal specification also helps with software design and documentation. It can be a useful tool for exposing inconsistencies in specifications and inefficient implementations.

The suggestions here not only make code easier to verify, but also more amenable to testing and fuzzing. For example, separating the core logic from effectful components makes it easier to use techniques like property-based testing to focus on checking that the main logic is correct without worrying about additional infrastructure (like spinning up a virtual machine) for testing the entire program. Clearly defined interfaces make techniques like fuzzing more effective by avoiding irrelevant inputs and focusing on generating only meaningful ones.

While the list we present here is certainly not exhaustive, we hope that these simple best practices help developers improve the long-term quality and reliability of their smart contracts.

References

• Stellar Foundation documentation on security best practices: https://developers.stellar.org/docs/build/security-docs
• A great video from JaneStreet’s Yaron Minsky, which inspired some of the ideas here: https://www.youtube.com/watch?v=-J8YyfrSwTk
• Blog from OpenZeppelin on secure Solidity development: https://www.openzeppelin.com/readiness-guide#code-clarity

Acknowledgements

Thanks to Arie Gurfinkel and Alexander Bakst for valuable feedback on the content!