Certora
Published in

Certora

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.

--

--

--

Making trusted blockchain a reality with fully automatic exact verification technology for smart contracts

Recommended from Medium

Lets Change your view about GDB.

OKR Framework — Zimyo

Linux user tries Windows, in 2020

Algorithms Fundamentals: An Overview of the 3 Sorting Algorithms

Blockstack review

What are computer languages? And its types.

MICROSOFT AZURE

How I manage my AWS accounts with Terraform

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store
John Toman

John Toman

More from Medium

Our Take on the Inverse Finance Security Incident: Price Manipulation Attack

How Abracadabra Uses Gelato to Automate Cross-chain Process

Unleashing stETH with APWine

‘Be Optimistic!’: Hacker Returns $15M In ‘Optimism’ Tokens🚨