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 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"; // Using remapping for credible-std
import {Ownable} from "../../src/Ownable.sol"; // Ownable contract

contract OwnableAssertion is Assertion {
    // The contract we're protecting
    Ownable ownable;

    // Constructor takes the address of the contract to protect
    constructor(address ownable_) {
        ownable = Ownable(ownable_); // Initialize the Ownable contract reference
    }

    // 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 transactions interact with the Ownable contract
        registerCallTrigger(this.assertionOwnershipChange.selector);
    }

    // This assertion checks if ownership has changed between pre and post transaction states
    function assertionOwnershipChange() external {
        // 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.

​

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 ownable;

constructor(address ownable_) {
    ownable = Ownable(ownable_);
}

• State variables store the address of contract the assertion is protecting
• The constructor initializes this variable when the assertion is deployed
• The constructor is optional, but it is recommended to use this approach to have more flexibility and be able to use the same assertion to protect different contracts
• You can hardcode the address of the contract you want to protect in the assertion contract, but this only makes sense if you are sure that the assertion will only be used with that one contract and you want to safe a bit of gas

​

3. Triggering Assertions

// 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 transactions interact with the Ownable contract
    registerCallTrigger(this.assertionOwnershipChange.selector);
}

• The triggers function is required by the Assertion interface
• It defines which functions in your contract are assertions
• Each assertion function must be registered here via its function selector
• Multiple assertions can be defined in a single contract
• registerCallTrigger specifically registers functions to be called after any interaction with the protected contract
• Use triggers to make sure that assertions are only called when they are needed in order to save gas and resources

​

4. Assertion Logic

function assertionOwnershipChange() external {
    ph.forkPreState();                    // Take snapshot before transaction
    address preOwner = ownable.owner();   // Get pre-transaction owner
    ph.forkPostState();                   // Take snapshot after transaction
    address postOwner = ownable.owner();  // Get post-transaction owner
    require(postOwner == preOwner, "Ownership has changed");
}

• The main assertion logic uses special features:
  • ph.forkPreState(): Examines state before the transaction
  • ph.forkPostState(): Examines state after the transaction
• The assertion reverts if the condition is not met
• The ph namespace refers to the Phylax Helper, which provides 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

1. Single Responsibility: Each assertion should verify one specific property or invariant
2. State Management: Use forkPreState() and forkPostState() to compare values before and after transactions
3. Comprehensive Testing: Write thorough tests to verify both positive and negative cases

​

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.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 {
    address public newOwner = address(0xdeadbeef);
    Ownable public assertionAdopter;
    address public initialOwner = address(0xdeadb999f);

• Inherits from CredibleTest and Test which provides testing utilities
• CredibleTest provides the cl cheatcode interface for testing PCL 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

function setUp() public {
    assertionAdopter = new Ownable();
    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 Failure

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 under the hood when the protocol is being called
    cl.addAssertion(label, aaAddress, type(OwnableAssertion).creationCode, abi.encode(assertionAdopter));

    vm.prank(initialOwner);
    vm.expectRevert("Assertions Reverted");
    cl.validate(
        label, aaAddress, 0, abi.encodePacked(assertionAdopter.transferOwnership.selector, abi.encode(newOwner))
    );
}

Key components:

1. 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 arguments for the assertion
2. vm.prank(): Simulates a call from the owner’s address
3. vm.expectRevert(): Expects the assertion to revert
4. cl.validate(): Tests how the assertion responds to a transaction
   • First argument: Label of the assertion (use the name of the assertion you are testing)
   • Second argument: Address of contract to protect
   • Third argument: ETH value (0 in this case)
   • Fourth argument: Encoded function call (transferOwnership in this case)

​

Testing Assertion Success

function test_assertionOwnershipNotChanged() public {
    string memory label = "OwnableAssertion";
    address aaAddress = address(assertionAdopter);

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

    vm.prank(initialOwner);
    cl.validate(
        label, aaAddress, 0, abi.encodePacked(assertionAdopter.transferOwnership.selector, abi.encode(initialOwner))
    ); // assert that the ownership has not changed
}

• Similar setup 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.28;

import {OwnableAssertion} from "../src/OwnableAssertion.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 {
    address public newOwner = address(0xdeadbeef);
    Ownable public assertionAdopter;
    address public initialOwner = address(0xdeadb999f);

    function setUp() public {
        assertionAdopter = new Ownable();
        vm.deal(initialOwner, 1 ether);
    }

    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 under the hood when the protocol is being called
        cl.addAssertion(label, aaAddress, type(OwnableAssertion).creationCode, abi.encode(assertionAdopter));

        vm.prank(initialOwner);
        vm.expectRevert("Assertions Reverted");
        cl.validate(
            label, aaAddress, 0, abi.encodePacked(assertionAdopter.transferOwnership.selector, abi.encode(newOwner))
        );
    }

    function test_assertionOwnershipNotChanged() public {
        string memory label = "OwnableAssertion";
        address aaAddress = address(assertionAdopter);

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

        vm.prank(initialOwner);
        cl.validate(
            label, aaAddress, 0, abi.encodePacked(assertionAdopter.transferOwnership.selector, abi.encode(initialOwner))
        ); // assert that the ownership has not changed
    }
}

​

Key Testing Concepts

1. Assertion Registration: Use cl.addAssertion() to register assertions with contracts
2. Transaction Simulation: Use cl.validate() to test how assertions respond to transactions
3. State Manipulation: Use Forge’s cheatcodes (vm.prank, vm.deal) to set up test scenarios
4. Verification: Use vm.expectRevert() to verify that the assertion reverts when expected
5. 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:

1. Enhance Security: Block unauthorized changes to critical protocol parameters
2. Eliminate Risk: Prevent potential exploits before any damage occurs
3. Build Trust: Demonstrate to users that your protocol is actively protected
4. 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.