Skip to content

Latest commit

 

History

History
194 lines (135 loc) · 16.7 KB

README.md

File metadata and controls

194 lines (135 loc) · 16.7 KB

Kontrol Verification

Getting Started

Overview

Kontrol is a tool by Runtime Verification (RV) that enables formal verification of Ethereum smart contracts. Quoting from the Kontrol docs:

Kontrol combines KEVM and Foundry to grant developers the ability to perform formal verification without learning a new language or tool. This is especially useful for those who are not verification engineers. Additionally, developers can leverage Foundry test suites they have already developed and use symbolic execution to increase the level of confidence.

KEVM is a tool that enables formal verification of smart contracts on the Ethereum blockchain. It provides a mathematical foundation for specifying and implementing smart contracts. Developers can use KEVM to rigorously reason about the behavior of their smart contracts, ensuring correctness and reducing the likelihood of vulnerabilities in the contract code.

This document details the Kontrol setup used in this repo to run various proofs against the contracts in the contracts-bedrock directory.

Directory structure

The directory is structured as follows

├── pausability-lemmas.md: File containing the necessary lemmas for this project
├── deployment: Custom deploy sequence for Kontrol proofs and tests for its fast summarization
│   ├── KontrolDeployment.sol: Simplified deployment sequence for Kontrol proofs
│   └── DeploymentSummary.t.sol: Tests for the summarization of custom deployment
├── proofs: Where the proofs (tests) themselves live
│   ├── *.k.sol: Symbolic property tests for contracts
│   ├── interfaces: Interface files for src contracts, to avoid unnecessary compilation of contracts
│   └── utils: Proof dependencies, including the autogenerated deployment summary contracts
└── scripts: Where the scripts of the projects live
    ├── json: Data cleaning scripts for the output of KontrolDeployment.sol
    ├── make-summary-deployment.sh: Executes KontrolDeployment.sol, curates the result and writes the summary deployment contract
    └── run-kontrol.sh: Wrapper around the kontrol CLI to run the proofs

Installation

  1. cd to the root of this repo.
  2. Install Foundry by running pnpm install:foundry. This installs foundryup, the foundry toolchain installer, then installs the required foundry version.
  3. Install Kontrol by running pnpm install:kontrol. This installs kup, the package manager for RV tools, then installs the required kontrol version.
  4. Install Docker.

Usage

Verifying proofs has two steps: build, and execute.

Build Deployment Summary

First, generate a deployment summary contract from the deploy script in KontrolDeployment.sol by running the following command:

./test/kontrol/scripts/make-summary-deployment.sh [container|local|dev]

The make-summary-deployment.sh supports the same execution modes as run-kontrol.sh below.

KontrolDeployment.sol contains the minimal deployment sequence required by the proofs. The make-summary-deployment.sh script will generate a JSON state diff. This state diff is used in two ways by Kontrol. First, Kontrol generates a summary contract recreating the state diffs recorded in the JSON. This contract is used to test that the information contained in the generated JSON is correct and aids in the specification of the symbolic property tests. The generation of this contract is also handled by the make-summary-deployment.sh script. Second, the state diff JSON is used to load the post-deployment state directly into Kontrol when running the proofs.

This step is optional if an up-to-date summary contract already exists, which will be the case until the KontrolDeployment contract changes, or any of the source contracts under test change. See the Implementation Details section for more information, and to learn about the CI check that ensures the committed autogenerated files from this step are up-to-date.

The summary contract can be found in DeploymentSummary.sol, which is summarization (state changes) of the KontrolDeployment.sol contract.

Execute Proofs

Use the run-kontrol.sh script to runs the proofs in all *.k.sol files.

./test/kontrol/scripts/run-kontrol.sh [container|local|dev] [script|tests]

The run-kontrol.sh script supports three modes of proof execution:

  • container: Runs the proofs using the same Docker image used in CI. This is the default execution mode—if no arguments are provided, the proofs will be executed in this mode.
  • local: Runs the proofs with your local Kontrol install, and enforces that the Kontrol version matches the one used in CI, which is specified in versions.json.
  • dev: Run the proofs with your local Kontrol install, without enforcing any version in particular. The intended use case is proof development and related matters.

It also supports two methods for specifying which tests to execute:

  • script: Runs the tests specified in the test_list variable
  • tests: Names of the tests to be executed. tests can have two forms:
    • ContractName.testName: e.g., run-kontrol.sh ContractName.test1 ContractName.test2
    • Empty, executing all the functions starting with test, prove or check present in the defined out directory. For instance, ./test/kontrol/scripts/run-kontrol.sh will execute all prove_* functions in the proofs directory using the same Docker image as in CI. [Warning: executing all proofs in parallel is very resource intensive]

For a similar description of the options run run-kontrol.sh --help.

Add New Proofs

These are the instructions to add a new proof to this project. If all functions involved in the new proof are from a contract already deployed by KontrolDeployment the first two steps can be skipped.

Make Kontrol aware of the new contract being tested

The runKontrolDeployment function of KontrolDeployment partially reproduces the deployment process laid out in the _run function of Deploy.s.sol. runKontrolDeployment has the stateDiff modifier to make use of Foundry's state diff cheatcodes. Kontrol utilizes the JSON resulting from this modifier for two purposes:

  1. Load all the state updates generated by runKontrolDeployment as the initial configuration for all proofs, effectively offloading the computation of the deployment process to forge and thus improving performance.
  2. Produce the DeploymentSummary script contract to test that the produced JSON contains correct updates.

Hence, in order to write a proof for a contract which is not present in KontrolDeployment it must be added there first. To add a new contract, properly inspect the above-mentioned _run function and place the corresponding deployment steps of the contract appropriately within the runKontrolDeployment function.

Once new deployment steps have been added to runKontrolDeployment the state-diff files have to be rebuilt.

Include existing tests on the new state-diff recorded bytecode

The next step is to include tests for the newly included state updates in DeploymentSummary.t.sol. These tests inherit the tests from test of the contracts deployed by runKontrolDeployment. This ensures that deployment steps were implemented correctly and that the state updates are correct.

It might be necessary to set some of the existing tests from test as virtual because they can't be executed as is. See DeploymentSummary.t.sol for more concrete examples.

Add function signatures to KontrolInterfaces

So far we've got all the state updates ready to be added to the initial configuration of each proof, but we cannot yet write any proof about the function. We still need to add the relevant signatures into KontrolInterfaces. The reason for having KontrolInterfaces instead of using directly the contracts is to reduce the amount of compiled contracts by Kontrol. In the future there might interfaces for all contracts under contracts-bedrock, which would imply the removal of KontrolInterfaces.

Write the proof

Write your proof in a .k.sol file in the proofs folder, which is the test directory used by the kprove profile to run the proofs (see Deployment Summary Process). The name of the new proofs should start with prove (or check) instead of test to avoid forge test running them. The reason for this is that if Kontrol cheatcodes (see Kontrol's own cheatcodes) are used in a test, it will not be runnable by forge. Currently, none of the tests are using custom Kontrol cheatcodes, but this is something to bear in mind.

To reference the correct addresses for writing the tests, first import the signatures as in this example:

import {
    IOptimismPortal as OptimismPortal,
    ISuperchainConfig as SuperchainConfig
} from "./interfaces/KontrolInterfaces.sol";

Declare the correspondent variables and cast the correct signatures to the correct addresses:

OptimismPortal optimismPortal;
SuperchainConfig superchainConfig;

function setUp() public {
    optimismPortal = OptimismPortal(payable(optimismPortalProxyAddress));
    superchainConfig = SuperchainConfig(superchainConfigProxyAddress);
}

Note that the names of the addresses come from DeploymentSummary.t.sol and are automatically generated by the make-summary-deployment.sh script.

Add your test to run-kontrol.sh

As described in Execute Proofs, there's a script mode for specifying which proofs to run, and that is the mode used in CI. To run the new proofs with the script option, add ContractName.prove_functionName_paused to the variable test_list in the run-kontrol.sh script.

Implementation Details

Assumptions

  1. A critical invariant of the KontrolDeployment.sol contract is that it stays in sync with the original Deploy.s.sol contract. Currently, this is partly enforced by running some of the standard post-setUp deployment assertions in DeploymentSummary.t.sol. A more rigorous approach may be to leverage the ChainAssertions library, but more investigation is required to determine if this is feasible without large changes to the deploy script.

  2. Size of bytes[] arguments. In OptimismPortal.k.sol, the prove_proveWithdrawalTransaction_paused proof is broken down into 11 different proofs, each corresponding to a different size of the _withdrawalProof argument, which is of type bytes[]. We execute the same logic for lengths of _withdrawalProof ranging from 0 to 10, setting the length of each symbolic bytes element to 600.

    • The reason for a max length of 10 is that it provides a conservative upper bound based on historical data for proof sizes.
    • The reason for choosing 600 as the length for the elements of _withdrawalProof is that each element is 17 * 32 = 544 bytes long, so adding a 10% margin for RLP encoding and rounding up yields 600 bytes. The same historical data confirms this is a valid bound.
    • All other symbolic bytes arguments that are not part of a bytes array have a symbolic length bounded by 2^63.

Deployment Summary Process

As mentioned above, a deployment summary contract is first generated before executing the proofs. This is because the proof execution leverages Kontrol's fast summarization feature, which allows loading the post-setUp state directly into Kontrol. This provides a significant reduction in proof execution time, as it avoids the need to execute the deployment script every time the proofs are run.

All code executed in Kontrol—even when execution is concrete and not symbolic—is significantly slower than in Foundry, due to the mathematical representation of the EVM in Kontrol. Therefore we want to minimize the amount of code executed in Kontrol, and the fast summarization feature allows us to reduce setUp execution time.

This project uses two different foundry.toml profiles, kdeploy and kprove, to facilitate usage of this fast summarization feature.:

  • kdeploy: Used by make-summary-deployment.sh to generate the DeploymentSummary.sol contract based on execution of the KontrolDeployment.sol contract using Foundry's state diff recording cheatcodes. This is where all necessary src/L1 files are compiled with their bytecode saved into the DeploymentSummaryCode.sol file, which is inherited by DeploymentSummary.

  • kprove: Used by the run-kontrol.sh script to execute proofs, which can be run once a DeploymentSummary.sol contract is present. This profile's src and script paths point to a test folder because we only want to compile what is in the test/kontrol/proofs folder, since that folder contains all bytecode and proofs.

The make-summary-deployment.sh scripts saves off the generated JSON state diff to snapshots/state-diff/Kontrol-Deploy.json, and is run as part of the snapshots script in package.json. Therefore, the snapshots CI check will fail if the committed Kontrol state diff is out of sync. Note that the CI check only compares the JSON state diff, not the generated DeploymentSummary.sol or DeploymentSummaryCode contracts. This is for simplicity, as those three files will be in sync upon successful execution of the make-summary-deployment.sh script. We commit the DeploymentSummary.sol and DeploymentSummaryCode.sol contracts, because forge fails to build if those contracts are not present—it is simpler to commit these autogenerated files than to workaround their absence in forge builds.

During make-summary-deployment.sh, the mustGetAddress usage in Deploy.s.sol is temporarily replaced by getAddress—the former reverts if the deployed contract does not exist, while the latter returns the zero address. This is required because the deploy script in KontrolDeployment.sol is does not fully reproduce all deployments in Deploy.s.sol, so the mustGetAddress usage would cause the script to revert since some contracts are not deployed. KontrolDeployment.sol is a simplified, minimal deployment sequence for Kontrol proofs, and is not intended to be a full deployment sequence for the contracts in contracts-bedrock.