c4-submissions commented 11 months ago

Lines of code

https://github.com/code-423n4/2023-10-zksync/blob/1fb4649b612fac7b4ee613df6f6b7d921ddd6b0d/code/system-contracts/bootloader/bootloader.yul#L551-L633 https://github.com/code-423n4/2023-10-zksync/blob/1fb4649b612fac7b4ee613df6f6b7d921ddd6b0d/code/system-contracts/bootloader/bootloader.yul#L771-L782 https://github.com/code-423n4/2023-10-zksync/blob/1fb4649b612fac7b4ee613df6f6b7d921ddd6b0d/code/system-contracts/bootloader/bootloader.yul#L2194-L2216

Vulnerability details

Impact

Use a formally verified implementation for critical logic around transaction processing, signatures, authentication etc. Current contract seems prone to risks.

Proof of Concept

Using a formally verified implementation would improve the security and reliability of critical logic in this contract. Some areas that could benefit from a formally verified implementation:

Transaction processing logic - https://github.com/code-423n4/2023-10-zksync/blob/1fb4649b612fac7b4ee613df6f6b7d921ddd6b0d/code/system-contracts/bootloader/bootloader.yul#L551-L633

// @dev Function responsible for processing the transaction
function processTx(
  txDataOffset, 
  resultPtr,
  transactionIndex,
  isETHCall,
  gasPerPubdata  
) {
  // ... transaction processing logic
}

The processTx method and associated transaction handling logic is complex and security-critical. A formally verified implementation would prevent bugs here.

Signature verification - https://github.com/code-423n4/2023-10-zksync/blob/1fb4649b612fac7b4ee613df6f6b7d921ddd6b0d/code/system-contracts/bootloader/bootloader.yul#L771-L782

// @dev Saves the paymaster context and checks the signature is valid
function storePaymasterContextAndCheckMagic() {
  // ... signature verification  
}

The signature validation logic should be formally verified to ensure it is correctly implemented.

Authentication logic - https://github.com/code-423n4/2023-10-zksync/blob/1fb4649b612fac7b4ee613df6f6b7d921ddd6b0d/code/system-contracts/bootloader/bootloader.yul#L2194-L2216

// @dev Validates the transaction against the senders' account.  
function accountValidateTx(txDataOffset) {
  // ... authentication logic
}

The account validation and authentication logic requires formal verification to avoid issues.

Using an existing formally verified system like Certora, DappHub's Hevm, or custom proving over the code would significantly improve security and confidence.

So in summary, all transactional logic, signature checking, authentication, etc should leverage formal verification techniques to avoid relying solely on test coverage.

Benefits of formal verification:

Transaction processing:

Involves complex application logic and EVM intricacies
Bugs could lead to loss of funds or data corruption
Formal proofs on core logic would prevent flaws
Can verify edge cases like gas usage, reentrancy, etc

Signature validation:

Signatures are a frequent source of vulnerabilities
Tools like ECDSA Fuzzer find common pitfalls
Formal proofs would guarantee signature validation works as intended

Authentication:

Flaws can allow unauthorized access or account theft
Formal modelling proves access controls are properly enforced
Important for financial logic to be precisely correct

Overall, the high complexity and financial stakes mean gaps in test coverage are unacceptable.

Formal verification provides mathematical guarantees that the implemented logic matches the specifications, meeting a much higher bar for reliability and security.

Leveraging verification tools would significantly improve confidence in the system, preventing subtle but critical bugs that can lead to loss of funds.

Let's look at the signature validation logic:

// @dev Checks signature is valid after paymaster call
function storePaymasterContextAndCheckMagic() {

  // Copy magic value from return data
  returndatacopy(0, 0, 32)  
  let magic = mload(0)

  // Check magic matches expected
  if (magic != EXPECTED_MAGIC) {
    revert("Invalid magic value");
  }

  // Use signature

}

This compares the magic return value to an expected constant.

A flaw is that it does not check the length of the returndata before copying.

An exploit would be:

Attacker paymaster returns data less than 32 bytes
Copying will read corrupted memory
Magic check passes even though signature is invalid

This bug could be missed in testing but would be caught by formal verification:

// Formal spec
invariant validSignature() 
  requires validReturndataLength()

function validReturndataLength() {
  return (returndatasize() >= 32)
}

The invariant states the signature must be validated only if the returndata length satisfies the validity condition. Trying to verify the copy logic would fail, proving there is a case where the invariant can be violated.

This demonstrates how formal specifications can catch flaws even in simple logic that traditional testing may miss.

So for critical code, formal proofs provide a significantly higher bar of assurance and should always be applied.

Tools Used

Manual

Recommended Mitigation Steps

Using an existing formally verified system like Certora, DappHub's Hevm, or custom proving over the code would significantly improve security and confidence.