How to diagnose a faulty compiler: the LLVM bug

Transcript

Hello and welcome to another edition of the Defi Security Summit webinar. Before we start, we have a few announcements. First, we have opened the applications to volunteer in the D5 security summit. So, if you can make it to Bangkok, uh we will appreciate your help. uh we need help in uh checking people in or posting on social media and helping with the setup. If you want to be a part of the community, if you want to get a ticket to DSS, we would appreciate if you apply through our website. And also, we're going to start and publish uh the results of all the speaker applications

starting today. You should get all the results today or tomorrow. Um, I wish you all good luck and hope to see you in Bangkok nonetheless. And for today's webinar, I'm going to pass the stage to Icing Death, an independent security researcher and she's uh has been in the space for a long while in security. Her focus is on fuzzing and manual review and she's one of the members of the fellowship and she's also a member of the D5 security summit steering committee.

Stage is yours. Thanks. Hey everyone, I'm Sing. Thanks for joining us today. Today we're going to talk to the core members of Satara and BGD labs leading to the discovery of a compiler bug in LVM. I'm super excited to welcome uh John Tolman, chief of chief scientist at Satoria and Ernesto, co-founder of BGD Labs as they discuss and delve into how they found the bug in LVM and how they addressed it. Take it away.

Yep. Uh yeah, hello everybody. So yeah, I think first of all I will introduce myself like so as I in that shape like I'm Ernesto. I'm the co-founder of BD Labs and yeah, for those that are maybe not familiar with BD Labs, we are like a development company and our main point of contribution at the moment and and for probably what if those that you know me like yeah know me is because we contribute to a protocol. We are currently like the the team doing core development and all type of yeah security maintenance like tasks on AB

and and well yeah this is this this webinar is about something that we we found together like with other contributors like team during our our work on the protocol and yeah I hope is is interest I think Maybe. Yeah, John, you can introduce yourself. Yeah, sure thing. [clears throat] Hi, I'm John. Uh, I'm the chief scientist at STORA. Uh, like Ernesto and BG Labs. We work with a to provide formal verification and other security services and we were involved in the uh incident that we're going to be talking about today. And thank you for that kind

introduction both uh and death. Yeah. And I think so maybe to talk a bit about the how we are going to structure the the webinar first like so the roles that my team and and myself I had during the detection like how we addressed this bug and how the cert team represented by by young like what what their role was is slightly different. So from our side it was yeah we are application developers mainly like so our role was like on detecting the side of the problem and addressing it on the

initial stage and high level stage on on the basically solidity side and then yeah sa team like help to go quite deep like into the low level like to to actually find the the root cause together with other contributors too. So I will start with like a small like presentation from my side of well to give a bit of more context of how this what happened like and and and how this happened in the context of AB and yeah kind of high level like description of of everything and then yeah John will will continue with more the nitty-gritty details like on the low level side. So yeah, I will share my screen.

Yeah, I hope is it visible? I hope so. Erh yeah so the yeah the from the title of of of the webinar this is like of yeah the course is LBM bug I think that yeah maybe John can explain later on like more in detail what exactly is the LLBM like but basically this is a bug that that appeared like on purely high level of a5 protocol like like AB and and well then we detected it something very very deep on on software which is not specifically like blockchain blockchain base like so

uh yeah as I say I will start a bit with an overview about AB and and the context so yeah first of all like maybe I need to explain a bit of how it works like with when AB wants to do a deployment on on the different blockchains. So basically is a pretty decentralized organization at this moment like so completely independent teams like like mine with BD labs, certo like there is other labs, there is ACI there is like quite a lot of different teams and we contribute in sometimes quite frequently different areas of of the what we call the abdo

in some cases like yeah we need to coordinate quite a lot like so for example development and security even if kind of different areas like they are quite heavily interconnected like so most probably like the the type of process which joins more of these contributors is whenever a expands the protocol to a new blockchain because different to some other defy systems like uh for a which is in the in the lending space like to expand to another network there is quite quite a lot of let's say work to do both on the purely technical side like but also like on the security and the and the quality side.

So um this problem that we detected was I think in the order of one month ago and it was when trying to deploy the AB3 protocol in in the CK sync um blockchain or roll up. So, so yeah, uh yeah uh a bit of this is also very very important even if then John I will will explain more in detail but well CK sync is EBM compatible like like high level EVM compatible roll up meaning that you you write your solidity code and and technically like that EVM solidity code will will be deployed will

actually will be like compile in multiple layers like to a native a native BM of CK sync. So quite different to DBM but yeah technically the behavior of what you compile on the solidity code it should be exactly the same whenever the smart contract goes goes on chain. So as you can see here like there is yeah quite a lot of intermediary steps. So from the solidity side then there is like the intermediary part which is currently mainly dual then it goes to this LLVM inter intermediate representation which this is the one that actually will be the

most interesting like for for this webinar and then there is like still some extra some extra layers until it reaches like the like the CK virtual machine but again I think this is more on on the John side a bit it. So, uh yeah, first of all, like is that how do we yeah how do we end with a bug in production like so [snorts] um whenever we activate like a new network obviously before like reaching like the a being completely active for like end users like to supply assets like to borrow assets or to do any type of operation in the in in the protocol there is like a lot of technical and

security procedures before that. So that involves deploying the the smart contracts first like in obviously in in test nets like running all the all the let's say unit tests and then running some integration tests on fork uh like doing a lot of like reviews of any type both automatic and manual like on on on everything like from the code base itself like to the parameters configurations the assets listed like So basically quite quite a lot of of of processes but uh yeah CK sync actually is not was not different

to this even more like CK sync took uh quite a lot of time because like the tooling well I mean the same same as almost any other network which is newer than Ethereum like the tooling is continuously improving. So uh it took uh quite a while until we reached the the position of saying okay like the the software is completely ready like and actually thanks like to the mother labs teams we who did like a quite impressive effort like of improving that tooling for for multiple months.

But yeah, like at some point like we reached like like a state like of being completely ready to deploy the protocol and we thought that everything was pretty fine like uh so like all the unit tests like that that that we were able to run and and I will elaborate on that further were running fine. things like for example verifying that the the code base the solidity code base was exactly the same in CKC that on other networks where a was deployed the code basically were the same. Uh there was even instances like using the same of other products like using the same code base as of a already

running in CKC and they they also have like the majority of the code that was the same. So yeah, we reach a like a position where like we we felt very confident of activating the pool which means that we need to create like a what we call governance proposal and then the governance smart contracts like execute this governance proposal and factory activate the smart contracts of of AB. So uh yeah like this process of governance like from the moment that we create the proposal being the technical team until it it reaches execution it has like five days of voting period

during which like the other token holders like actually decide if activating it or not. Um so yeah during this period everything like look normal like the tests more like end to end tests that we run in that time in in fork environments for example they look also quite fine. So yeah it was kind of another day in the office like a process that we repeated like in the past for for other networks. Now it arrived the moment like of the activation which means like that a has some onchain automation that like execute this governance proposal and before any type of so when it gets

executed like but both some minutes before that execution and minutes after that execution like is quite common like that teams of that are working more like on on the UI side well a has multiple as to access like but like the one that is run by a lab they usually do like some extra testing more manual testing like of different types of actions and flows. Now the the difference of this testing is that the quite [snorts] frequently it is kind of sever random like scenarios like so slightly more complex that the ones that

are that exist on the base test suite of a and what happens is that they notice like notice like some strange behavior right like on the on how how yeah as they were doing actions like on on on this user interface how like the the user interface were reacting basically. So um yeah immediately we we got contacted on B labs by by a labs and we started talking a bit and and looking at what was happening like so initially looked like that what happened quite frequently that there was like some some issue of

integration with the user interface like usually there are like some helper smart contrast that could create those kind of minor issues but uh Uh soon after like in a matter of well couple of minutes like we noticed like testing certain scenarios like that actually the problem was pretty critical like because the the smart contracept were allowing to do certain operations which they should never allowed to do in in in the other protocol like so we are talking yeah like very low amount of minutes after the activation like when even the pool was not really so public to to any user Like so like all the fans that were

there were purely like testing funds of of the interface team and yeah immediately as we have certain procedures like we decided like to pause the pool first of all because it looked like some critical problem and in parallel think if well think and test if any other pool like production running pools of fab could be affected. by the same weird behavior. Let's let's call it. So those tests were negative which were was pretty expected like given that yeah the other pools are heavily used out there like and this kind of behavior will be

noticeable very very fast but yeah we just didn't know of what was happening. We only knew that it was not good let's say. So yeah the these mechanism that the has which is like a guardian like post the whole pool there were no funds there and then kind of the work started of like figuring out yeah which was the issue like because there was clearly an issue but it was not clear what the issue was. So um this is quite interesting like this part of the analysis like because it yeah it shows in practice on how that how it works. So what what we started by doing was like

between mainly between us like the Abelabs team on that were that actually detected the issue doing the tests and and the Serto team like we started discussing of potential scenarios like because um the characteristics of the of the of the problem were pretty pretty strange for the following reasons like yeah first reason was that yeah Okay, the tests of the proto were working like the basic tests like so that was like a check mark of that it should be fine.

The second which is yeah the most even almost the most clear is that we we are quite strict when we deploy new instances that the code base is exactly the same as in previous instances or whenever there is like certain exception why it's not the same yeah I mean it's pretty pretty transparent on on why it's not the same and usually it's related like with completely minor aspects of of the protocol. So first thing that we we proved was that all the core logic of AB was exactly the same as some other pools.

We also thought about okay it could be some type of configurations like that are yeah more dynamic in nature than the than the code itself. But the configurations and the assets listed for example they were nothing special like they were just standard. So yeah, everything was kind of the same as in another network especially the code and still like the behavior was very very critical like on logic that should be very core to the other protocol. So yeah there there we had kind of a a big issue like and yeah next step was like stop to think a bit more and and high level like our our approach

was to say okay if we assume that the logic somehow is broken we don't know how this logic is broken how um yeah which type of of broken logic it is like because We we knew certain details like for example during those those tests like by doing an action over one asset certain configurations of another asset were getting affected and and high level in in the protocol like this is a very unexpected behavior like because technically the assets configuration wise are pretty isolated like so this was already like a bit of hints on on

where we we needed to look. So yeah, with different types of of hypothesis like we started to to narrow a bit like on which type of logic of the protocol could be affected even if we didn't know at all how or why. Um and as we were like coming up with with hypothesis, we were in parallel defining certain tests that we could do as fast as possible like to to prove those hypothesis right or wrong. So um yeah we iterate a bit on this on this on this process of hypothesis formulation and test and yeah since the very beginning like of

course like one of our hypothesis was that there could be some type of compiler bug. However like in this kind of in this kind of process security processes like of course you need to focus on what is more realistic first like and and only leave like the what is not. so realistic at the end and for pretty obvious reasons. Usually compiler bugs are are are more rare like that some of the other type of bugs like so as we were narrowing more and more like the the source of the bug even of even not knowing the bug like we started to notice that like the compiler bug hypothesis was more and more realistic

because again like when you have exactly the same logic as in another network when you even have like another product on the same network with the same code base and the same logic and it has no problem like so then is very clearly something that is specific to to your own code and to most probably like how that code is actually running on the blockchain which is the compiler version. So at that point yeah we we were yeah we we isolated like to one single smart contract which John will explain yes very soon which is called the user configuration and our hypothesis was there is for sure

like some type of bug on the compiler we don't know in which in which layer of the compiler of of the picture that I showed before but yeah it was fairly here and then uh yeah like the work actually swapped a bit. So we request like the structural team which has better expertise than us like in compile in compiler stage like to to research like more in deep to detect the the root of the issue together with yeah mother labs on on their own side like which basically they are the the experts on that blockchain to also in parallel like try to find out like what what would be the exact problem and then yeah kind of

the the adventure start life on from the certo side. So I think yeah John if you can go and there we go. Yeah. Thank you Ernesto. Well, as Ernesto mentioned, uh, Stora and myself specifically got rope, not roped in, excuse me, were called in to start diagnosing where actually the low-level

bug occurred. And that is what this subsection of the talk will be about. So, uh, this is not the agenda for the whole talk, but rather for this little bit where I am going to be speaking about the actual low-level details. start out with some quick background uh elaborating a little bit on what Ernesto was saying about how there are these uh asset configurations and different assets were being changed when only one asset should have been changed and then describing how we actually spun through the assembly code to find the cause of this unexpected behavior. And then I think Ernesto and I will both be discussing a little bit the takeaways and the lessons learned about this particular anecdote.

So the piece of code that Ernesto was referring to is what's called the user configuration map. This there is one such configuration map for every single user and it maps for every single reserve whether or not the user is either uh borrowing from that reserve or whether or not it's using that reserve as collateral. Now here the reserves are given just indices starting from zero but these reserves these indexes correspond to some asset on chain like USDC a token frack so on now again despite its name this is actually not a mapping in solidity but a

bit vector and we see that the status for reserve zero is stored in the lower two bits of a 256 The status for the next reserve is in the next upper two bits. So bits 2 and three and so on. In theory all the way up to bit 255 if you want to store 128 reserves. Currently a tracks somewhere around 30 different reserves. So in practice it's not actually going to fill up the entire bit vector mass. Now I want to say that I've been talking about reserves and assets. I will not go into further detail about what exactly that means because for the low-level section of this talk it's not quite so important but uh if you have some familiarity with

a that'll help ground this discussion but it is not going to mean you're going to be totally lost. This is going to be really focusing on the technical details of what happens. So as Ernesto mentioned the detected anomaly was when certain operations were changing different parts of the state in the someone raised their hand it's my CEO uh okay anyway hi Moly so the uh code that was mentioned Here uh we first hypothesis we had was that the code that was managing these maps was

somehow affected and affected by some anomalous compiler behavior. As Ernesto mentioned, we once sera really started to do this deep dive, we had ruled out most other possible hypotheses. And at this point, it was trying to understand what the compiler was actually doing and what might explain this possible behavior. And so before we describe the actual bug itself, I think it is useful to go over what the Solidity code was actually doing. This is a simplified version of the code that manages the user configuration map.

And now the user configuration map is just a strct that contains this bit vector. For those of you who know Solidity, you should know that you can't pass 256s by reference. So this is just a way to accomplish that. And we see that this function can either clear or set the borrowing bit for a specific reserve whose index is reserve index. And that decision about whether or not to set it as borrowing or not is determined by this boolean borrowing flag. So I think it is helpful for us to quickly walk through how this code executes and what it's actually doing at the very low level so that we can better understand what actually happened and where the buggy compiler behavior comes

into play. So let's assume that we are calling this function with reserve index 3 and we're setting we have borrowing set to false. So that means that we are clearing the borrowing bit of some reserve in this case reserve three. So here we have this configuration map for the user and we start out here on this line and we have one. So one is just a bit. It's the bit at zero at index zero and then a bunch of um zeros following that. We then will shift it up by this amount which is reserve index.

shift it up by one which for those of you who bits on a regular basis will know this is actually just six. So if we shift up this one by six places we have that uh we have one followed by a bunch of zeros um six zeros to be exact. And if we look we can see that this indeed is setting uh this one is now at the uh bit location for the borrowing bit for reserve index 3. And again, we're starting from zero. In case you're thinking, hey, that's reserve four. It it's reserve index three, zero based indexing.

So, next we pop down here and we do a bitwise knot. Now, this will just flip all of the bits. So, all of the other bits that were previously zero now become uh one and all of the the bit at the index for the borrowing flag for reserve 3 is now flipped to be zero. Then we end this operation or we end the result of this rather with the original uh user configuration map. And what we end up with is a configuration map that is completely the same as the previous map that was passed into this function except now the borrowing bit for reserve index 3 has now been set to zero.

And this is exactly what we expected. And I should mention that this code has been deployed and I've removed some require statements but it is I'm not there are no real other simplifications here. It is almost as straightforward as what I'm presenting here on the slide. So this all makes sense and it works it seems to work very well. Now what happened in this case was actually we would set the borrowing flag for reserve index 3 to zero and then all the other bits below would also be cleared. So both the collateral bit and the borrowing bit. Now perhaps Ernesto you could very quickly jump in and describe what exactly this would let the user do if this would actually happen and this had been uh allowed to persist on the zkync uh ecosystem.

Yeah. basically like that is something I didn't mention before like but the the the behavior that we observed was like so when when from a user perspective you were providing two collaterals like and and borrowing to different assets like then what it was possible was just to repay like some of the one of the assets like and then it will allow you to withdraw all the collateral like while you still kept borrowings open and and this like on on how we actually notice that the pointing to this like clear clearing of of the of the bit map is that yeah it was very clear that that kind of

manifestation on on the bit map like because a way that the protocol will allow you to withdraw your collateral while keeping borrowers will be that if you skip basically the system checks for this this this flags like of is borrow borrowing or collap collateral in order to not do what we call health factor validations of over collateralization. So to simplify if if we see on the B map that the user for example is not borrowing anything we just allow like that protocol just allow to withdraw all the collateral like so all zeros on on like all the is borrowing flags on all these bits will mean that the user factory is not borrowing anything no matter like

then the balance of tokens that it has like so if the protocol sees those zero say okay fine you can just withdraw the collateral because your over collateralization should be healthy. However, like this is this was not the case. Yeah. Right. So, effectively to quickly condense it for those of you who are not familiar with a a bunch of your loans suddenly magically get forgi for forgiven and you no longer have to post collateral. This is [clears throat] very bad for the health of the protocol for I think obvious reasons. So, this is pretty strange. Um, and it was it led to a lot of head scratching and we first ruled out a lot of different possible scenarios. I think Ernesto mentioned the sort of well maybe the UEI was just wrong. Maybe some of

these helper contracts are wrong. But again, it became very clear that low level this is actually was happening. So the actual state and data that was being manipulated on the zkync uh execution environment was just wrong. So here are some confounding factors that made this all the more puzzling. Um this does not happen on the EVM. Ernesto mentioned that A is very careful to deploy exactly the same code on new blockchains and new ecosystems. And this very same code was working perfectly fine on a for years now.

Now again I mentioned the EDM because ZK sync runs its own VM called the ZK era VM. And an more confusing factor was that this logic, the logic in the set borrowing function was actually formally verified uh by Storra. Um, now this was targeting the EVM code. And you might guess that all of my references to the EVM is maybe foreshadowing a little bit. And but just to be sure, we reread, double checked, triple checked the logic of set borrowing, and it looked correct.

There was at this point pretty clearly not a logical error, but a compiler error. And so at this point because there is some disagreement between what the source code says we should be doing and what is actually happening when we run that code we need to ask a question. So what does the assembly say? At this point we started diving into the actual low-level assembly that came out of the zkync compiler to try to understand this difference. Now one very crucial part of the process that I think is made all of this possible was to start small.

The affected contract was in a file called pool instance which pulls in several different libraries and it's very big and for those of you who've looked at any low-level assembly code there are sometimes descriptive labels but very often not there's nothing that says here is the set borrowing function look at this source code here you can see in fact the closest we get is BB0 one two three and so on which is just basic block this is not helpful and trying to scan through this huge swath of assembly code trying to hopefully just notice the code that corresponds to this set borrowing function would be like finding a needle on a h stack. It would just be deeply unrealistic. So

instead we just wrote a meaningless test contract here. This is the actual test contract we use uh called test appropriately enough and the logic here is not important but what's important to see is that we are using this set borrowing function. And the hope was that we would have we would run this through the compiler, get a much much much smaller piece of assembly code, and if we're very lucky, we'll maybe find the bug in that assembly code, which would then explain the anomalous behavior on the code that was uh deployed and found to be buggy uh on the actual ZK sync EVM.

So, at this point, we should be close to done. Well, uh we we were So because the assembly code was so small, it was fairly easy to trace the execution and find the snippet of assembly code that corresponds to set borrowing. That's great. Um this is the code on the slide here. The actual details of this are not terribly important. Um we see some shift lefts which is what we'd expect to see because the original code remember has two shift lefts. We shift the reserve index left by one and then we shift one left by that amount. We load from storage. We do some bit twiddling to get the bit masks.

We and it back together and then we store it back. And those are the commands you see highlighted. Now again, I'm not going to go into depth about [clears throat] what exactly is happening on each of these instructions or even how to interpret these instructions, but hopefully you get a from reading it, you can get some intuitive idea about what's going on. Now I want to stress that this is also ZKVM by code not EVM by code here. So like I said good news we found it but the bad news is that this looks fine. Uh we read this we double checked it. I went over this again and again and this is this is correct. This actually fits what this is the faithful encoding of the operations that originally appear in the solidity code.

So maybe we've hit a dead uh a dead end here. But we've actually got something incredibly we got two things that were incredibly valuable out of this small experiment we've done. The first thing is that we do actually have a a fingerprint of sorts to look for the code of set borrowing in the full pool instance assembly. Now, that's very useful because we aren't just left scanning through thousands of lines of assembly code hoping something jumps out of us. But I think at this point, the even more exciting finding was that we have a plausible culprit for this behavior, which is namely the optimizer.

And this is where we're going to actually return to the same diagram that Ernesto shared in his slides, but uh with slightly different formatting. Uh and at this point we're going to discuss the LVMIR. Now as Ernesto mentioned the ZK uh compilation pipeline is actually several pipelines strung together. The original solidity source code is uh compiled with solidity which produces ule which is an intermediate representation. That intermediate representation is translated to LVMIR.

At that point, the LVM, which is this open source compiler tool chain, a lot of compilers out there actually use LVM. The Rust compiler uses the LVM. Uh the Rust compiler actually just generates LVMIR and then leaves the actual optimization and assembly, the generation of the code that actually gets executed to the to LLVM. So it's a compiler library, if you will. And this is what ZK souls does. It will take you will translate to LDMIR and then leave to LLVM the details of allocating registers, stack allocations and so on.

And that's the part of the pipeline here that I've circled in green. At the end of this process, ZK the ZK sync team has written something that takes the LVMR and spits out the actual uh bite code that I was combing through. Now there are a lot of benefits of using LVM. It is as I said open source. It is also battle tested. It is used to compile Rust. So this is not some obscure project. It is very well tested, very well respected. But another nice benefit is that when you use LVM, you get optimizations for free because LVM operates on this independent intermediate representation. It has this huge host uh library of optimizations

that make your code faster and smaller. And for those of you who are familiar with smart contract deployment, you know that smaller code means much cheaper deployment costs. And so it is standard practice to ask these compilers to optimize for code size, which is indeed what was done in this case here. So we had a working theory that there was something going wrong with optimizations and all that was left was to find the affected assembly code in the output on the full pool instance contract.

And when we look for this pattern in particular, we just literally use GP to search for uh shift left. S1 and looking for the rest of the patterns, we found exactly one place in the source code which matched this pattern and it's this one. Now you can see that is this matches fairly closely what we saw in the test contract code. We are doing some shift lefts to get uh a bit. We are doing an S load. We're computing some bit mask. We're anding it with a value read out of storage and then finally writing that value back into storage. But you'll notice that we're not doing exors or bitwise knots.

We're using roll which you know what is that and what is CPIO 60? So roll stands for rotating left shift. It is a left shift where if you're familiar with bit vector semantics, usually when you shift left, any bits that are in the upper part that would be shifted off the end, they just go away. And all of the bits uh that are were occupied by the lower bits that are now shifted upwards are usually filled with zero. Rotating left shift instead takes those bits that are shifted off the left end and append it back onto the other end instead of just filling it with zeros.

So that's what rotate left shift is. But that doesn't really yet explain what this is really doing because what is CPIO 60? So here we have R1 which is the index of the bit which holds the borrowing flag to clear and we're using that as the amount to rotate left shift CPIO 60 by. So what is CPIO 60? Well, it is a seemingly random looking magic constant. This is just this there's nothing that jumps out to me at least when reading this number until we turn it into hex. And then we see it's a bunch of fs followed by one e. And if you know your hexodimal, you'll know

that in binary this is a bunch of ones followed by one single zero. And so we can see that this is actually a very clever optimization. the uh original solidity code would left shift this single one into place and then bitwise not it and then apply the bitwise and and here LVM has saved a small number of instructions but every instruction counts when you're optimizing for code size to basically pre-apply the bitwise knot and then that gives a hole which is the zero at the very end of this bit vector and then you rotate that hole into the place that you want to clear. So this is an example again of this strategy applied to uh bit index 6 [clears throat] which remember

was the reserve or excuse me the borrowing flag for reserve index 3. So we first rotate off these upper six one bits. We've now then rotated this zero into place and then we appended those ones that we shifted off the top onto the bottom. And then if we added this we would have exactly the intended behavior that we wanted. So this is a great very fun optimization. Great job LBM. Uh you saved a couple of instructions but works as intended. There's just one problem and maybe some of you have seen where this is coming but this magic constant was actually chosen for a 64-bit architecture.

So two the this value is actually 2 64 minus 2 which has this decimal representation. This is only 63 ones because ZKevm uses 256 bit words. This was implicitly left padded with 192 zeros. So that makes the behavior of rotate left shift very different. Instead of shifting off these ones and then putting them back into place, we have a bunch of zeros which get shifted off of the top of this bit vector and then placed on the bottom. And now we can see exactly how this happened. This explains almost perfectly the behavior we were

seeing setting the borrowing flag. And I should also mention at this point a very similar uh problem existed I believe collateral as well. Uh although we're just for the purposes of discussion I've been focusing on the borrowing bit. The uh the collateral has the same anomaly as well. And so in this case um we can exceed exactly what was described. All of the borrowing and collateral flags for every reserve with an index less than the one that we were trying to affect get zeroed out. Now I don't mention it here on the slide but we weren't satisfied with just this.

I then further found the set borrowing code and tried to write some very complicated version that was doing basically the same thing. it was just doing it in a very roundabout way that made it very hard for the optimizer to apply the same optimization. And indeed when I recompiled the set borrowing function to use this uh more complicated version to defeat the optimizer, this pattern with rotate left shift disappeared. So this was very helpful because it confirmed that this was in fact optimization bug because if we made it impossible for the optimizer to do its job, the bug disappeared. And it also further confirmed that the assembly

code that we were looking at actually corresponded to set borrowing. there was a small chance that we just happened to find some completely unrelated code that happened to somehow show the exact characteristic of this bug, but we actually were looking somewhere else. At this point, I shared the findings with uh Ernesto and the rest of the uh ZKYNC team and the rest of a excuse me, A and BT Labs and all the stakeholders. At this point, we started a search and the uh it was eventually found that just uh relatively recently LVM had independently found this bug and this is the pull request that ended up fixing it. You can see from the screenshot,

this was changed last month. Um, in case you're curious, you can see that they are using git constant, which is bitwise not, but they are now getting doing get sign constant again, which produces the correctly padded uh constant for the architecture. Um, I think this is let's see we have um about 10 minutes left, which I think is perfect for Q&A, but I think before we get to that, I want to share some of the sort of the takeaways from this entire experience. So, I think Ernesto has a slide here that we can share as well.

This is a screenshot. I'm not trying to dunk on anyone here or call this person out specifically, but this is a Twitter response to a a thread that was posted about this bug. And someone said, "At this point, I don't trust anything." And, you know, that's a reasonable sort of impulse to have here. And so, we could say, okay, well, let's only use verified software. That's a great way to get around this. If everything is verified to be bug-free, then great, you're you're never going to have a bug. Unfortunately, this is actually mathematically impossible due to something called Gal's incompleteness theorem.

Even if you verify something, you then have to verify the verifier. But what verifies the verifier? It's a very much a who watches the watching problem. Now, I'll sort of by the same token, maybe you say, what can you actually trust? absolutely nothing like this uh Twitter commenter was saying. And this is also impossible because at some point even if you aren't trusting tools, you having to trust people. If you're not trusting people, you have to trust the code that those people write and so on and so forth. So I think the actual takeaway is to not just throw it all away and burn it all down. But I think instead we want to the takeaway is to not assume the correctness of any of your tools. So don't assume that your compiler is

correct. You should test test fuzz verify the output of your compiler. Don't write you know sourcebased tests. Write code like invest in spinning up instances and uh actually running all of this complicated work on the actual target VM um to test this behavior. But I think it's also just as important to test fuzz and verify your tools. This is something that we find very often in the formal verification side of things at Sertora. It is very easy to write a specification, a grammatical description of your intended behavior of your system that is actually vacuous. It's just paologically true all the time. So make

sure that you are not proving nothing. Similarly, inject bugs into your source code and then check to make sure that your fuzzing tools actually find those bugs. And if they're not, then the no bugs found result is not terribly. And so um also I'm gonna give a I think Ernesto, like I said, had some gives his own takeaways, but I really really quickly shout out a BGD labs, Matalab, all of them for their incredible collaboration. It was a it was a very exciting moment where all hands on deck in the war room. Um and it was a it was super great collaboration uh all around.

So with that, I'll throw it back to Ernesto. Yeah, cool. Yeah, as John say, I will just share some some extra thoughts like on the takeaways. So, yeah, let me share. Yeah. So more or less to reiterate like on on what Jo mentioned like is for all those that you want full full certainty like on on blockchain code like and it behavior like and basically on all type of software in general like this yeah maybe there are some bad news there because you cannot get it 100%.

But what you can get like is yeah a lot of tooling and apply a lot of tool like to reduce like the the the appearance of these kind of issues to basically the minimum like so 100% maybe is not achievable but 99 with quite some lines maybe is something that that you can you can reach at the same time like something that is very very important and that we are trying to always tell to to the partners that work with with AB like blockchains is that it's very very important like to have up to standards tooling like sometimes yeah it's it's actually not the case of CK sync like

because as I said at the very beginning like they put tremendous effort like on on on the tooling side but it's a good representation because like even on whenever you put like a lot of effort like tooling for application developers like us is maybe not completely enough like so is yeah extremely important like for those that contribute to the touring ecosystem of Ethereum and blockchain in general like to put focus on that. Then some other something that is quite interesting is that well the LLBM as explained is far from being like some niche project like or or dark

project with one or two maintainers like is a production grade like software like used by basically a good percentage of of the infrastructure out there like and definitely not only on blockchain. So but the Ethereum architecture like and and by inheritance like all other architectures that are trying to be compatible with Ethereum they are a bit specific like in this case with 256 bits. So that creates that even the coverage of these dependencies like the LLVM sometimes is not as good as you could have expected. Like in this case for example like yeah they it was a a

bug that was fixed like but for what it seems is just that the 256 bits target architectctors are simply not as cover as it can be like 64 bits which are like way more standard like in commercially out there then yeah not everything is is is bad news like far from that like on this webinar like because yeah Maybe you can you cannot have full certainty that your protocol be will be fully protected. But the reality is that we are talking about double protocol which is quite big like and and there is always the target for exploits and yeah it was a critical bug that appeared like

on on its activation and in practice there was se impact on a bug that was very very deep like so this doesn't come by by by chance like this this comes because like the yeah on the ecosystem the aid has put like a lot of resources and effort to improve this these quality levels like and and yeah like if you focus on on that quality on the prevention side like yeah you reach this kind of situation some where the outcome is uh kind of happy happy story even more like today like CK sync happy with CK sync has been activated finally after some delay like so yeah that was a good

end result then there are like some stuff like for example the endless debate like of immut immutability on blockchain versus nonimmutability which this is a good example how sometimes you need to be pretty careful when when expanding like with immutable code to especially to new environments because yeah I mean in this case you think that your code is exactly the same as in other place but it's it happens that under the hood is not really the same what gets executed like so you just I mean immutability is perfectly fine obviously and probably what Ethereum like all applications should target in the long term but at the same time we

application developers we should be very careful. Uh yeah another another point is that yeah it is this was quite quite tremendous job in my opinion and from different entities collaborating together which yeah is quite positive aspect like of Dows like because yeah there is a lot of criticism sometimes on why Dows are so anoptimal that they don't work like well in this case it worked quite well and quite deep uh And yeah like in in general like that security is very important like it looks quite repetitive like sentence but yeah it's quite important and usually when

you spend into the quality of it you get good results like like this this detection and prevention and yeah kind of that's it if we have like maybe some questions. Yeah, we have a few questions that came in through uh YouTube or the chat. So, I'll just go through some of them. Um the first question is, is the ASM that's shown in the slides X64 or ZKVM assembly?

Uh that was ZKVM assembly. Perfect. It [clears throat] looks uh the confusion sample looks very much like uh x86 uh assembly. Our second question is, is there a way in the LLVM backend to select which optimizers you want to go through in your code when you're running them? So, it depends on who you is in this scenario. You as the person who is writing a compiler that uses LVM has, as far as I understand it, very fine grain control about what LVM actually does. uh LVM itself also will

check whether or not an architecture basically supports a certain optimization. In the screenshot that I shared in my slides, there was actually you could see a little query that says does the architecture I'm compiling for support rotate left shifts. But you as the if you're the person who's using a compiler, I don't believe so. I think there are a couple of flags that you can say turn off this specific optimization, turn off that specific specific optimization. Uh but you have to rely on those optimizations being exposed as specific flags. This particular optimization was what's called a peeppole optimization and I'm not aware you could turn off that very specific optimization. You can also just turn off optimizations in general. You can turn on optimization

level zero for example and that will not apply any optimizations. I think like if I would like to add here a bit like because something very very important and we didn't really touch because it's not so much the topic is that obviously after detecting all this like this issue and protecting the system like our objective at the end of the day was okay how do we do or can we like keep like with the deployment of fab3 into into CK sync like and yeah that was a lengthy discussion by itself like but one of the points was that like we consider okay what what what happens if we disable optimizations because yeah it's quite natural to think that yeah the optimizer

had the issue like the LBM optimizer so yeah maybe if we disable the optimizer this will be there would be less surface for bucks right but at the same time when you when you start thinking about that you you also notice that if all the smart contracts that are actually running in production like are using the optimizers the optimizer like and and still this is like a let's say a bit tricky target like machine you you have like this battle testing like of of systems that use this optimizer. So yeah maybe like it will reduce like certain surface but it could be also that you are creating a completely new surface that was not better tested at all at all

because the majority of users use the optimizer. So um at the end like the solution like well by the way like maybe we can quickly brief the solution because the solution was just to update the compiler where like this fix was was done and then of course like improve all the testing like and and give some yeah some extra assurances like to run faster the tooling and so on. But that like the simplest solution was just to update the compiler look like actually the most robust like in in in terms of in practical terms. Uh yeah.

Uh, one question that just came in is, is there a way with direct differential fuzzing to highlight this bug with optimization and not optimized? Uh, I assume by differential fuzzing this means running the same inputs but with just different versions of the source code. In uh principle, yes. My understanding is that this would rely on a fuzzing tool existing for ZK uh EVM uh which I do not believe is the case. But in principle, yeah, and I I mentioned previously that we actually verified this rule as well,

which I think also is something that was just asked in chat, which is was this tested for? Did we have a test? And I know very simply we have a we formally verified the implementation of this function for the EVM. The sora verifier does not currently support the zkync VM. So that is sort of where the the gap occurs here. So it's not like this was just untested code. I want to give a lot of credit to the folks at a and btd labs and all that. This was not just some code that has been no one really looked at or thought about because it was just so simple. No, we were we were there were there were there was all the verification rules for this exact piece of code. It just because of limitations

in tooling it didn't uh we weren't able to to reverify it on the ZK EVM by code. Yeah. And also like to answer like I'm just like the next question which is completely related like so one of the core issues where like the the test suite of a is quite big like on a foundry environment and we could say that there is like kind of two parts one is like the most base test suit which tests like units and relatively simple scenarios while there is like some other parton where like you do a bit more let's say combinatorial scenarios like and precisely this bag was manifesting like what I explained before of you need

two assets of collateral, two assets of borrowing and you need to do specific amounts like of repayment basically the whole repayment in certain assets for the back to manifest like of course like and there is like infinite scenarios that will like manifest the bug but the the main point is that you need to go a bit deep already in in these combinations like of test like so precise of those tests like it was basically impossible in practice like to run them like because the tool the timing with the tool was just too much.

So obviously like we trusted on all the other assumptions of like okay if the basic test work if the code is the same like if yeah all all these kind of things like the possibilities to have like compiler bug or something like that are extremely low like also because of the other thing that there was an instance of of the code base of a running in production even if it was not a itself like for quite a while like so uh yeah like right now the advance answer that that question like of course like to before activating the the pool again we tested exactly the same scenario and a bunch of others more and yeah that will give us extra assurances apart from

other stuff that we are doing in general for a not only for CKC to improve fasting and and some other security sections Maybe one last question to tie everything up. Um, you mentioned tooling and and kind of using a lot of tooling throughout your process. What kind of tools did you use to find like root cause? And other than like unit testing, what tools are you using to continue to test?

Oh quite a lot like I mean within within the limits like of of Ethereum development like and blockchain development but yeah so basically the most basic is that we have a like a foundry suite like for the development and the basic testing then of course we have for like for quite a while for years like the the certa properties suite which I mean sadly we can only apply it like whenever like is the dbamage yourself and until now we had big assurance that that was enough.

Yeah. What else like we we do we have a lot of custom tooling that most probably people is not so aware on a on our own repositors especially for diffs of code like visibility of difference between of configurations of assets whenever something happens in production. We have like certain monitor internal monitoring like uh yeah we have probably almost everything that is available out there like to to to improve asurances like but but yeah like it's very important to have like for other teams like to have the mentality of trying new stuff like because this is I mean it's very early times like so um still like new new tools appear all the

time that are actually game changing like in terms of development experience. Yeah, I just in case there was a question about like what tools did we use to find this exact bug itself. Um, Emacs uh on my side. So, I I wouldn't recommend in general opening up the assembly of your smart contracts and just scrolling through it with Emacs. This was just a this was what was expedient. I'm afraid there's no terribly exciting answer about the exact tooling or magic wands that were used here to to find this very specific example.

All right, awesome. Um, I think that's all the questions that came in through Zoom and through the YouTube stream. So yeah, thank you for highlighting this bug and highlighting like the root cause investigation. I think that was super interesting and super eye opening. And thank you everyone else for tuning in. Yeah, thank you all. Thanks everybody. Bye.