Kontrol Integrated Verification of the Optimism Pausability Mechanism

We are pleased to announce our recently completed work with Optimism and Kontrol integration into their CI. Having Kontrol as part of Optimism's CI produces proof of correctness for critical properties of the code as it evolves. For this particular engagement, we verified the pausability mechanism of their L1 contracts and integrated the verification work as part of Optimism's CI. This ensures that the code is verified as it evolves.

Our formal verification tool of choice is Kontrol, which is actively developed by the team at Runtime Verification. Simply put, Kontrol combines KEVM and Foundry to grant smart contract developers the ability to perform formal verification without learning a new language or tool through the use of symbolic property testing. If you want to know more about the capabilities of the tool, you can check our last blog and our documentation, or go to our Discord and ask our team directly.

Kontrol Verification of Optimism's Pausability Mechanism

The goal of this engagement was twofold: first, verify Optimism's pausability mechanism for the L1 contracts, and second, ensure that the mechanism is verified as Optimism's code evolves. But what is this pausability mechanism we're talking about?

Optimism L1 contracts have a security mechanism that allows L2-to-L1 transactions to be paused. This means that, if necessary, governance can prevent L2-to-L1 transactions from being finalized by the pertinent L1 contracts.

The L1 contracts can be paused by the appointed guardian address by calling the pause function of the SuperchainConfig contract. Once pause() is called by the guardian, all bridge functions in charge of processing L2-to-L1 transactions must always revert if called. This ensures that ETH and tokens in the L1 contracts cannot be withdrawn while the system is paused.

The specifications for such a pausability system are quite straightforward. For instance, here's the specification in the form of a property test that expresses the correctness of the pausability mechanism for the finalizeWithdrawalTransaction function of the OptimismPortal contract:

function prove_finalizeWithdrawalTransaction_paused(Types.WithdrawalTransaction calldata _tx) external {
    	vm.prank(optimismPortal.guardian());
    	superchainConfig.pause("identifier");

    	vm.expectRevert(CallPaused.selector);
    	optimismPortal.finalizeWithdrawalTransaction(_tx);
}

Kontrol will execute this property test with the parameter _tx being symbolic (i.e., representing all possible values) and check that the code always follows the behavior described in the property test. As opposed to fuzzing, which will instantiate _tx with plenty of random or pseudo-random concrete values, Kontrol mathematically ensures that for any possible value of _tx, the behavior complies with what is outlined in the property test.

Since the logic of the specifications is not particularly complex, where do the main verification challenges reside? There are two main conditions for running these symbolic property tests that must be met: the correct signature of the functions under verification, and the appropriate context in which they are symbolically executed.

Let's start with the function signatures. Kontrol performs EVM-bytecode symbolic execution, which means that, instead of reasoning directly on the arguments provided at the Solidity level, it has to work with their ABI encoding. Reasoning about Booleans or unsigned integers doesn't pose much of a problem since their ABI encoding rules are straightforward. However, dealing with dynamic types such as bytes or bytes[] significantly increases the reasoning difficulty due to the way in which they're encoded in the EVM.

Reasoning about these types presents some challenges. First, in ABI, the encoding of these types consists of several components that have to be properly abstracted. Second, the Solidity compiler inserts manipulations for these types that, when treating them as symbolic values, can introduce unbounded loops. This post does not cover how we addressed these two difficulties; we will discuss them in detail in a follow-up post.

The other main condition to be resolved is executing the formal verification proofs in a realistic environment. The code under verification does not implement very complex logic. However, the challenge lies in verifying that when the system is correctly deployed, the pausability mechanism will always function as intended. This means that checking in isolation that calling a function reverts if the system is paused could miss unforeseen interactions introduced by the complexity of the overall system.

To ensure that the verification considered the whole system as it is intended to be deployed rather than an isolated contract, we developed a new feature in Kontrol that leverages Foundry's recent state diff recording capabilities to faithfully include the relevant parts of the deployment sequence as the initial configuration to perform the verification. A follow-up post will describe in detail the mechanism.

You can find the technical description and implementation of this project in the Optimism repository here.

Kontrol Integration Into a Protocol's CI System

Kontrol can be used in different ways and at different stages of the development cycle, depending on the project's needs. In the case of Optimism, our focus was on integrating Kontrol into their CI process and improving the overall security of the protocol after deployment.

Many projects set up a CI system just before a project is deployed to mainnet, and CI becomes a key component of the delivery and development processes. At that point, it is safe to assume that a project has undergone several different reviews, including but not limited to an audit, different testing cycles, design reviews, and has a bug bounty program. All of that aside, these measures don't cover two constants that are particularly critical in the web3 space:

• Code cannot be proven to be 100% free of vulnerabilities and possible exploits. This, combined with the fact that most web3 code is open source and holds a large amount of funds, makes projects a target for hackers who try to find a way to exploit them.

• Every time a piece of code is changed or updated, it introduces the possibility of introducing new vulnerabilities that were not present before. Audits are significantly impacted by this, making it critical to set up post-deployment security measures to mitigate risks introduced by code changes.

Kontrol CI integration mitigates the risks associated with both of these concerns, and Kontrol helps to ensure that important properties will continue to hold after the code changes. For active projects that regularly update the code, we recommend introducing Kontrol into the CI for continuous assurance that the protocol-specific invariants hold and that critical code elements cannot be exploited.

As an example of how Kontrol will further enhance Optimism's smart contract security, consider the OptimismPortal contract. This critical contract, which holds all bridged ETH, has been recently modified to support upcoming fault proofs upgrade. To ensure the security and confidence of the new implementation, the existing Kontrol proofs are being extended to the new implementation before mainnet launch.

Want to Learn More?

We will be publishing more blog posts on our work with Optimism from a more technical perspective, so keep an eye out for them on our Twitter. If you have any questions on how to start using Kontrol or how we can help you integrate it into your project, contact us!