Learning CVL Language (Part 4)

Formal verification is critical for ensuring smart contract security. Certora Verification Language (CVL) provides powerful tools for this task, with ghost variables and storage hooks being especially useful for tracking contract state and proving complex properties. Let's explore how these mechanisms work and examine practical examples.

Ghost Variables: Tracking State Beyond the Contract

Ghost variables in CVL behave like contract storage but are only visible within specifications. They offer several advantages:

• They revert when storage reverts

• They can be assigned specific values after contract construction

• They can be directly accessed from the specification (read/write)

• They provide a way to track state that isn't explicitly stored in the contract

ghost mathint numVoted;
ghost mapping(address => uint256) balanceGhost;

Setting Initial State

Ghost variables can have their initial values set using the init_state axiom syntax:

ghost mathint someGhost {
  init_state axiom someGhost == 0;
}

This ensures the condition is true immediately after the constructor executes. The expression cannot contain calls to Solidity functions.

Storage Hooks: Responding to State Changes

Storage hooks inject CVL code whenever a storage variable is accessed, whether for reading or writing. One common use is updating ghost variables in response to contract state changes:

hook Sstore _hasVoted[KEY address voter] bool newVal (bool oldVal) {
  numVoted = numVoted + 1;
}

here whenever a sstore is made on the _hasVoted mapping of the contract we are formally verificating, it will increment our ghost variable numVoted.

Practical Applications

Tracking Votes in a Voting Contract

Consider a simple voting contract that tracks who has voted and counts votes in favor or against a proposal:

contract Voting {
  mapping(address => bool) internal _hasVoted;
  uint256 public votesInFavor;
  uint256 public votesAgainst;
  uint256 public totalVotes;

  function vote(bool isInFavor) public {
    require(!_hasVoted[msg.sender]);
    _hasVoted[msg.sender] = true;
    totalVotes += 1;
    if (isInFavor) {
      votesInFavor += 1;
    } else {
      votesAgainst += 1;
    }
  }
}

Using a ghost variable and a hook, we can track every change to the _hasVoted mapping:

ghost mathint numVoted {
  init_state axiom numVoted == 0;
}

hook Sstore _hasVoted[KEY address voter] bool newVal (bool oldVal) {
  if (!oldVal && newVal) {
    numVoted = numVoted + 1;
  }
}

invariant sumResultsEqualsTotalVotes()
  to_mathint(totalVotes()) == numVoted;

This verification ensures that totalVotes accurately reflects the number of people who have voted.

Verifying Bid Integrity in Auctions

For an English auction contract, we can prove that the highest bid is strictly greater than all other bids:

ghost bool _hasAnyoneBid {
  init_state axiom !_hasAnyoneBid;
}

hook Sstore bids[KEY address bidder] uint newAmount (uint oldAmount) {
  _hasAnyoneBid = _hasAnyoneBid || (newAmount > 0);
}

invariant highestBidStrictlyHighest(address bidder)
  (_hasAnyoneBid && bidder != highestBidder()) => (highestBid() > bids(bidder));

Verifying Fund Manager Relationships

In a fund management system, we can verify that every active manager is associated with a fund:

ghost mapping(address => uint256) managersFunds;

hook Sstore funds[KEY uint256 fundId].(offset 0) address newManager {
  managersFunds[newManager] = fundId;
}

invariant activeManagesAFund(address manager)
  isActiveManager(manager) => getCurrentManager(managersFunds[manager]) == manager;

Testing Your Specifications

Certora provides Gambit, a tool that automatically generates random mutations (bugs) in the code to test the coverage of your specifications. This helps ensure your rules catch potential issues:

certoraRun Voting.conf

Why This Matters

Ghost variables and hooks provide several key benefits for formal verification:

1. They allow tracking state transitions that may not be explicitly stored in the contract

2. They enable concise expression of complex properties about contract behavior

3. They help maintain invariants across contract execution

4. They connect different aspects of contract state for comprehensive verification

By combining ghosts and hooks, you can create powerful specifications that detect subtle bugs and provide strong guarantees about contract behavior.

These verification techniques are essential for mission-critical smart contracts where security failures could lead to significant financial losses.