Automated Detection of Dynamic State Access in Solidity

Automated Detection of Dynamic State Access in Solidity

Introduction

Deciding to support only static state access (SSA) or to support full dynamic state access (DSA) is one of the remaining open questions on the Eth2 roadmap. If a purely SSA system proves feasible, there are a number of benefits that simplify:

  • State providers;
  • Synchronous communication between execution environments;
  • Account abstraction; and
  • Transaction pools, witness aggregation and refreshes.

Continuing the exploration of state provider models described earlier, we have roughly prototyped a modification to the solidity compiler that can detect instances of DSA in smart contracts using taint analysis.

This proof of concept shows that it is possible to build tooling to support a purely SSA Ethereum.

Background

State Access & Witnesses

For the direct push state provider model to work, the actor creating the transaction should be able to build a witness (such as a Merkle proof) to every storage location the transaction will read or write. If the transaction does read from or write to a location not included in the witness, the transaction is reverted, and its fees are forfeit.

DSA is a particularly problematic issue that can lead to an insufficient witness. In concrete terms, DSA occurs when the offset argument to sload or sstore is influenced by a previous sload result.

A short classification of some types of DSA, with solidity examples, can be found here.

Yul Language

Example code in this article is written in pseudocode loosely resembling EVM-flavored Yul, an internal representation language used in the solidity compiler. The prototype is written as an optimization pass that operates on Yul.

Taint Analysis

Taint analysis (or taint checking) is a type of data flow analysis where “taint” flows from an upstream source into all downstream variables. It is commonly used in web applications, where user supplied values (like headers) are the source of taint, and variables used in database queries are verified to be taint-free.

In a compiled language, it is conceptually similar to symbolic execution, though much less complex.

Consider the following example, where value is tainted by an sload:

function tweedle() -> twixt
{
    let zero := 0
    let value := sload(zero)
    let dee := 45
    let dum := add(dee, value)
    let rattle := 88
    
    let selector := gt(dum, 100)
    
    switch selector
    case 0 {
        twixt := dee
    }
    default {
        twixt := rattle
    }
}

The graph below shows the flow of taint from value all the way to twixt. Red nodes and edges indicate taint, and dotted lines represent indirect influence (in this case, through the switch.)

00-tweedle

Prototype

Implementation

Implementation source code is available for solidity 0.5 and for solidity 0.6, though not all features are implemented on both branches. Test cases can be found here, though not all successfully pass. This prototype is built as a Yul optimization pass, and so requires --optimize-yul --ir as additional compiler flags.

Since this is a proof of concept, the output is messy and barely readable, the implementation is inefficient, and is 100% capable of summoning nasal demons. Obviously, don’t use this software in any kind of production environment.

The analysis can be split into three conceptual phases: data gathering, function resolution, and taint checking.

Data Gathering

In the data gathering phase, the analyzer visits each node in the Yul abstract syntax tree (AST). This phase accomplishes several goals:

  • Creates a scope for each function;
  • Tracks variable assignments, declarations, and function calls;
  • Tracks return variables and arguments of sload and sstore;
  • Resolves the effects of built-in functions (ex. add, iszero);
  • Propagates constant values; and
  • Converts memory accesses into special variables.

The following is a simplified example of the information collected for the given input:

{
    let zero := 0
    let ret_0 := fun_narf_19()
    sstore(ret_0, zero)

    function fun_narf_19() -> vloc__4
    {
        let addr := 97
        let foo_0 := 54
        let foo_1 := sload(addr)

        vloc__4 := add(foo_0, foo_1)
    }
}

The collected output:

Known Variables:
    addr         [constant=97] [Untaintable]
    ret_0                      [Untaintable]
    zero         [constant=0]
    vloc__4
    foo_0        [constant=54]
    foo_1                      [Tainted]
    !!block_0    [constant]

Functions:
	!!main() -> 
		Data Flow:
			!!block_0            -> zero, ret_0, 
		Unresolved Function Calls:
			- fun_narf_19

	fun_narf_19() -> vloc__4, 
		Data Flow:
			addr                 -> foo_1,
			foo_1                -> vloc__4, 
			foo_0                -> vloc__4, 
			!!block_0            -> addr, foo_1, foo_0, vloc__4,

01-split

The variable !!block_0 is synthesized to represent indirect influence, such as if statements and loops. This example does not contain any indirect influence, though the block variables are still created. The !!main function represents statements not contained in any other function, like the sstore in the example code.

Data flow, in the example output, shows how data flows from upstream variables (to the left of ->) to downstream variables (on the right.)

Note that fun_narf_19 is listed as an unresolved function call.

A Note on Memory

Memory accesses are tracked by synthesizing variables (ex. !!m0) for every mstore, similar to how compilers convert to single static assignment form. This process relies on very basic constant folding. Should an mstore or an mload access an offset which is not computable at compile time or has not been written to yet, a catch-all variable !!memory is used instead.

Function Resolution

The function resolution phase iteratively embeds callee function scopes into the caller’s scope, uniquely renaming variables in the data flow graph. Embedding functions in this way allows accurate tracing between arguments and return variables.

Continuing with the above example, the data flow graph after this phase looks like:

Functions:
	!!main() -> 
		Data Flow:
			!!block_0            -> zero, ret_0, addr_embed0, foo_1_embed1, foo_0_embed3, vloc__4_embed2
			addr_embed0          -> foo_1_embed1,
			foo_1_embed1         -> vloc__4_embed2,
			foo_0_embed3         -> vloc__4_embed2,
			vloc__4_embed2       -> ret_0

Taint Checking

Last, and probably simplest, is taint checking. This phase walks through the data flow graph, tainting every variable that is reachable from an initially tainted variable.

Once the taint is propagated, the “protected” variables (variables used as the key argument to an sload or sstore) are checked for taint. If tainted protected variables are found, a taint violation exception is thrown.

In this example, ret_0 is both protected and tainted.

Limitations & Future Work

Click to expand...

Call Graph Cycles

A call graph cycle happens when a function foo calls a function bar and bar also calls foo. For example:

function foo(arg0) -> ret0 {
    switch arg0
    case 0 {
        ret0 := bar()
    }
    default {
        ret0 := 1
    }
}

function bar() -> ret1 {
    ret1 := foo(1)
}

Cycles in the call graph currently cause the prototype to loop infinitely. It should be possible to break these cycles by assuming all parameters of one function influence all of that function’s return variables.

Constant Propagation

Constant propagation is the process of substituting the values of known constants in expressions at compile time.

This prototype implements a very limited form of constant propagation to support the mstore and mload instructions. If the offset argument to mstore or mload can be computed at compile time, the taint analysis through memory is more accurate (fewer misleading taint violations.)

Calling Contracts

The builtin functions to call other contracts are disabled in the prototype. Enabling them requires further thought on the ABI between contracts.

Currently the prototype assumes that call data opcodes (CALLDATALOAD, CALLDATASIZE, CALLDATACOPY, etc) return untainted data. If a contract calls another contract, that assumption is invalidated.

Control Flow

The approach taken in this prototype to handle control flow and branching (synthesizing !!block variables) is insufficient to accurately trace taint through loops.

Consider the following:

function fizzbuzz() {
    for { } 1 { }
    {
        let zero := 0
        let foo := sload(zero)
        let cond := eq(foo, zero)
        if cond {
            break
        }
    }
}

Which roughly translates to the following data flow graph:

04-flow

zero is not influenced by !!block_0 between where it is assigned and where it is used for sload. In other words, zero is not dependent on storage[0] at the time sload is called, even though the data flow graph thinks it is.

Bit-Accurate Taint

Variables in the prototype are tracked as an indivisible unit, which may be tainted or clean. Tracking each bit of a variable separately enables more accurate analysis.

This improvement is particularly relevant when using boolean operations (like or & and) and the mload instruction with non-256 bit types.

For example, the following snippet does not exhibit any DSA, though the prototype will report a taint violation:

function fizzbuzz(value)
{
    // Place a constant byte into memory.
    mstore(0, 0xAB)
    
    // Read a value from storage, place it into memory. This
    // taints memory offsets 1 through 32 inclusive. 
    let from_storage := sload(0)
    mstore(1, from_storage)
    
    // Get the constant back from memory.
    let mem_tainted := mload(0)
    let mem_cleaned := and(mem_tainted, 0xFF)
    
    sstore(mem_cleaned, 0xC0FFEE)
}

After execution, the first 33 bytes of memory look like:

Since mload(0) populates mem_tainted with the first 32 bytes of memory, mem_tainted contains 31 tainted bytes (all bytes after memory[0]). mem_cleaned, on the other hand, contains no tainted bytes, since only the first byte can influence its value; the other bits are masked out by and.

Unimplemented Features in Yul

The solidity compiler’s Yul implementation doesn’t yet support libraries. This makes analyzing existing contracts tedious at best.

Conclusions

Although the limitations mentioned above present challenges for analyzing existing contracts for DSA, we believe that existing compilers can be extended, with reasonable effort, to detect and prevent DSA while maintaining features. Furthermore, given the ease of inadvertently introducing DSA, we believe that adding this feature to smart contract compilers is necessary to write secure code.

One contract, part of @PhABC’s uniswap-solidity, did successfully compile with minimal modification.

A big thanks to Quilt for supporting this research and providing invaluable review and feedback.

8 Likes

Please see Rice’s Theorem.

AFAIK, the plan is to enforce access lists when necessary. An alternative we considered was to introduce new syntax to give us the properties we want, but this would have too many disadvantages.

Please see Rice’s Theorem.

I’m not at all familiar with Rice’s Theorem, and from a quick read, it does seem applicable. However, I’m not sure where it breaks taint analysis.

Are you implying that this approach will report falsely tainted variables, or that it is impossible to prevent false negatives? I believe the former is acceptable (as long as the language provides an escape hatch), and that the latter is unacceptable.

AFAIK, the plan is to enforce access lists when necessary.

Proofs/witnesses form a sort of informal access list which gets “checked” as the transaction is executed. I don’t see how this would be avoidable.

How will developers know if their access lists are complete? If an earlier transaction in the block can invalidate your access list, I think that’s a bug in your contract and we should endeavor to prevent it.

An alternative we considered was to introduce new syntax to give us the properties we want, but this would have too many disadvantages.

What disadvantages? Was there a write-up or post about it? I’d love to learn more about it.

This is true, but this is missing some cases!

I know this is early work, but for the sake of completeness I thought it might be useful to enumerate all the other causes of DSA which I could think of.

Well, first, let me write out what I think the different kinds of state access are, let me know if I’m misunderstanding your terms:

  • SSA: The transaction specifies a short list of addresses and storage items it might touch (read or write).
    • for example: BALANCE > 1000 ? SSTORE[0] = 1 : SSTORE[1] = 1.
  • “large bound state accesses” (LBSA?): transactions for which the set of accounts/storage items it might touch is bounded, but too large to provide a witness for.
    • for example: I might call BLOCKHASH and depending on the result send a reward to any one of a thousand beneficiaries. It would be very expensive to provide a witness for all thousand of them!
  • DSA: The set of addresses the transaction might touch to is [0,2^{160}-1], or the set of storage items the transaction might touch is [0,2^{256}-1]. We have no idea what the transaction might try to access.
    • for example: SSTORE[SSLOAD[0]] = 1

There are some additional causes of full DSA:

  • The COINBASE opcode can’t be predicted at witness-creation time, and returns an address the transaction could try to interact with.

  • I might call BLOCKHASH (which can’t be predicted during witness creation) and treat the result as an address and try to send eth to that address. This will almost certainly fail, but proving that it fails requires a witness from the relevant part of the account trie.

  • I might call BLOCKHASH and use it to derive the salt for a call to CREATE2. This will result in the account being created at a completely unpredictable location.

  • Due to the Wild Magic shenanigans which CREATE2 enables, other contracts might entirely change between the time of witness creation and the time the txn makes it to the blockchain:

    • If the txn reads an address out of the result of EXTCODECOPY, that could cause full DSA.
    • If the txn calls any of the CALL opcodes (even STATICCALL) on a wild magic contract that contract could do anything, easily invalidating the transaction’s witness.

There are some potential sources of “LBSA”:

  • BALANCE returns your current balance, which might change between witness generation and transaction confirmation, someone might send your address ETH. So, SLOAD[BALANCE] could attempt to access any of a large variety of storage items.

  • Other opcodes have the same property: TIMESTAMP, NUMBER, DIFFICULTY, GASLIMIT. None of them can be predicted ahead of time (except possibly NUMBER) and and of them could be the target of an SLOAD.

  • GAS is also tricky. Even if you can know for sure wihch set of accounts / storage items that a call to CALL will touch, the values of those storage items can change how much gas the call consumes. This means the result of GAS cannot be known ahead of time.

There are also some additional complications:

  • The initcode passed to CREATE and CREATE2 has all of the same considerations, they also need to be analyzed.

  • In the general case it’s difficult to even construct a witness. Say that you have access to the entire state trie and you want to create a witness for a transaction, you would need to do something very fancy to determine which accounts might be accessed by the transaction, given that you don’t know the results of all the opcodes mentioned above.

  • It’s not just SLOAD which can read from different parts of the state trie. EXTCODESIZE, for instance, can also read from arbitrary parts of the account trie. EXTCODESIZE[BLOCKHASH] can read from almost anywhere, and proving that the result ought to be 0 requires proving that part of the state tree.

Anyway, I’m sure that most of this is already on your TODO list, posting it because there might be something here which hasn’t already surfaced.

Thank you so much for posting your thoughts! This is a great comment.

You are correct, there are quite a few other sources of taint: GAS, call and return data, balances, block hash and so on.

You have to be careful including the size of the access list as part of the definition of dynamic state access. If a contract conditionally pays to an address (ex. a smart wallet), the size difference between the minimal guaranteed-complete witness and the naive include-all-addresses witness could be significant.

In these case, we would still call this dynamic state access. I’ve used the phase “branched state access” to refer to this category.

To us, static state accesses are only accesses that are absolutely independent of other state accesses. Everything else falls under the umbrella of dynamic state access.

We’ve been calling this arbitrary state access.

Yep! These are all sources of taint. I don’t think there’s anything particularly problematic here, the analysis just needs to be aware of them.

Could you expand on this a little bit? I’m not familiar enough with the contract creation opcodes to comment.

I think witness creation will either need to be handled by the contract developers (say, for example, with a wallet plugin), or by simply running the transaction and collecting state accesses as it goes. If we can avoid DSA in smart contracts, the latter should be sufficient to generate a minimal guaranteed-complete witness.

This is harder than you’re making it sound!

witness creation will either need to be handled by the contract developers (say, for example, with a wallet plugin)

This works in the very simple cases. It’s probably feasible in the harder cases, though I don’t envy the developers of more complicated contracts. However, once your contract calls into another contract we’re back to where we started, it’s going to be very difficult to figure out the set of accounts/storage-slots that the other contract you didn’t write might touch.

simply running the transaction and collecting state accesses as it goes

This also works in the simple case. But say I have a contract which has a conditional (maybe based on a read from BLOCKHASH and based on the result might update one storage slot or the other. The witness has a 50% chance of being wrong! I had thought SSA meant it was possible to specify a set of accounts which the transaction might touch. You’re talking about not allowing any flexibility at all! I would be surprised if it was possible to add this restriction without breaking a ton of existing contracts.

This isn’t very exciting, it’s just another place which needs to be taken into account! When you call CREATE you provide some code (called initcode) which is executed, and the result of executing that initcode is what becomes the code of the newly created contract.

This initcode also needs to be inspected, if you want to find all the places we currently perform DSA!

This is exactly why, for the direct push model, we believe we have to eliminate all types of dynamic state access. Obviously arbitrary state access is a problem, but even simple branching is an issue because the set of all possible locations could become quite large compared to the minimal set.

That is essentially correct. For new contracts there are some workarounds, but we aren’t convinced that they are sufficient for a good developer experience. That is what motivated this prototype.

@adietrichs and @villanuevawill are manually auditing some contracts to see what changes they’d need to be rewritten without DSA, but it’s unlikely that contracts could be ported without modification.

Getting Eth1 into Eth2 is going to be a whole process on its own, and at least one of the proposals would require semi-statefulness for Eth1 contracts.

In short, this post is far from a statement that Eth2 should abandon support for DSA. It makes the much smaller claim that compilers can (probably) detect DSA, should we choose to go in that direction.

1 Like

Yeah, totally, the set of potential accesses can grow quite quickly.

ahhhh, thanks for this! I missed this somehow. I agree compilers can probably detect it, in most cases.

In this situation, I think Rice’s Theorem implies that the compiler can’t detect it perfectly. There are going to be some cases where the compiler can say “DSA happens”, and some cases where the compiler can say “DSA definitely does not happen”, but there are always going to be some cases where the compiler has to say “I don’t know”. Rice’s Theorem tells you the third set must exist, but I don’t think it says anything about how big that set is! It might be possible to write something which correctly bins all existing contracts.

1 Like