Incorrect Memory Alignment and Proof Verification in 'readMem' and 'writeMem' Functions

[howlbot-integration[bot]]

Lines of code

https://github.com/code-423n4/2024-07-optimism/blob/70556044e5e080930f686c4e5acde420104bb2c4/packages/contracts-bedrock/src/cannon/MIPS.sol#L538-L584 https://github.com/code-423n4/2024-07-optimism/blob/70556044e5e080930f686c4e5acde420104bb2c4/packages/contracts-bedrock/src/cannon/MIPS.sol#L592-L632

Vulnerability details

Impact

• Incorrect Memory Operations: Misaligned memory addresses can lead to incorrect data being read or written, potentially causing data corruption.
• Invalid Proof Verification: Failure to correctly verify memory proofs can result in accepting invalid memory states, compromising the integrity of the MIPS emulator.

Proof of Concept

• If an unaligned address is passed to 'readMem' or 'writeMem', the functions will not correctly handle the memory operation, leading to potential data corruption.

  uint32 unalignedAddress = 0x00000003; // Example of an unaligned address
  uint32 value = readMem(unalignedAddress, 0); // This should revert with an alignment error

• If the proof verification logic is incorrect, an invalid memory proof could be accepted, leading to an incorrect memory root being used.

  // Example of an incorrect proof that should fail verification
  bytes memory incorrectProof = hex"0000000000000000000000000000000000000000000000000000000000000000";
  uint32 address = 0x00000000;
  uint32 value = readMem(address, 0); // This should revert with a proof verification error

Tools Used

Manual review

Recommended Mitigation Steps

• Ensure the alignment check is correctly implemented with a meaningful error message.

  function readMem(uint32 _addr, uint8 _proofIndex) internal pure returns (uint32 out_) {
  unchecked {
      uint256 offset = proofOffset(_proofIndex);
  
      assembly {
          // Validate the address alignment.
          if and(_addr, 3) { revert("Memory address not aligned") }
  
          // Load the leaf value.
          let leaf := calldataload(offset)
          offset := add(offset, 32)
  
          // Convenience function to hash two nodes together in scratch space.
          function hashPair(a, b) -> h {
              mstore(0, a)
              mstore(32, b)
              h := keccak256(0, 64)
          }
  
          // Start with the leaf node.
          // Work back up by combining with siblings, to reconstruct the root.
          let path := shr(5, _addr)
          let node := leaf
          for { let i := 0 } lt(i, 27) { i := add(i, 1) } {
              let sibling := calldataload(offset)
              offset := add(offset, 32)
              switch and(shr(i, path), 1)
              case 0 { node := hashPair(node, sibling) }
              case 1 { node := hashPair(sibling, node) }
          }
  
          // Load the memory root from the first field of state.
             let memRoot := mload(0x80)
  
             // Verify the root matches.
             if iszero(eq(node, memRoot)) {
                 revert("Memory proof verification failed")
             }
  
             // Bits to shift = (32 - 4 - (addr % 32)) * 8
             let shamt := shl(3, sub(sub(32, 4), and(_addr, 31)))
             out_ := and(shr(shamt, leaf), 0xFFffFFff)
         }
     }
  }

• Ensure the proof verification logic is correct and provides meaningful error messages.

  function writeMem(uint32 _addr, uint8 _proofIndex, uint32 _val) internal pure {
  unchecked {
      uint256 offset = proofOffset(_proofIndex);
  
      assembly {
          // Validate the address alignment.
          if and(_addr, 3) { revert("Memory address not aligned") }
  
          // Load the leaf value.
          let leaf := calldataload(offset)
          let shamt := shl(3, sub(sub(32, 4), and(_addr, 31)))
  
          // Mask out 4 bytes, and OR in the value
          leaf := or(and(leaf, not(shl(shamt, 0xFFffFFff))), shl(shamt, _val))
          offset := add(offset, 32)
  
          // Convenience function to hash two nodes together in scratch space.
             function hashPair(a, b) -> h {
                 mstore(0, a)
                 mstore(32, b)
                 h := keccak256(0, 64)
             }
  
             // Start with the leaf node.
             // Work back up by combining with siblings, to reconstruct the root.
             let path := shr(5, _addr)
             let node := leaf
             for { let i := 0 } lt(i, 27) { i := add(i, 1) } {
                 let sibling := calldataload(offset)
                 offset := add(offset, 32)
                 switch and(shr(i, path), 1)
                 case 0 { node := hashPair(node, sibling) }
                 case 1 { node := hashPair(sibling, node) }
             }
  
             // Load the memory root from the first field of state.
             let memRoot := mload(0x80)
  
             // Verify the root matches.
             if iszero(eq(node, memRoot)) {
                 revert("Memory proof verification failed")
             }
  
             // Store the new memory root in the first field of state.
             mstore(0x80, node)
         }
     }
  }

Assessed type

Math

[mbaxter]

It's true that we allow unaligned reads / writes, this is a known issue we are considering addressing.

However, the submission doesn't really demonstrate the issue - we already have reverts in the methods mentioned. And we already have memory proof checks. The suggested changes use a different revert style and add some additional proof checks that are incorrect.

Additionally, this issue is highlighted in the Cantina audit (3.3.2) - not sure if that invalidates this submission (I don't see the cantina audit listed in the rules).

[mbaxter]

Switching to confirmed after offline discussion because the unaligned read / write issue is real.

[c4-judge]

zobront marked the issue as satisfactory

[c4-judge]

zobront marked the issue as selected for report

[Haxatron]

This report is invalid, in all the calls to readMem and writeMem the effective address passed will have the two least significant bits zeroed, making them aligned

                    uint32 mem = readMem(a1 & 0xFFffFFfc, 1); // mask the addr to align it to 4 bytes

                    writeMem(a1 & 0xFFffFFfc, 1, mem);

There is indeed a problem with certain instructions not throwing an exception when the effective address is unaligned thus not adhering to MIPS spec, but that is described in https://github.com/code-423n4/2024-07-optimism-findings/issues/82 and not here.

[zobront]

This issue specifically focuses on readMem() and writeMem(), which are always called safely in the code as @Haxatron points out. Therefore, there is no situation in which the memory could be misaligned when these functions are called.

This is in contrast to issue #82, in which LH and LHU do not have this same guarantee, and is therefore valid.

For this reason, I will be marking this issue as Invalid.

[c4-judge]

zobront marked the issue as not selected for report

[c4-judge]

zobront removed the grade

[c4-judge]

zobront marked the issue as unsatisfactory: Invalid