Storage Proofs Done Wrong: a Case Study

Transcript

All right. Um, hello everyone. Um, I'm Eliani. I'm a smart contract auditor at Chin Security. You might not know us, but you've probably heard of our clients. >> [snorts] >> But um I'm here today basically to tell you about a very interesting and cool bug that was found back in March in a library that was deployed across many many protocols that uh we're using it to operate on L2s and it was used as a as an efficiency solution for bridging compactly many values at once.

uh and a bug in that library meant uh that since you know the values being bridged were very sensitive like voting powers or oracle parameters. It meant that an attacker could basically either uh inflate or skew the price of assets dramatically or it could uh reset somebody else's voting power which could have entailed either some governance takeover on L2s or even loss of funds in the order of a few millions. Luckily uh it was found by a white hat actually a developer a curve a curve it was responsibly disclosed uh to all the protocols that were affected and it was patched and then published so it went

through the canon it went through the happy path and that brings me here that's the reason why I'm here to present it to you so the road map for this presentation is that first I'll cover some technical grounds and explain what are splurge proofs anyway way why are they useful? Uh then we'll try to have a small makeshift mini CTF. I'll present a reduced version of the function of the library that was verifying the Merkel proof and we'll see if I've made it easy or hard enough to spot the bug and then we'll have a few minutes to talk about the takeaways.

So let's start with the technicalities. Who of you already has heard of mele trees? Okay. Okay. That makes [laughter] it easier. Um well, as um as a high level overview, as many of you may already know, uh the point of a Merkel tree is to efficiently being able to prove membership, right? Because you hash many all the leaves which are the members of your set. You hash them instead of sequentially, you hash them in a treel like structure. So that then somebody who wishes to prove inclusion in that set has to provide log n hashes rather than the whole set to reconstruct

the root and the root is the only well root of trust is called in security. It's the trust anchor which is what the verifier needs uh as a as a as a trusted you know value to be able to ver to correctly verify the proofs. Now this is all nice but for our ends a simple Merkel tree is not enough. It doesn't have enough structure and in particular it doesn't allow us to um insert leaves at a specific position. It in other words it doesn't allow us to have an explicit key value mapping. We need something slightly more advanced to to use the position of the leaf as [snorts]

the key. And for that we need a Merkel Patricia tree which is ubiquitous in Ethereum. How many of you have heard of this bad boy? Okay, not bad. Still less than before. [laughter] Not bad. So the point of this tree is exactly to solve the previous problem actually. Um the way I'm showing it to you it's just a radics tree because uh what we are just adding is explicit uh positions within the many possible children position of a certain branch and the path that you follow the children that you follow along the way uh give you the key give you the

position. So in this case the leaf two uh to reach leaf two you have to from the root branch node you have to go to child E and then to child one. Uh I'm talking in hexadimal here. There's 16 children for each branch. And to get to leaf two you have to get the the 15th child of branch B1 and then the second child of branch B2. And that's the key. uh E1 in exodimal is the key that gets you to leave two. Um and then since in this structure uh a branch contains pointers which are hashes to all of its children,

it is enough as a proof to just attach the path itself. Because if you attach B1, the whole branch B1, you're also attaching the hashes of all of its children because that's part of the content. And so yeah, the proof in a merch tree is the path itself that leads to either the node or the leaf. You can prove a node, an intermediate node as well because intermediate nodes can have values. Uh and then to verify you need well a proof and a key which is the path and these both values that are in bold and need to be supplied by the prover by the user which are so to say untrusted

whereas the root is trusted and needs to be you know um correct and then the verification algorithm just outputs 01 depending on whether the proof correctly hashes along the way simple as that now I have skipped [laughter] a few detail details in this uh namely there's an optimization which actually turns this rad x tree into the actual mer patricia tree I won't go over it because I think it's a detail for the for the purposes of this presentation uh those are called extension nodes so there not just branch and leaf nodes there are also extension nodes that allow you to skip across uh uh a straight line sequence so if many branches in a row have only one

child it's a bit of a waste to explicitly have each and every node intermediate node. So what actual meratricia trees have uh is extension nodes in the middle that allow you to you know shortcut your way through and one thing that is very relevant for us is proofs of exclusion. Now since we have explicit positions for each leaf, uh it follows that you can prove that something is in leaf uh [snorts] at position E1 as as is actually the case for leaf 2. But you can also prove that there's nothing in position E 0 for example. How can you

prove that? Well, you can just attach branch B1 and B2. And in branch B2, you can see that the hash zero is empty. it leads nowhere and that's enough that's enough arguments to to tell the verifier that there's nothing in that position. Um something else another reason another way to prove exclusion you can prove that there's nothing at position E11 why because at E1 you already have a leaf so there can't be anything after that so that's the interesting thing about meratricia trees you can al also prove exclusion you can prove that there's nothing in a circosition now why are these trees actually useful uh well they are used very widely across

Ethereum in the core protocol So in particular every account has uh every contract every smart contract has as you all know storage and its storage is indexed by 32 byte keys and it's uh whole contents for verifiability for provability and is actually all is stored in a database on the nodes.

but is also arranged in a merch patricia tree whose root is part of the consensus. We'll get to that later. But the key takeaway is that every contract has storage and you can think of that storage as arranged in a mer patricia tree. Uh which is is nice because then you can prove some storage the value of some storage slots to somebody who has the storage route. Uh another tree that is very widespread in Ethereum is the global state tree is the world state right this guy this tree has uh for every account has a value and the value is the the details the summary

of of that account it can be an EOA or it can be a contract if it's a contract then the storage root field of that account is the root of its storage tree and the good news is that the root of the state tree is uh broadcast and agreed upon through consensus at the end of every block because that is summarizes the world state of Ethereum. So you can find that in the block structure and the block among the many things that you can find in a block is the new uh root storage route is the new route of the state tree.

So the main point is that one can use this route that you can find in the in the latest block in the latest block hash maybe to prove to anybody any storage slot of any contract on on on Ethereum L1. And why is this useful? It's useful because many protocols want to operate on L2s as you all know because L2s are cheap but still they want to keep their main internal accounting on L1 because that's the probably that's the easiest and most reliable place to keep it on.

So many protocols follow a structures roughly like this. I've made up the names of the storage variables but you can think that you know the storage is actually stored on L1 and then on L2 you are just uh exposing some functions that wish to operate on the same view of the storage of the internal accounting without the need to bridge every single value. That's the point of using Merkel trees. You don't want to bridge every single storage value that's relevant. So what you do is you bridge a single value which is the root hash of the world state in Ethereum.

Here I said it's a permissionless function. It's a permission function. It doesn't need to be a permission function because uh the block hash is actually accessible uh programmatically. So you can just bridge that route. And then the userfacing function is something like this. You prove a storage slot. You give a key. You give a path. You give the proof which is the path itself the list of nodes and then you either prove or or it reverts if it's uh if it's uh an invalid proof but that function allows you to prove that a certain storage lot of a certain contract on L1 has this value and then this allows the contract on L2 to act as if it was the contract on L1

just with a cheaper gas. It's it's a clever solution. So uh let's get to the juice. Let's get to the actual library. Okay. Uh that was used. Well, as we said, the L2 contract needs some way to verify a Merkel proof. And it will need a function like this that we've seen before, right? We need a way to verify given a trusted root, it needs to verify that a proof and a key matches right? The one we are interested in uh was actually semantically slightly different but it was effectively the same. It was returning not 01. It was returning the value of the of the storage slot or reverting if the proof was invalid.

And by some semantic uh contract you can say like by semantics of the return value. This function was a solidity function return an empty byte sequence if you prove the exclusion. if you prove that the that there's nothing at the at the path identified by the key. Right? So that's just the semantics of the solidity function. Now what I want to show you is the solidity function itself. Now this is very simplified. Don't worry the the actual thing was three or four times longer and much harder to decrypt. But with this hopefully in my head this was going to be a sort of CTF. I'm not sure this can actually be the case because I've

simplified it a lot and for sure I've introduced more bugs, but I want to show you the the structure of the function and how sneaky and hidden the bug was. So we have a function that's takes a trusted root hash. Uh this is not coming from the user. then uh key and the path which is the proof and it returns uh the value right of the storage slot. So the way to do this is basically to walk down the path that walk down the tree walk down the proof. So there's a for loop that walks through the proof and then at every at every node at every

intermediate node we are wondering is it an extension node? Is it a leaf node? Is it a branch node? You know the high level structure of the body of the for loop is that for every node it's either a extension leaf or no or branch and and then we wrap around and continue the loop. So if it's an extension well if it's an extension we are skipping we are jumping. So there's the there's the possibility that it's skipping past uh our arrival point. So there's a possibility that this is actually proving exclusion. Otherwise, we just follow the extension loop. We increment our loop iterators and we wrap around and continue. Otherwise, if it's a leaf,

well, if it's a leaf, we are ended. We're done. Uh it could be the case that the leaf is came before we expected it, in which case we proved exclusion because we wanted to go further, but we found a leaf on the way, in which case it's exclusion. Otherwise, if it falls exactly where we expect it to, then we prove the inclusion of of that leaf. Otherwise, if it's a branch node, um if we are run out of nodes, it could be that we tried to prove inclusion of that branch node and that's the case. We proved inclusion. Otherwise, well, a branch node has 16 children.

We identify from the key which children we want. This is the only place where we actually get actually read the key with the index. So given that nibble given that index of of the in the in the array of 16 children we verify whether that node actually has a children in that position. If it doesn't we reach a dead end. And this is a valid proof of exclusion in this case. If it does we continue the loop. just uh advance the the loop iteration given this this uh this new ch this new child.

So given this believe me all the checks within the for loop are correct all the conditions for termination for proofs of inclusion proofs of exclusion are correct. I've deleted for visi for readability I've deleted some reverts for you know malformity of the proof but everything within the for loop is correct given this can you see what's wrong I'll give you 10 seconds [laughter] to find something that was dormant for

years Yeah, >> sorry, I can't hear it. >> It's not It's not working. It's not working. >> What happens if the loop exits early? >> Ah, what happens when the loop exits early? Exactly. >> Exactly. You could have [laughter] got this. Yeah, the loop doesn't expect to ever return to ever break out, which would be maybe uh correct if it was checking for one more condition. But the way it is now, the full loop can just run out of nodes.

And if it runs out of nodes, then you see that there's nothing. The function, the programmer did not expect the full loop to to end. it expected to to reach a return or a revert within the loop. So um what does that mean that at the end there's nothing? It means that there's an implicit return in solidity, right? It's solidity syntax. What does implicit return means if the function returns bytes memory means returns an empty byte sequence? What does that mean by the semantics of the function?

Means exclusion. Means that you've fakely proved exclusion of the leaf by just truncating a valid proof of inclusion. You could make this for loop run out of nodes just by truncating the proof. And if it was a valid proof that would have led to a proof of inclusion, well, now you got a proof of exclusion. Right. I want to stress one thing. What does proof of exclusion mean in the term in the context of storage for contracts?

If this value is not present in the storage tree is if it's not initialized, what does that mean in the EVM? It means that it's zero. The default value. That's the correct interpretation for a proof of exclusion of a storage slot. Means that the storage value is zero. So you fakeely proved that any storage slot that you want on Ethereum is zero even if it's not. So yeah, that's a summary of the bug. The function does not expect to break out of the loop, but you can make it break out of the loop by just truncating a valid proof. The implicit return will return something that by the caller will be interpreted as a as a proof of exclusion, which means storage lot equals zero.

And you know since what was being bridged was something quite critical like uh Oracle parameters that could skew the Oracle price or voting powers the consequences as you can imagine were quite dire. Uh yeah, takeaways. Well, oh what happened? [laughter] >> I don't know what. Yeah, maybe this is an old version. Well, I wrote the takeaways maybe 20 minutes ago, so maybe that's a good reason why. Takeaways. Well, get your audits done. This was live in production for years before it was found. And then and then uh I want to stir up a discussion like how do you automate this? How do you verify this

with tools? You can't possibly catch this bug with fuzzing because the fuzzing will never catch like a truncated proof. It's too malicious an example. And how would you verify this with solvers like like Stora or Z3? It's too hard to model well hash functions, but that that you can get away with. It's hard to model loops and it's hard to model memory operations that are done in assembly. So this was not a good fit for for tools for at least sortoriz 3 would have struggled a lot. So so that's my pitch like how would you do this besides manual review besides manual auditing and then yeah thank you presentation is over. I'll take your questions.

[music] [applause] >> Thank you very much I wonderful presentation. friends.