PCL Assertion Guide - Phylax Credible Layer Documentation

Introduction

The Phylax Credible Layer (PCL) is a security prevention framework that helps protect smart contracts by continuously verifying critical protocol invariants. PCL assertions act as automated guardians that detect, alert on, and prevent unauthorized state changes or invalid conditions in your protocol.

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

Why Use PCL Assertions?

Unlike traditional auditing or testing that only happens during development, PCL assertions:

Actively protect your protocol in real-time on the blockchain
Automatically detect and prevent violations of critical invariants
Block potential exploits before any damage occurs
Provide an active defense layer beyond standard tests and audits

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.28;

// 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

Project Structure

When using PCL assertions, your project should follow this structure:

|-- assertions
|    |-- src
|    |    |-- OwnableAssertion.a.sol  # Assertion implementation
|    |
|    |-- test
|         |-- OwnableAssertion.t.sol  # Tests for your assertions
|-- src
     |
     |-- Ownable.sol  # Your protocol contract

The phorge command takes the assertions directory location as an argument and should be run from the project root containing both assertions and src directories.

Installing the credible-std Library

Before writing assertions, you need to install the credible-std library which provides the base contracts and utilities for PCL assertions:

forge install https://github.com/phylaxsystems/credible-std/

After installation, create a remappings.txt file at the root of your project with the following content:

credible-std/=lib/credible-std/src/
forge-std/=lib/credible-std/lib/forge-std/src/

These remappings will ensure that your imports work correctly when referencing the credible-std library. The PCL CLI will automatically detect and use these remappings when compiling your contracts, so no additional configuration is needed.

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.28;

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 addresses of contracts we need to interact with
The constructor initializes these variables when the assertion is deployed
The constructor is optional, you don’t need to implement it if you don’t need to pass any values to the assertion
Optimization: In most cases using immutable to define the address of the protocol is more efficient

Here’s how you would implement the optimized version with immutable:

// More gas-efficient implementation using immutable
Ownable immutable ownable;

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

The constructor of the assertion runs against an empty state. That means you can pass values in the constructor but you can not read values from other contracts.

3. Registering Assertion Functions

// 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

The PCL framework supports different trigger types. registerCallTrigger is used to run assertions after any transaction interacting with the protected contract. Other triggers can be implemented depending on your needs. See the “Triggers” section in the cheatcodes documentation for more information.

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 PCL

Best Practices for Writing Assertions

Single Responsibility: Each assertion should verify one specific property or invariant
State Management: Use forkPreState() and forkPostState() to compare values before and after transactions
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 phorge 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 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 = "Ownership has changed";

    // 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:

cl.addAssertion(): Links the assertion to the contract being protected
- First argument: Label of the assertion
- Second argument: Address of contract to protect
- Third argument: Bytecode of the assertion contract
- Fourth argument: Constructor arguments for the assertion
vm.prank(): Simulates a call from the owner’s address
vm.expectRevert(): Expects the assertion to revert
cl.validate(): Tests how the assertion responds to a transaction
- First argument: Label of the assertion
- Second argument: Address of contract to protect
- Third argument: ETH value (0 in this case)
- Fourth argument: Encoded function call (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

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

    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 {console} from "../../lib/credible-std/lib/forge-std/src/console.sol";
import {CredibleTest} from "../../lib/credible-std/src/CredibleTest.sol";
import {Test} from "../../lib/credible-std/lib/forge-std/src/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 = "Ownership has changed";

        // 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 = "Ownership has not changed";
        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

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 meaningful labels to identify assertions

Running the Tests

pcl phorge test

Conclusion

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

Credible Layer

Use Case Mapping

​Introduction

​Why Use PCL Assertions?

​1. Setting Up Your Project

​Project Structure

​Installing the credible-std Library

​2. Writing the Assertion

​How Assertions Work

​Anatomy of the Assertion

​1. Imports and Contract Definition

​2. State Variables and Constructor

​3. Registering Assertion Functions

​4. Assertion Logic

​Best Practices for Writing Assertions

​3. Testing the Assertion

​Test Contract Structure

​Setup

​Testing Assertion Failure

​Testing Assertion Success

​Full Test Contract

​Key Testing Concepts

​Running the Tests

​Conclusion

​What’s Next?

Introduction

Why Use PCL Assertions?

1. Setting Up Your Project

Project Structure

Installing the credible-std Library

2. Writing the Assertion

How Assertions Work

Anatomy of the Assertion

1. Imports and Contract Definition

2. State Variables and Constructor

3. Registering Assertion Functions

4. Assertion Logic

Best Practices for Writing Assertions

3. Testing the Assertion

Test Contract Structure

Setup

Testing Assertion Failure

Testing Assertion Success

Full Test Contract

Key Testing Concepts

Running the Tests

Conclusion

What’s Next?