Finding and Understanding Miscompilation Bugs in the Solidity Compiler Bhargava Shastry1 1
Ethereum Foundation, [email protected]
arXiv:2607.07217v1 [cs.SE] 8 Jul 2026
Abstract
ming languages like Solidity and are executed on the Ethereum blockchain. The compiler is responsible for translating the high-level smart contract code written in Solidity into bytecode that can be executed on the Ethereum Virtual Machine (EVM). It is no surprise that compilers for smart contracts, like any complex software system, contain bugs. In this paper, we look specifically at miscompilation bugs: compiler defects that result in incorrect code generation. Miscompilations are dangerous in general because they may go unnoticed unless the compiled code has been thoroughly tested. Miscompilations of smart contracts deployed on the Ethereum blockchain are particularly problematic because (1) deployed code is immutable (bugs persist); (2) they may alter the blockchain’s persistent state (side effects of bugs persist); and (3) side-effects routinely include financial transactions (sending/receiving Ether or other ERC20 tokens). In our experience, miscompilations occur due to two main reasons: incorrect optimization and incorrect translation. Miscompilations due to incorrect optimizations occur for the following reasons. First, if optimization correctness checks are either inadequate or not thoroughly tested such that in most cases the optimization produces the desired output with the exception of corner cases. Second, if a formally verified optimization rule is correct in theory but incorrect in practice (e.g., function side-effects are not taken into account leading to more aggressive optimization than permissible). Third, if wrong assumptions are made on the code to be optimized (e.g., may conditions are assumed to be must). Mis-
Smart contract compilers are critical to ensuring the correctness of public blockchains whose defining characteristics are open-source and immutable code. We created SolSmith, a semantics-aware differential fuzz testing tool, to improve the quality of the Solidity compiler—the most popular compiler for the Ethereum blockchain—and spent over three years finding compiler defects that produce incorrect code. We call these defects miscompilation bugs. During this time period, we have discovered 25 miscompilation bugs that went unnoticed, some for multiple years. Our first contribution is to make compiler testing more rigorous. SolSmith achieves this goal by generating valid test programs that are likely to stress test code generation and optimization components. This helps SolSmith find bugs missed during routine testing that could potentially have serious implications for smart contracts and their users. Our second contribution is a qualitative and quantitative analysis of miscompilation bugs that we found in the Solidity compiler. We classify miscompilation bugs found by SolSmith based on their nature, root-causes, and impact on end-users. This sheds light on some pitfalls of optimizing compilers.
1
Introduction
Smart contracts are programs that codify the terms of an agreement between contracting parties. They are written in domain-specific program1
compilations due to incorrect translation occur either due to implementation flaws or inconsistent cleanup of typed data. Verifying the correctness of the compiler is challenging, and traditional testing methods, such as writing unit and end-to-end tests, have limited effectiveness because they do not fully tease out compiler output for diverse programs. Blackbox fuzz testing— simply generating random input—is of little value when it comes to compiler testing if the goal is to find miscompilation bugs. This is because the test input needs to trigger code generation to be able to test for correct compilation and this is highly unlikely to occur when the input to the compiler is a random sequence of bytes. In order for a test input to cause the compiler to emit code, it must do something within the semantic rules of the programming language. Otherwise, the compiler errors. To trigger code generation, some form of semantic awareness is required. One of the forms of whitebox fuzz testing that have been proposed to test compilers involve generating programs based on the language’s context-free grammar [1]. Although whitebox fuzzing techniques perform slightly better than blackbox approaches, they rarely trigger code generation because of semantic errors such as mismatched types, incorrect statement placement etc. Our hypothesis is that semantic expressiveness of test input is correlated with its bug finding potential. We create SolSmith for finding miscompilation bugs in the Solidity compiler, the most popular smart contract compiler for the Ethereum blockchain. We discover two classes of miscompilation bugs: (1) Incorrect code due to faulty program translation; (2) Incorrect code due to faulty program optimization. SolSmith pseudo-randomly generates semantically correct Solidity programs and invokes the compiler against them. The testing is differential in nature. The compiler is invoked twice for the same input program but in non-identical compiler configurations, namely the control configuration (C) and the experiment configuration (E). The configurations are chosen such that they differ in exactly one setting that controls a specific function of the compiler that is to be tested. Each invocation produces bytecode that is run on a production EVM in an identical
state. The two runs are traced at runtime to obtain execution traces corresponding to configurations C and E. Normally, both runs should result in an identical execution trace because the compiler is expected to preserve program semantics during compilation. If traces are non-identical, the input program and the compiler configurations are saved to validate if the divergence is due to a miscompilation bug or not. We find miscompilation bugs of class 2 (incorrect optimization) by comparing the runtime of unoptimized and optimized invocations of the compiler. Finding miscompilation bugs of class 1 (incorrect translation) is tricky because we need a suitable baseline implementation. To do this, we leverage existing alternative (semantics preserving) implementations of the code generator (legacy and IR-based); one is chosen as the baseline while the other as experiment configuration. Using the proposed method, we have identified 25 miscompilation bugs in the compiler that have been patched. Because random testing lends itself well to automation, we have been using it as part of the development life-cycle of the compiler to identify bugs as early as possible. Listing 1 illustrates a miscompilation bug for a semantically valid program written in the Yul IR language. The Yul program contains a function byteIndexedBy(n) that returns the nth byte of the constant 256-bit (32-byte) value 31 indexed by its input argument n. The output of this function invoked with 1 as the input parameter is written to the EVM blockchain’s persistent storage slot zero in the subsequent line. Since the 256-bit value 31 may be represented by 0000...1f (first 31 most significant bytes zeroes, the least MSB non-zero), and indexing starts from the most significant byte (index zero), the function call must return the value zero. However, this program compiled using the Solidity compiler version 0.5.5 would return one. The miscompilation occurred due to an optimization rule that transforms byte accesses of constant values into a mask (and(value, 0xff )). The rule targeted the wrong input argument for optimization: instead of targeting byte(31, X) (X being the constant expression) for optimization, the rule targeted byte(X, 31) and transformed it into and(X, 0xff ) Therefore, byte(n, 31) is evaluated as byte(31, n) yielding the value 2
one instead of the correct value of zero. This paper makes two contributions. Our first contribution is to make compiler testing more rigorous by generating expressive source programs and executing their compilation output differentially. SolSmith has found 25 miscompilation bugs in over three years of testing, some of which were discovered during continuous integration i.e., while a pull request was being reviewed. Our second contribution is a qualitative analysis of miscompilation bugs found by SolSmith: Where are they present? What is their rootcause? How do they affect end-users? We find that (1) close to two thirds of miscompilation bugs occur due to incorrect optimization, and the rest due to incorrect code translation; (2) miscompilation bugs due to incorrect optimization mostly occur because of underconstrained application of an optimization rule; (3) miscompilation bugs found by SolSmith have not been externally reported to us leading us to believe our effort is proactive.
2
increase the test coverage of the JS interpreter; it is not evaluated whether the proposed approach affects bug-finding ability or if it actually discovers miscompilation bugs as defined by our work. JS programs are generated using the context-free grammar and the constraint-solver is used to prune generations such that they stay syntactically valid. In contrast, SolSmith generates context-sensitive programs that respect language semantics (e.g., a break statement may only be inserted inside a loop statement, type checking on variables must pass etc.). More importantly, SolSmith is tailored to discover miscompilation bugs. CSmith [3] is a differential testing tool targeted at C compilers, and closest to our work. It generates test programs that respect the C language semantics (e.g., no undefined behavior, type safety respected etc.) and finds bugs by comparing the runtimes of binaries generated by multiple compiler implementations. The scope of that work is to find bugs in any C compiler unlike our aim of finding bugs in the Solidity compiler. The biggest difference between CSmith and SolSmith is that the latter benefits from domain-knowledge: generations and mutations that actually test specific optimization steps are implemented. For example, to test the redundant write-tomemory eliminator (that removes redundant writes to memory as the name suggests), writes to memory are generated that are later either read-from or notread-from testing whether the test cases containing non-redundant write and redundant writes respectively do not lead to incorrect code generation i.e., a non-redundant write being wrongly removed. Equivalent Modulo Inputs (EMI) [4] is a compiler testing method that involves feeding multiple semantics-preserving programs to the compiler and checking if they produce the same output to a given set of inputs. This is complementary to random differential testing and may be applied to the inputs generated by SolSmith. Since EMI does not perform differential testing of multiple implementations, it relies quite heavily on the correctness of semanticspreserving mutations. Although certain mutations are easy to implement (e.g., adding/removing dead code), the mutations that would be useful to find bugs in specific optimization routines (e.g., redun-
Related Work
Broadly speaking, there are two directions that have been taken to find miscompilation bugs: (1) Random generational testing; (2) Equivalence modulo inputs.
2.1
Random generational testing
jsfunfuzz [2] is a JavaScript fuzzer that finds miscompilation bugs by targeting Mozilla’s non-standard JavaScript decompiler interface. A randomly generated valid JavaScript program is first compiled, then decompiled to obtain the original source, and finally compiled again to check for syntax errors. This helps discover bugs in the decompiler that would alter the syntax of the original code. Similarly, consistency bugs are reported by the author by checking if two “round-trips” (compilation plus decompilation) produce an identical result. Our work uses a different— arguably more important—notion of a miscompilation bug to mean compiler bugs that affect compilation rather than decompilation. Grammar-based whitebox fuzzing [1] uses a constraint-solver to generate JavaScript programs to 3
Listing 1 Yul code snippet before optimization. 1
{ // Function that outputs the byte indexed by Listing 2 Yul code snippet after optimization. // input n of the constant 1 { 256-bit value 31. // Expected: sstore(0, 0) because the // 0 indexes the most significant 2 second MSB of byte of 31 (= 0). 3 // 31 is zero. // 31 indexes the least // Actual result: sstore(0, 1) because significant byte of 31 (= 31). 4 the optimizer function byteIndexedBy(n) -> o 5 // incorrectly constant folds and { optimizes for the // Optimization rule bug: Swaps 6 // least significant byte of the order of arguments constant 1. // Assumes 32’nd most 7 sstore(0, 1) significant byte of n. 8 } o := byte(n, 31) } // Store function output to slot zero sstore(0, byteIndexedBy(1))
2
3
4
5
6 7 8
9
10 11 12
13 14
}
dancy elimination) require precise program analysis; (width of 1 upto 32 bytes), boolean, address, and lack of precision would lead to false positives. statically sized arrays of static types. An address holds a 20-byte key that could be used to index either a deployed contract or a wallet. Dynamic types 3 Background include variable width bytes or strings, structs, mappings and dynamically sized arrays. A mapping is a In this section, we provide a brief overview of the key-value type. Solidity programming language and the compiler implementation.
3.2
3.1
Solidity Compiler
The Solidity compiler may be viewed as a conjunction of a front-end (FE), middle-end (ME), and a backend (BE). Until the development of the Yul intermediate representation, the Solidity compiler only had a front-end and a back-end. With the production release of the Yul based code generation engine [5], the Solidity compiler supports two compilation pipelines: legacy and IR-based. The two pipelines share the FE and BE. The legacy pipeline comprises the FE and an EVM bytecode based BE. The IR-based pipeline comprises the FE, the IR-based ME, and the BE.
Solidity Programming Language
Solidity is a high-level programming language [5] that is used to develop programs—so-called smart contracts—to be deployed on the Ethereum Virtual Machine (EVM). The compilation entry point is a contract or a library. A contract may contain one of more functions that may accept Ether, EVM’s native currency. There are both statically and dynamically typed variables in Solidity. Static types include integers (both signed and unsigned), fixed width bytes 4
The legacy code generator translates Solidity programs directly to EVM bytecode. The Intermediate Representation (IR) based code generator is based on an IR called Yul. The IR-based code generator translates Solidity programs to Yul, then optimizes it retaining the optimized output in Yul form, and finally assembles optimized Yul to EVM bytecode. Front End The front end parses Solidity source code into an abstract syntax tree (AST) and performs semantic analysis on it. Semantic analysis includes name resolution, type checking, and controlflow checks; it annotates the AST with the information that code generation depends on. Both compilation pipelines consume the same annotated AST, which makes the front end a shared component of the differential test setup.
Figure 1: Finding miscompilation bugs using differential fuzz testing
state. An account state comprises code, storage, nonce, and a balance. Nonce and balance are machine words 1 used to prevent replay attacks and maintain the Ether held by the account. An account may be either be externally owned (EOA) or a smart contract. An EOA is managed by a public-private key pair but contains no code as such. A smart contract contains code (sequence of bytes of EVM bytecode) and can access non-volatile storage. At any given point, the EVM has a singular state. State transitions are governed by transactions. Transactions are of two types: create, and call. The former deploys a smart contract (bytecode) to a new address on the Ethereum blockchain; the latter calls another account. A call is accompanied by transferred balance, gas that limits the call’s access to computational resources, and data (sequence of bytes).
Middle End Yul is an intermediate representation (IR) used for ease of optimizing Solidity programs. It is untyped, data being 256-bit in size. Because Yul contains control-flow constructs like loops, switch statements it permits a higher-level view than EVM bytecode can afford yet is close enough to EVM to ease assembly. The Yul optimizer can perform optimizations that are not possible by the byte code optimizer. Since the Yul IR does not permit arbitrary jumps, function side-effects may be computed. This aids in, for example, re-ordering function calls or removing function calls entirely (e.g., if the result of a single output function call without side-effects is multiplied by zero). Back End The bytecode optimizer optimizes EVM bytecode that is output by either of the two code generation engines.
4
SolSmith
One of the key requirements to find miscompilation bugs is compilability: test programs must compile 3.3 Ethereum Virtual Machine without errors. This rules out black-box fuzzers that do not respect language semantics because although The Ethereum Virtual Machine (EVM) is a diswe may supply these fuzzers with a sampling of valid tributed computing system that maintains a shared input (existing test cases), it is highly unlikely that state and works on the principle of consensus. The they mutate them in a semantics preserving manner. shared state comprises a mapping of accounts that 1 An EVM machine word is 256-bits in size are referenced via 160-bit addresses to their account 5
Thus, we set out to design a white-box fuzzer called language constructs as possible. SolSmith creates SolSmith that understands Solidity syntax as well as programs with the following features: semantics. • contracts and library definitions Successful compilation is not sufficient to find miscompilation bugs because we need a reference for • function definitions what may be deemed correct compilation. Since there • state variables, immutables, and constants is little control over the nature of programs generated by SolSmith, it is impossible to find miscompilations • most kinds of Solidity expressions and statesimply by comparing the output of the compiler for ments a given program with the byte code that the input program is expected to produce. Therefore, we adopt • most kinds of Yul (inline assembly) expressions a runtime testing approach. and statements
4.1
• control flow statements such as if/else if/else, loops, break, continue, return
Differential Fuzz Testing
A miscompilation bug is flagged if two distinct semantics preserving code generation pipelines produce an executable whose runtime semantics differ. We call the baseline the control group, and the test subject the experiment group. Runtime semantics of a compiled smart contract include stateful changes it makes, the returned result of a call initiated against it, and the status of the initiated call. To find miscompilation bugs in the end-to-end code generation, we use Solidity compiler’s legacy code generator implementation as the control group and its new Yul IR-based code generator implementation as the experiment group. To find miscompilation bugs in the Yul optimizer, we use unoptimized code as the control group and the optimized code as the experiment group.
• typed variables covering most kinds of Solidity types • user-defined types such as struct, enum Third, test programs should be constructed incrementally from other test programs. This means that it should be possible to slightly alter an existing (semantically valid) test program to create another (semantically valid) test program. Our hypothesis is that incremental test generation (via mutations) is correlated with bug-finding ability.
4.3
Program Generation and Mutation
SolSmith generates test programs on the basis on language grammar. It synthesizes test cases in a top4.2 Design Goals down manner. Each test case to the compiler is a SolSmith has three main design goals. First, every sequence of Solidity files, each Solidity file may contest program must be semantically valid that has a tain zero or more functions, contracts, libraries, and single interpretation. This imposes two requirements: so on and so forth. A function body is a statement (1) the test program contains no syntax or typing er- block i.e., a sequence of statements. SolSmith suprors; (2) documented divergences in control and ex- ports most statement types defined by the Solidity periment groups that preclude unique interpretation programming language. A contract body may conmust be avoided. A unique interpretation means that tain state variables, constants, immutable variables, the generated byte code has well-defined side effects and zero or more functions that may accept Ether (payable functions) 2 . In addition, a contract may and performs the same computation. Second, generated test programs capture the ex2 A full grammar specification supported by SolSmith may pressiveness of the Solidity programming language. be found at https://github.com/ethereum/solidity/blob/ This means that test programs make use of as many develop/docs/grammar/SolidityParser.g4 6
define a constructor function that constructs the contract for later use. We generate simple forms of inheritance: a contract may derive from another base contract, overriding one or more functions. We also synthesize inline assembly statements based on an independent specification of the Yul syntax. In order to generate error-free test programs, SolSmith defines a type system for the Solidity programming language. The type system is capable of supporting aspects of an object-oriented language (objects, methods, inheritance) by maintaining a record of objects and their methods and typed instance variables. SolSmith maintains a global state in source file scope and multiple local states that refer to records in one of the following scopes: contract, function, and inline assembly block. The global and local states are updated as we generate a new entity. For example, the generation of a contract creates a contract state that will hold entities in its namespace (state variables, user-defined types, constants) that will be generated in the scope of that contract. SolSmith commences test program generation by creating a set of Solidity test files. A test file is created as follows.
3. Since Solidity enforces types rather strictly, a typed expression may only be formed from subexpressions of the same type or another type that is acceptable by the Solidity type checker. To produce type conformant expressions, SolSmith annotates expressions with types (see Section 4.4). 4. Should the chosen term be an inline assembly block, SolSmith starts iterating on a top-level inline assembly terms, the grammar of which is independently specified. As with Solidity statements, it recurses into or discards productions as necessary. Compared to Solidity, inline assembly is untyped and not burdened with as much contextual annotation (e.g., function visibility, mutability) which makes its production rather straightforward. 5. The maximum number of test files per test case is user-controlled. SolSmith nears completion of a test case production once a randomly chosen number of test files have been generated. It writes the test configuration before finalizing a test case. The configuration includes parameters that define the control and experiment groups that are to be differentially tested. This configuration is parsed by the fuzzer test harness which then executes the test accordingly.
1. SolSmith randomly selects a term from the toplevel language grammar and invokes its production. It consults a probability table in order to select a term from the set of all top-level terms. Each term in the language grammar has an associated (user-controlled) probability of being generated. The production is discarded if certain criteria are not met. For example, production of the using...for statement—that declares functional operators on types—is discarded if no function is available for use. If a production is discarded, SolSmith selects another top-level term uniformly at random. SolSmith recurses should the selected term contain itself e.g., block statement within an outer block. Otherwise, it visits the production rule’s right-hand-side term.
Once a test case is generated by SolSmith, it is parsed by the fuzzer harness. The fuzzer harness parses the contracts, libraries, and their functions from the test case. The test configuration defines the control and experiment groups of the differential test. The test harness executes the following steps for each of the two groups. 1. It chooses a contract uniquely at random, and deploys it to the blockchain. 2. It chooses one of the contract’s functions uniquely at random and invokes it with typed arguements to that function which have also been generated randomly.
2. If the selected production has dependencies e.g., function call that requires input arguments, the dependent term is either looked up from the scoped record (e.g., a variable reference in scope) or produced on-the-fly (e.g., literal expression).
3. The output and status code of the function invocation, and the state of the blockchain are preserved for comparison later on. The output is 7
Problem typing errors
Solution type system; lookup table of permissible types type system
Enforcement static
ery generated expression. In addition, it consults a lookup table to choose which expression kinds are suitable for a given type. The lookup table maps a given type to a list of expression lookup tables for that type and their probability of selection. scoping static An expression lookup table maps a given expression errors kind to a set of probabilities for its operand types. unspecified disallow ex- static For example, Solidity’s 256-bit unsigned integer type eval. order pressions with (uint256) can hold arithmetic expressions composed unspecified eval. from other unsigned integer types of various widths; order the lookup table for uint256 therefore admits, among large mem- user-defined dynamic others, arithmetic expressions whose operands are ory expan- upper-bound unsigned integers of at most 256 bits, and encodes sion the probability with which each operand width is sestatic code com- disallow lected. The same mechanism rules out scoping errors: parison only identifiers recorded in one of the currently visible scopes may be referenced by a generated expression. Table 1: Summary of SolSmith’s strategies for avoid- To keep test execution within practical resource liming false positives and code generation errors. its, memory accesses in generated inline assembly are bounded by a user-defined upper limit on memory exa sequence of bytes whose length is specified by pansion that is enforced at runtime. the function output argument list. The status code is an enum that indicate whether the call was successful or not, and if not the reason for Unspecified evaluation order The Solidity lanfailure. The state of the blockchain comprises a guage does not specify the order in which substring representation of the contract storage, the expressions of an expression are evaluated. The two sequence of calls initiated by the called function, code generation pipelines are therefore free to evaluate sub-expressions in different orders, and they do and log data. so in practice. A program whose observable behavA miscompilation is flagged if the control and ex- ior depends on the evaluation order would cause the periment groups diverge in at least one of the com- control and experiment groups to diverge without a pared indicators: output, status code, and blockchain miscompilation being present. SolSmith statically restate. Flagged miscompilations are inspected manu- jects generations that combine multiple side-effecting sub-expressions within a single expression. ally to sort out false positives.
4.4
Filters to Reduce False Positives
Environment-dependent instructions EVM instructions such as gas, pc, and codesize return values that legitimately differ between the control and experiment groups: optimized code consumes less gas, has different program counters, and produces smaller byte code. Comparing the results of such instructions would flag divergences that are not miscompilations. SolSmith therefore excludes the Type and Memory Safety To rule out typing results of such environment-dependent instructions errors, SolSmith’s type system tracks the type of ev- from the compared runtime indicators. Table 1 summarizes the strategies employed by SolSmith to avoid false positives and code generation errors. Most strategies are enforced statically, i.e., during test program generation; the bound on memory expansion is enforced dynamically, i.e., while the compiled test program is executed.
8
4.5
Design Trade-offs
No ground truth Differential testing does not require a specification of correct compilation, but it can only detect divergence, not absolute correctness. A miscompilation that manifests identically in both the control and experiment groups—for instance, a bug in the shared front end—goes unnoticed. We accept this blind spot in exchange for a fully automated test oracle.
Number of miscompilation bugs
No guarantee of termination SolSmith does not statically guarantee that generated programs terminate; for example, generated loops may fail to make progress. We rely on the EVM’s gas metering to bound execution: every execution is supplied a fixed gas budget, and an execution that exhausts its budget is terminated by the EVM. Since gas exhaustion manifests identically in both groups, non-terminating programs do not produce false alarms; they merely test the compiler less effectively. Target miscompilation bugs SolSmith is designed to find miscompilation bugs rather than compiler crashes. Design decisions such as generating well-typed programs reduce the diversity of inputs presented to the compiler front end, which is where crash-inducing inputs are typically rejected. Nonetheless, internal compiler errors are detected as a by-product of testing and constitute a majority of the bugs found by SolSmith (see Section 5.3).
5
Results and Discussion
5.1
Where Are The Bugs?
15
14
10 6 5 3 1
1 ly ze r A na
he
od e C
Ty p
e
C
en e G e
od C
ck er
or ra t
tim iz op
B
yt e
co
de
Yu l
op
tim iz
er
er
0
Component Figure 2: Distribution of miscompilation bugs found by SolSmith across compiler components.
Table 2 characterizes the miscompilation bugs found by SolSmith. Figure 2 shows their distribution across compiler components: over two thirds (17 out of 25) are optimizer bugs, with the Yul optimizer alone accounting for 14. Table 3 breaks the bugs down by root cause. The most common root cause is an insufficient safety check, i.e., an optimization that is correct on most inputs but is applied to inputs on which it is not. Table 4 shows where the bugs are located in the 9
compiler code base: the single buggiest file is the list of algebraic optimization rules (RuleList.h) shared by the Yul and byte code optimizers, followed by the store eliminator optimization steps.
1 2 3 4 5 6
5.2
Examples of Miscompilation Bugs
7 8
Bug 1: incorrect Keccak256 caching (#11131) The keccak256(p, s) hash function is a first-class opcode that computes the hash value of EVM memory region in the byte range [p, p + s], where p, s (start pointer, length) are non-negative integers. We found that the Solidity compiler since its very first release until version 0.8.2 contained a bug that would result in the hash values of overlapping memory regions in successive calls to the keccak function being incorrectly computed. The problem occurred when a call to keccak256(p, s) was followed by another call keccak256(p, s’) such that mod(s, 32) == 0, mod(s’, 32) != 0 (the first but not the second length parameter is a multiple of 32) and s’ < s (the memory region for the second keccak call was contained within the first memory region). The root-cause of the problem was that the Solidity legacy optimizer wrongly rounded up the length argument of the keccak function to the nearest multiple of 32 and in doing so, considered keccak256(p, s) == keccak256(p, s’) although s != s’. This happened because of two reasons: (1) the mistaken assumption that keccak hashes are always computed over memory regions that span a multiple of 32 bytes; (2) keccak256 hash computation of memory regions that may deduced to be the same (i.e., identical start pointer and length rounded upto 32) may be optimized by performing the computation for the first call, caching the computed value, and re-using the cached value for the second call instead of computing it again. The wrong deduction caused the keccak256 hash value computed by line 5 of Listing 3 and subsequently cached to be re-used on line 6, eventually returning true instead of the correct return value false.
9 10
contract C { function f() public returns (bool ret) { assembly { mstore(0, 0) let a := keccak256(0, 32) let b := keccak256(0, 23) ret := eq(a, b) } } }
Bug 2: unaccounted side-effects (#7411) The Yul optimizer encodes an optimization rule that simplifies MUL(X, SHL(Y, 1)) to SHL(Y, X): an expression X multiplied by one left-shifted expression Y times is equal to X left-shifted Y times, eliminating the multiplication. We found a bug in the Yul optimizer shipped with Solidity compiler versions prior to 0.5.12 that would result in functional expressions with side-effects (functions that return a single output and modify shared state) being incorrectly computed. The root-cause of the problem lay in the swapped evaluation order of parameters due to the optimization rule. This happened because in the original code MUL(X, SHL(Y, 1)), the evaluation order in Yul being left-to-right, the expression X was computed before Y, but vice versa in the optimized code SHL(Y, X). Therefore, the result on line 14 of Listing 4 is incorrectly computed as two because the function readValue() is evaluated before the function writeValue(), instead of the other way round as intended in the unoptimized code that would result in the value eight. Although the optimization rule is computationally correct, it does not account for side-effects of expressions that depend on the evaluation order. Interestingly, this optimization rule was proven to be correct using Z3 at the time the bug was found. This is not surprising since the proof does not account for side-effects. Listing 4 The Yul optimizer incorrectly optimizes the function bug() to return two. The correct return value is eight.
Listing 3 Multiple versions of the Solidity compiler miscompiled this function wrongly returning true. The correct return value is false. 10
1 2 3
{ function readValue() -> x {
Component Yul optimizer
Bug location Optimizer rule
Yul optimizer
Expression simplifier
Yul optimizer
Legacy optimizer
Redundant assignment eliminator Dead-code eliminator Optimizer rule
Legacy optimizer
Optimizer rule
Legacy optimizer
Optimizer rule
Yul optimizer
Structural simplifier
Legacy optimizer
Optimizer rule
Yul optimizer Code generator
Redundant store eliminator Yul IR generator
Code generator
Yul IR generator
Code generator
Yul IR generator
Code generator
Yul IR generator
Code generator
Legacy optimizer
Code generator Yul optimizer
Legacy back-end Optimizer rule
Yul optimizer
Redundant store eliminator Redundant store eliminator Loop-invariant mover Redundant assignment eliminator Load Resolver
Incorrect control-flow analysis (#11352)
Type Checker Common subexpression eliminator Redundant store eliminator
Permissive free function definition (#9851) Incorrect code transformation (#9308)
Incorrect computation Incorrect computation Undefined behavior Compiler error
Incorrect removal of store (#13478)
Incorrect state
Yul optimizer
Yul optimizer Yul optimizer Yul optimizer Yul optimizer Front end Yul optimizer Yul optimizer
Bug description Side-effects due to expression re-ordering not accounted for (#7411) Variable reassignments not accounted for (#6127) Side-effects of assignments that access memory not accounted for (#6827) Dead code not properly removed (#6492) Parameter ordering in rule swapped (#6316) Overflow check missing (#6246) Side-effects of expression unaccounted for (#7098) Undefined behavior because of duplicate switch case expressions (#6359) Side-effect of expression unaccounted for (#9558) EVM specification of opcode not respected (#13039) Missing clean-up post casting down to smaller fixed bytes type (#12535) Incorrect forwarding of modifier input parameters (#12061) Missing truncation before shift operation (#11736) Incorrect function forwarding (#11631) Incorrect re-use of cached keccak256 hash value (#11131) Missing clean-up of typed data (#11602) Incorrect transformation function (#9546)
Incorrect data-flow analysis (#12672) Side-effect of expression not accounted for (#7847) Incorrect data-flow analysis (#8072) Incorrect control-flow analysis (#8032)
Table 2: Miscompilation bugs found by SolSmith. 11
Impact Incorrect computation Incorrect computation Incorrect computation Syntactically incorrect transformation Incorrect computation Incorrect computation Incorrect computation Undefined behavior Incorrect computation Incorrect controlflow Incorrect data Incorrect code Incorrect data Incorrect controlflow Incorrect computation Incorrect data Incorrect computation Incorrect computation Incorrect computation Infinite loop
x := sload(0) } function writeValue() -> y { sstore(0, 2) y := sload(0) } function bug() -> z { // Post optimization: z := shl(readValue(), writeValue()) z := mul(writeValue(), shl(readValue(), 1)) }
4 5 6
Bug root cause Insufficient safety check Incorrect analysis Lazy clean-up Implementation flaw Overly permissive parsing Incorrect optimization Total
7
Number 11 4 3 3 3 1 25
8 9 10 11 12 13
14
Table 3: Distribution of the root cause of bugs found by SolSmith.
15 16
}
Bug 3: Incorrect removal of storage writes (#13478) The Yul optimizer contains an optimization pass called unused store eliminator that removes provably redundant writes to storage and memory. We found a bug in the optimization pass shipped with Solidity versions 0.8.13–0.8.16 that would lead to File Name Purpose Num. Bugs an incorrect state of persistent program storage in RuleList.h List of op6 programs containing function calls that would write timization to storage and conditionally terminate. The rootrules cause of the bug lay in not summarizing the effect UnusedStoreEli Optimization 4 of a storage write in conditionally terminating funcminator.cpp pass tions. 2 YulUtilFunctio Solidity to The Yul program in Listing 5 demonstrates the inYul utilities ns.cpp correct storage removal bug. The function f() writes opti6 Misc. Yul op- Yul a one to storage slot zero and then calls the functimization mod- mization tion g(). The latter in turn gracefully returns the passes ules function via the leave statement in case the 32-byte Misc. legacy op- Byte code 3 value at memory location zero is two. Otherwise, timization mod- optimization program execution is terminated (i.e., the top-level ules passes transaction is terminated) via the return statement. 2 Misc. Solidity Code transThe top-level program makes two calls to the functo Yul modules formation tion f(). The compiler generates code that incorMisc. analysis Semantic 2 rectly removes the first write to storage (via the first modules code analysis call to f()). Due to this removal, program persistent Table 4: Distribution of miscompilation bugs found storage is empty should the call to g() via the first top-level call to f() terminate. The correct state of by SolSmith across compiler source files. storage is a one written to slot zero and the compiler must therefore retain the first storage write. The fix for this bug is to add the additional safety check while annotating store statements: if a function may 12
was found in unreleased code, i.e., the defect was caught by SolSmith before it shipped in a compiler Listing 5 The Yul optimizer incorrectly removes the release. first storage write to slot zero resulting in an incorrect blockchain state after conditional program termina- Bug persistence Figure 5 shows how long the mistion. compilation bugs found by SolSmith persisted in the terminate, storage must be retained.
1
function f() { sstore(0, 1) g() } function g() { switch mload(0) case 2 { leave } // terminate execution return(0, 0) } f() f()
3 4 5 6 7 8 9 10 11 12 13 14
code base, measured as the number of days between the change that introduced a bug and its fix, for the 22 bugs whose introducing change we could identify. The median miscompilation bug persisted for 134 days; roughly a third (7 out of 22) persisted for over a year, and the two longest-lived bugs persisted for roughly six (KeccakCaching, 2148 days) and seven (DirtyBytesArrayToStorage, 2597 days) years respectively. This shows that routine testing not only misses miscompilation bugs at the time they are introduced but is unlikely to catch them later: bugs stay hidden until either a fuzzer or—worse—an affected user finds them.
{
2
}
5.3
Longitudinal Analysis
We performed a longitudinal analysis of the Solidity compiler using tests generated by SolSmith. We tested Solidity compiler releases that were made in the past three years and recorded the bugs that were discovered in each of them. We use crash count— number of test cases that lead to an internal compiler error—to gauge the robustness of a release. Since the discovered bugs have now been fixed, we analyze the nature of discovered bugs over the course of several years. Crash count In addition to the 25 miscompilation bugs, SolSmith has found 164 internal compiler errors: inputs on which the compiler terminates abnormally instead of producing output or a diagnostic. Figure 4 shows their distribution across compiler components. The SMT-based model checker and the type checker together account for close to half of the internal compiler errors; both are front end components that every generated program exercises. Figure 3 shows the compiler version in which each internal compiler error was first observed. Notably, the largest single share of internal compiler errors (76)
Bug severity Of the 25 miscompilation bugs found by SolSmith, 8 affected a released compiler version in a manner that warranted a severity rating and a public security alert; the remaining 17 were fixed before they shipped in a release. Figure 6 and Figure 7 show how long these severity-rated bugs persisted in the code base. None of the bugs was rated high or critical severity, chiefly because the affected code patterns were judged unlikely to occur in typical production contracts. The highestrated bug (StorageWriteRemovalBeforeConditionalTermination, rated medium/high) silently removed a storage write, corrupting persistent contract state. Notably, severity is uncorrelated with how long a bug persisted: the two longest-lived bugs were rated medium and low respectively.
6
Conclusion
We created SolSmith to find correctness bugs in the Solidity compiler, the most popular compiler for smart contracts deployed in the public Ethereum blockchain. Using SolSmith, we found over two dozen miscompilation bugs in the Solidity compiler. These bugs are serious because they cause the compiler to
13
76
60
40
20 4 2 4 1 2 3 3 1 1 1 1 3 1
0
8
3 4 4 1 2 4 4 5 2 4 2 1
7
3 2
U
nr
el
ea s 0. ed 5 0. .4 5. 0 7 0. .5.8 5. 0. 10 6 0. .3 6 0. .4 6 0. .6 6 0. .7 6. 0 8 0. .6.9 6 0. .10 6 0. .11 6. 0. 12 7 0. .0 7 0. .1 7 0. .4 7 0. .5 7. 0. 6 8 0. .1 8 0. .2 8 0. .3 8. 0. 4 8 0. .6 8 0 .7 0. .8.9 8 0. .10 8 0. .11 8 0. .15 8. 16
Number of internal compiler errors
80
Compiler version Figure 3: Number of internal compiler errors found by SolSmith per Solidity compiler version. Errors labeled “Unreleased” were found and fixed before they shipped in a release.
14
39
37
1,000
Days
Number of internal compiler errors
40
30 23
22
100
21
20 13 10
9
Figure 6: Number of days a severity-rated miscompilation bug found by SolSmith persisted in the code base (log scale).
SM
T
C Ty hec pe ker C he I ck R B er G yt en ec e od ra Se eGe tor m ne an r tic ato r A na ly ze O r pt im M iz isc er el la ne ou s
10
Days
emit incorrect code in a manner that alters runtime semantics. Although the bugs are serious, SolSmith Component helped soften their impact by finding them early, sometimes during code review. Only about a third Figure 4: Distribution of internal compiler errors (8 out of 25) of miscompilation bugs found were in found by SolSmith across compiler components. production code and assigned a severity rating. Our work demonstrates that it is possible to find miscompilation bugs before they endanger end-users. To find miscompilation bugs, the key problem we solved was to create semantically valid programs that are likely to stress test security critical components of the compiler, while avoiding programs that are likely 1,000 to result in false alarms or typing errors. The key insight of our study is that miscompilations occur due to various reasons such as not anticipating safety checks sufficiently, lazy cleanup of data, and permis100 sive parsing. The cost-benefit analysis of differential fuzz testing for finding miscompilation bugs is promising. The rental costs of the AWS compute instance that was 10 used to find miscompilation bugs over the course of more than three years amount to a little under $15000, suggesting an average computational cost Figure 5: Number of days a miscompilation bug per bug of under $1000. Differential fuzz testing is found by SolSmith persisted in the code base (log not only economically viable but also promotes sescale). cure software development by making it less likely that miscompilation bugs slip to production. Secu15
1,000
Software SolSmith is open source and is developed as part of the Solidity compiler. It is available at https://github.com/ethereum/solidity.
2,1482,597
Very low Low Medium Medium/High
References [1] P. Godefroid, A. Kiezun, and M. Y. Levin, “Grammar-based whitebox fuzzing,” SIGPLAN Not., vol. 43, p. 206–215, jun 2008.
176 100
[2] J. Ruderman, “Fuzzing for javascript correctness.” https://www.squarefree.com/2007/08/ 02/fuzzing-for-correctness/, 2007.
26 15 15 12 14
[3] X. Yang, Y. Chen, E. Eide, and J. Regehr, “Finding and understanding bugs in c compilers,” in Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’11, (New York, NY, USA), p. 283–294, Association for Computing Machinery, 2011.
DirtyBytesArrayToStorage
KeccakCaching
StorageWriteRemovalBeforeConditionalTermination
FreeFunctionRedefinition
DoubleShiftSizeOverflow
IncorrectByteInstructionOptimization
ABIEncoderV2LoopYulOptimizer
10 YulOptimizerRedundantAssignmentBreakContinue
Number of days bug persisted
rity alerts were avoided for two thirds of the miscompilation bugs (17 out of 25) found by SolSmith because they were found before production use.
[4] V. Le, M. Afshari, and Z. Su, “Compiler validation via equivalence modulo inputs,” in Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’14, (New York, NY, USA), p. 216–226, Association for Computing Machinery, 2014. [5] S. Team, “Solidity documentation.” https:// docs.soliditylang.org/en/latest/, 2022.
Bug name Figure 7: Number of days each severity-rated miscompilation bug found by SolSmith persisted in the code base (log scale), shaded by assigned severity.
16