Overly Optimistic Optimizer — Certora Bug Disclosure

John Toman, VP of R&D at Certora, discovered a previously unknown optimization bug in the Solidity compiler (version 8.14 and lower). This bug causes the optimizer to consider some memory operations in inline assembly as being "dead" and remove them. Later operations that would read the values written by these improperly removed memory operations will instead observe the old version of memory.

The Bug

Unlike many of our prior bug disclosures, this bug does not rely on invalid or maliciously crafted inputs; rather, under certain compiler/optimizer settings the Solidity compiler will delete memory operations it (mistakenly) considers as having no effect on final contract output.

In particular, using the new YUL optimizer and legacy code generation (i.e., with compiler flags --optimize and without --via-ir) memory operations (i.e., returndatacopy, mstore, etc.) can be removed from the output of the compiler even when they can affect the execution output. The cause of this bug is where and how the YUL optimizer is run. If an inline assembly block does not mention any Solidity variables, it is assumed to be self-contained. In this case, the YUL optimizer is applied to the inline assembly if it executes in total isolation, i.e., as if execution immediately halted after the last command. Under the above (faulty) assumption, it would be safe to remove commands like mstore if they were provably not read within the block. However, there can be arbitrary code execution after the optimized assembly block completes, some of which could observe the effects of these memory mutations, meaning it is not safe to remove.

Example

The following (trivial) contract demonstrates this bug:

contract Test {
	function test() external {
		assembly {
			mstore(0, 0x123456789abcdef)
		}
		assembly {
			log0(0, 64)
		}
	}     
}

Examining the output of solc8.13 --asm --optimize reveals that the mstore command is missing but the log command remains (and would thus log the incorrect value). You can confirm this behavior yourself using our self-contained proof-of-concept.

While this example is trivial, we have confirmed this bug less trivial examples, including low-level copies from RETURNDATA that are frequently found when performing low-level calls.

Discovering the Bug

This code generation bug was uncovered by running the Certora Prover on the actual compiler output and failing to find the mstore commands expected by our researchers. This bug illustrates the importance of Certora's approach: verifying what you actually run without trusting the compiler.

Conclusion

The Solidity developers have confirmed this bug (which was introduced in Solidity 0.8.13) and fixed it in Solidity version 0.8.15. We thank the Solidity development team for their rapid response and explanation of the circumstances under which this bug occurs.