Assertion Guide

Introduction

The Credible Layer is a security prevention framework that helps protect smart contracts by continuously verifying critical protocol invariants.

This guide assumes that you have already installed the Credible Layer. If you haven’t, please see the Credible Layer Quickstart for instructions.

For a visual learners a video introduction to assertions is available:

We will use a simple ownership protocol as an example that demonstrates how to protect against unauthorized ownership transfers - a critical security concern in smart contracts.

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

// Do not use this in production, it is just an example!!!
contract Ownable {
    address private _owner;

    event OwnershipTransferred(address indexed previousOwner, address indexed newOwner);

    constructor() {
        _owner = address(0xdead);
        emit OwnershipTransferred(address(0), _owner);
    }

    modifier onlyOwner() {
        require(_owner == msg.sender, "Ownable: caller is not the owner");
        _;
    }

    // Get the current owner
    function owner() public view returns (address) {
        return _owner;
    }

    // Transfer ownership to a new address
    // Can only be called by the current owner
    function transferOwnership(address newOwner) public onlyOwner {
        require(newOwner != address(0), "Ownable: new owner is the zero address");
        emit OwnershipTransferred(_owner, newOwner);
        _owner = newOwner;
    }
}

In the above code, we have a simple contract that manages ownership transfers. While ownership transfer functionality is common in protocols, it should be carefully controlled since unauthorized changes can be catastrophic. For example, in 2024, Radiant Capital lost $50M when an attacker gained access to their multisig and changed the protocol owner.

To prevent such incidents, we can write an assertion that guards ownership changes. The assertion will block transactions if ownership changes unexpectedly, though it can be temporarily paused when legitimate ownership transfers are planned.

Our assertion will verify that the contract owner remains unchanged after each transaction.

1. Setting Up Your Project

For detailed instructions on setting up your Credible Layer project structure, please refer to the Credible Layer Quickstart Guide.

Alternatively, you can quickly get started by cloning the Credible Layer starter repository:

git clone --recurse-submodules https://github.com/phylaxsystems/credible-layer-starter 
cd credible-layer-starter

This repository includes the necessary file structure, dependencies, and configuration for writing and testing assertions.

2. Writing the Assertion

Let’s create our assertion in OwnableAssertion.a.sol. Here’s the complete code first, followed by a detailed breakdown:

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

import {Assertion} from "credible-std/Assertion.sol";
import {Ownable} from "../../src/Ownable.sol"; // Ownable contract

contract OwnableAssertion is Assertion {
    Ownable public ownable;

    // The triggers function tells the Credible Layer which assertion functions to run
    // This is required by the Assertion interface
    function triggers() external view override {
        // Register our assertion function to be called when transferOwnership is called
        registerCallTrigger(this.assertionOwnershipChange.selector, Ownable.transferOwnership.selector);
    }

    // This assertion checks if ownership has changed between pre and post transaction states
    function assertionOwnershipChange() external {
        // Get the adopter contract address using the cheatcode
        // This can be done instead of using the constructor and
        // is less error prone while storing and submitting the assertion
        ownable = Ownable(ph.getAssertionAdopter());

        // Create a snapshot of the blockchain state before the transaction
        ph.forkPreState();

        // Get the owner before the transaction
        address preOwner = ownable.owner();

        // Create a snapshot of the blockchain state after the transaction
        ph.forkPostState();

        // Get the owner after the transaction
        address postOwner = ownable.owner();

        // Assert that the owner hasn't changed
        // If this requirement fails, the assertion will revert
        require(postOwner == preOwner, "Ownership has changed");
    }
}

How Assertions Work

The key principle of assertions is simple: if an assertion reverts, it means the assertion failed and an undesired state was detected. In our case, the assertion will revert if the contract’s owner changes, allowing us to prevent unauthorized ownership transfers.

If an assertion reverts, the transaction resulting in the undesired state is reverted and not included in the block. This results in actual hack prevention, not just mitigation.

Gas Consumption

Assertion functions are limited to a maximum execution of 100,000 gas. If an assertion function exceeds this gas limit, the transaction will be invalidated and dropped. Please be aware that the gas consumption of certain cheatcodes, such as getCallInputs, can be variable, due to unknown lengths of the call inputs. We are actively working to improve this as soon as possible. Staying mindful of gas consumption is in general a good practice. See the Assertion Patterns for more details on ways to optimize gas consumption.

Anatomy of the Assertion

Let’s break down the key components of our assertion:

1. Imports and Contract Definition

import {Assertion} from "credible-std/Assertion.sol";
import {Ownable} from "../../src/Ownable.sol";

contract OwnableAssertion is Assertion {

The contract inherits from Assertion, which provides the base functionality and cheatcodes for assertions
We import the contract we want to protect (Ownable)

2. State Variables and Constructor

Ownable public ownable;

// Optional constructor
constructor() {}

State variables store the address of contract the assertion is protecting
The ph.getAssertionAdopter() cheatcode is used to get the address of the contract the assertion is protecting and provided the most flexibility.
If you are defining other state variables your assertion should know about this can be done in the constructor.
The constructor is optional and can be initialized during the storing and submitting of the assertion through the pcl.
The constructor runs against an empty state. This means you can pass values in the constructor but you can not read values from other contracts.
Storage that is set in the constructor persists in the assertion contract.
Cheatcodes/precompiles are not accessible in the constructor.
You can hardcode the address of the contract you want to protect in the assertion contract, but this is not a flexible or recommended approach.

3. Triggering Assertions

// The triggers function tells the Credible Layer which assertion functions to run and when to run them
// This is required by the Assertion interface
function triggers() external view override {
    // Register our assertion function to be called when transferOwnership is called
    registerCallTrigger(this.assertionOwnershipChange.selector, Ownable.transferOwnership.selector);
}

The triggers function is required by the Assertion interface.
Each assertion function must be registered here via its function selector.
Multiple assertions can be defined in a single contract.
registerCallTrigger specifies the function selector of the assertion function to run and the function selector of the protected contract function that should trigger the assertion.
A trigger can only trigger one assertion function.
Use triggers to make sure that assertions are only called when they are needed in order to save gas and resources.
The Credible Layer supports different trigger types. See the “Triggers” section in the cheatcodes documentation for more information.

4. Assertion Logic

// This assertion checks if ownership has changed between pre and post transaction states
function assertionOwnershipChange() external {
    // Get the adopter contract address using the cheatcode
    // This can be done instead of using the constructor and
    // is less error prone while storing and submitting the assertion
    ownable = Ownable(ph.getAssertionAdopter());

    // Create a snapshot of the blockchain state before the transaction
    ph.forkPreState();

    // Get the owner before the transaction
    address preOwner = ownable.owner();

    // Create a snapshot of the blockchain state after the transaction
    ph.forkPostState();

    // Get the owner after the transaction
    address postOwner = ownable.owner();

    // Assert that the owner hasn't changed
    // If this requirement fails, the assertion will revert
    require(postOwner == preOwner, "Ownership has changed");
}

The main assertion logic uses cheatcodes:
- ph.forkPreState(): Creates a snapshot of the blockchain state before the transaction.
- ph.forkPostState(): Creates a snapshot of the blockchain state after the transaction.
The assertion reverts if the condition is not met. You can have several require checks in the same function to make sure no rules are violated.
The ph namespace gives access to the Credible Layer cheatcodes, which provide utility functions for assertions. For more information see the cheatcodes documentation.
All assertion functions must be public or external to be callable by the Credible Layer.

Best Practices for Writing Assertions

Single Responsibility: Each assertion should verify one specific property or invariant.
- Sometimes it makes sense to check multiple properties in the same assertion function.
- Aim to have as many specific assertion functions as possible, since the Credible Layer executes assertions in parallel.
State Management: Use forkPreState() and forkPostState() to compare values before and after transactions.
Gas Optimization: Use triggers to make sure that assertions are only called when they are needed in order to save gas and resources.
Return Early: When writing more complex assertions checking multiple function calls in the callstack, it is recommended to check basic invariants first before starting to iterate over the callstack.

3. Testing the Assertion

Testing assertions is a critical step in developing effective security prevention. Since assertions act as automated guardians for your protocol, it’s essential to verify they correctly identify both safe and unsafe conditions. A false positive could unnecessarily block legitimate protocol operations, while a false negative could miss critical security violations.

To run the tests, you can use the following command:

pcl test

Good assertion tests should:

Verify that assertions fail when they should (e.g., when detecting unauthorized changes)
Confirm that assertions pass during normal operation
Simulate realistic protocol interactions

Let’s break down how to test our assertion:

Test Imports

import {OwnableAssertion} from "../src/OwnableAssertion.a.sol";
import {Ownable} from "../../src/Ownable.sol";
import {CredibleTest} from "credible-std/CredibleTest.sol";
import {Test} from "forge-std/Test.sol";

Let’s examine each import:

OwnableAssertion: This imports the assertion we created that we want to test
Ownable: Imports the protocol contract that our assertion is protecting
CredibleTest: Provides special testing utilities for assertion testing, including the cl cheatcode interface
Test: Standard testing base contract from Forge, providing utilities like vm.prank and vm.expectRevert

These imports provide all the necessary components to test our assertion effectively, including access to both the assertion logic and the protocol being protected.

Test Contract Structure

contract TestOwnableAssertion is CredibleTest, Test {
    // Contract state variables
    Ownable public assertionAdopter;
    address public initialOwner = address(0xf00);
    address public newOwner = address(0xdeadbeef);

Inherits from CredibleTest and Test which provides testing utilities
CredibleTest provides the cl cheatcode interface for testing assertions
Test is the standard Forge test base contract
assertionAdopter is the contract we’re protecting
newOwner is used to test ownership transfers
initialOwner is the owner of the contract before the tests are run

Setup

// Set up the test environment
function setUp() public {
    assertionAdopter = new Ownable(initialOwner);
    vm.deal(initialOwner, 1 ether);
}

Creates a new instance of the Ownable contract for testing
Gives the owner some ETH using Forge’s vm.deal
This setup runs before each test function

Testing Assertion Reverted

This test checks that the assertion reverts when ownership changes.

// Test case: Ownership changes should trigger the assertion
function test_assertionOwnershipChanged() public {
    address aaAddress = address(assertionAdopter);
    string memory label = "OwnableAssertion";

    // Associate the assertion with the protocol
    // cl will manage the correct assertion execution when the protocol is called
    cl.addAssertion(label, aaAddress, type(OwnableAssertion).creationCode, abi.encode(assertionAdopter));

    // Simulate a transaction that changes ownership
    vm.prank(initialOwner);
    vm.expectRevert("Assertions Reverted");
    cl.validate(
        label, aaAddress, 0, abi.encodePacked(assertionAdopter.transferOwnership.selector, abi.encode(newOwner))
    );
}

Key components:

cl.addAssertion(): Links the assertion to the contract being protected
- First argument: Label of the assertion (use the name of the assertion you are testing)
- Second argument: Address of contract to protect
- Third argument: Bytecode of the assertion contract
- Fourth argument: Constructor argument(s) for the assertion
vm.prank(): Simulates a call from the owner’s address
vm.expectRevert(): Expects the assertion to revert with “Assertions Reverted” (only current error message)
cl.validate(): Run a transaction against the assertion. If the assertion reverts, the transaction will be reverted and not included in the block.
- First argument: Label of the assertion (use the name of the assertion you are testing)
- Second argument: Address of contract to call the function on
- Third argument: ETH value (0 in this case)
- Fourth argument: Encoded function call to the protected contract (transferOwnership in this case)

cl is the cheatcode exposed by the CredibleTest contract used specifically for testing assertions. It provides tools to validate your assertions under different conditions without having to deploy them to a real blockchain.

Testing Assertion Success

// Test case: No ownership change should pass the assertion
function test_assertionOwnershipNotChanged() public {
    address aaAddress = address(assertionAdopter);
    string memory label = "OwnableAssertion";

    cl.addAssertion(label, aaAddress, type(OwnableAssertion).creationCode, abi.encode(assertionAdopter));

    // Simulate a transaction that doesn't change ownership (transferring to same owner)
    vm.prank(initialOwner);
    cl.validate(
        label, aaAddress, 0, abi.encodePacked(assertionAdopter.transferOwnership.selector, abi.encode(initialOwner))
    );
}

Similar to the failing test, but tests the case where no ownership change occurs.
Uses transferOwnership to the same owner to simulate a transaction that doesn’t change the state in ways that violate our assertion
cl.validate() will not revert if the assertion passes so we don’t need to use vm.expectRevert()

Full Test Contract

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

import {OwnableAssertion} from "../src/OwnableAssertion.a.sol";
import {Ownable} from "../../src/Ownable.sol";
import {CredibleTest} from "credible-std/CredibleTest.sol";
import {Test} from "forge-std/Test.sol";

contract TestOwnableAssertion is CredibleTest, Test {
    // Contract state variables
    Ownable public assertionAdopter;
    address public initialOwner = address(0xf00);
    address public newOwner = address(0xdeadbeef);

    // Set up the test environment
    function setUp() public {
        assertionAdopter = new Ownable(initialOwner);
        vm.deal(initialOwner, 1 ether);
    }

    // Test case: Ownership changes should trigger the assertion
    function test_assertionOwnershipChanged() public {
        address aaAddress = address(assertionAdopter);
        string memory label = "Ownership has changed";

        // Associate the assertion with the protocol
        // cl will manage the correct assertion execution when the protocol is called
        cl.addAssertion(label, aaAddress, type(OwnableAssertion).creationCode, abi.encode(assertionAdopter));

        // Simulate a transaction that changes ownership
        vm.prank(initialOwner);
        vm.expectRevert("Assertions Reverted");
        cl.validate(
            label, aaAddress, 0, abi.encodePacked(assertionAdopter.transferOwnership.selector, abi.encode(newOwner))
        );
    }

    // Test case: No ownership change should pass the assertion
    function test_assertionOwnershipNotChanged() public {
        string memory label = "Ownership has not changed";
        address aaAddress = address(assertionAdopter);

        cl.addAssertion(label, aaAddress, type(OwnableAssertion).creationCode, abi.encode(assertionAdopter));

        // Simulate a transaction that doesn't change ownership (transferring to same owner)
        vm.prank(initialOwner);
        cl.validate(
            label, aaAddress, 0, abi.encodePacked(assertionAdopter.transferOwnership.selector, abi.encode(initialOwner))
        );
    }
}

Key Testing Concepts

Assertion Registration: Use cl.addAssertion() to register assertions with contracts
Transaction Simulation: Use cl.validate() to test how assertions respond to transactions
State Manipulation: Use Forge’s cheatcodes (vm.prank, vm.deal) to set up test scenarios
Verification: Use vm.expectRevert() to verify that the assertion reverts when expected
Labeling: Use the name of the assertion you are testing as the label for improved feedback in logs

Running the Tests

pcl test

Conclusion

Assertions provide a powerful mechanism for protecting your protocol’s state and preventing security violations in real-time. By implementing well-designed assertions, you can:

Enhance Security: Block unauthorized changes to critical protocol parameters
Eliminate Risk: Prevent potential exploits before any damage occurs
Build Trust: Demonstrate to users that your protocol is actively protected
Sleep Better: Know that your protocol has an active defense layer

The simple ownership assertion we built in this guide demonstrates just one application. In practice, you might want to secure more complex invariants, such as:

Total supply of tokens should never increase unexpectedly
Funds should never be withdrawn without proper authorization
Key protocol parameters should only change through governance
Protocol reserves should always be sufficient to cover liabilities
Transaction values should never exceed the protocol’s limits
Voting power recorded during snapshot should match the actual voting power
Deviation of the price of a token from the oracle should never exceed a certain threshold
And many more…

By following the best practices outlined in this guide, you can create assertions that are both effective and easy to maintain. Remember to test thoroughly, optimize for gas efficiency, and focus on the most critical aspects of your protocol.

What’s Next?

Explore the assertion examples in the Assertions Book
Learn about the Cheatcodes
Follow the PCL Quickstart to learn how to deploy your assertions
For a comprehensive list of terms and concepts used in PCL, see the Glossary.

Getting Started

Credible Layer

Use Case Mapping

Introduction

1. Setting Up Your Project

2. Writing the Assertion

How Assertions Work

Gas Consumption

Anatomy of the Assertion

1. Imports and Contract Definition

2. State Variables and Constructor

3. Triggering Assertions

4. Assertion Logic

Best Practices for Writing Assertions

3. Testing the Assertion

Test Imports

Test Contract Structure

Setup

Testing Assertion Reverted

Testing Assertion Success

Full Test Contract

Key Testing Concepts

Running the Tests

Conclusion

What’s Next?

Getting Started

Credible Layer

Use Case Mapping

​Introduction

​1. Setting Up Your Project

​2. Writing the Assertion

​How Assertions Work

​Gas Consumption

​Anatomy of the Assertion

​1. Imports and Contract Definition

​2. State Variables and Constructor

​3. Triggering Assertions

​4. Assertion Logic

​Best Practices for Writing Assertions

​3. Testing the Assertion

​Test Imports

​Test Contract Structure

​Setup

​Testing Assertion Reverted

​Testing Assertion Success

​Full Test Contract

​Key Testing Concepts

​Running the Tests

​Conclusion

​What’s Next?

Introduction

1. Setting Up Your Project

2. Writing the Assertion

How Assertions Work

Gas Consumption

Anatomy of the Assertion

1. Imports and Contract Definition

2. State Variables and Constructor

3. Triggering Assertions

4. Assertion Logic

Best Practices for Writing Assertions

3. Testing the Assertion

Test Imports

Test Contract Structure

Setup

Testing Assertion Reverted

Testing Assertion Success

Full Test Contract

Key Testing Concepts

Running the Tests

Conclusion

What’s Next?