We’ve created a comprehensive suite of assertions based on Optimism’s Failure Mode Analysis (FMA) framework to prevent critical failure modes identified in the protocol.

Optimism’s FMA process systematically identifies, analyzes, and mitigates potential failure modes. As documented in their security design docs, FMAs “shift-left” risk assessment so mitigations can be planned and implemented earlier.

We chose Optimism’s FMA framework because it represents a comprehensive and well-documented approach to security analysis. The protocol has conducted extensive failure mode analyses across various components including the Interop Portal, ETH Lockbox, Message Passing contracts, and more. This makes it an excellent case study for demonstrating how assertions can prevent specific failure modes identified through systematic security analysis.

Link to the Phylax fork of Optimism: https://github.com/phylaxsystems/optimism/tree/feat/fma-assertions/packages/contracts-bedrock/assertions

​
Approach

Our approach follows the same systematic methodology used in Optimism’s FMA process. We analyze each identified failure mode and create assertions that prevent the conditions that could lead to those failures.

The key insight is that many failure modes identified in FMAs can be prevented by enforcing invariants at the transaction level. For example, if an FMA identifies that “incorrect state reporting by AnchorStateRegistry” could lead to withdrawal safety failures, we can write assertions that validate state consistency before allowing withdrawal transactions to proceed.

​
Assertion Collections Overview

​
FMA ETH Lockbox Assertions

This collection validates the ETHLockbox contract’s security properties, corresponding to the ETH Lockbox FMA document:

​
Key Checks:

  • FM1: Unauthorized Access Protection - Ensures only authorized portals can call lockETH and unlockETH functions
  • FM2: Drain Prevention - Prevents the lockbox from being drained to zero balance in a single transaction
  • FM3: Proxy Upgrade Protection - Monitors for unexpected proxy implementation address changes that could indicate buggy upgrades

​
Risk Context:

These assertions address CRITICAL failure modes where unauthorized access or bugs could lead to complete loss of ETH liquidity from the lockbox, with HIGH impact but LOW likelihood due to access controls and upgrade procedures.

​
FMA Interop Portal Assertions

This collection validates the OptimismPortal2 and AnchorStateRegistry integration, corresponding to the Interop Portal FMA document:

​
Key Checks:

  • FM1: AnchorStateRegistry Integrity - Validates retirement timestamp updates, respected game type changes, anchor state transitions, and blacklist operations
  • FM2: Migration Logic Safety - Ensures ETH lockbox and portal migrations maintain fund safety and state consistency
  • FM4: SuperRoots Toggle Validation - Validates that superRootsActive flag changes follow proper authorization and state requirements

​
Risk Context:

These assertions address CRITICAL failure modes where incorrect state reporting or migration bugs could lead to Withdrawal Safety Failure or Withdrawal Liveness Failure, with LOW likelihood but HIGH/CRITICAL impact.

​
FMA L2 Message Passing Assertions

This collection validates cross-chain message passing contracts, corresponding to the Message Passing FMA document:

​
Key Checks:

  • FM1: Destination Chain Validation - Ensures messages aren’t sent to invalid destinations (same chain, zero chain ID, etc.)
  • FM2: Message Validation Integrity - Validates message identifiers and parameters for cross-chain message validation
  • FM3: Message Relay Completeness - Ensures sent messages are properly recorded and can be relayed
  • FM4: Replay Protection - Prevents duplicate message execution through proper successfulMessages tracking
  • FM5: Reentrancy Protection - Ensures message relay functions are atomic and non-reentrant
  • FM6: Repeated Identifier Validation - Prevents duplicate identifier usage within the same transaction

​
Risk Context:

These assertions address CRITICAL failure modes where message passing bugs could lead to asset theft, duplicate minting, or lost funds, with MEDIUM likelihood and HIGH/CRITICAL impact depending on the specific failure mode.