# Raoul Schaffranek - Security tooling: Debugging Solidity - Speakers: Raoul Schaffranek - Channel: [ETHCluj Meetup](https://streameth.org/ethcluj-meetup) - Date: 2025-10-07 - Duration: 26:41 - Watch: https://streameth.org/watch/yt-IHUDUZosHUM - YouTube: https://www.youtube.com/watch?v=IHUDUZosHUM ## Description During the session, we will introduce Simbolik: a Solidity Debugger. It's a pioneering tool that brings interactive breakpoint-style debugging to Solidity. During the talk, we will exemplify the debugger's core functionalities and uncover how it excels in detecting nuanced bugs, which often elude more traditional methodologies like testing, fuzzing, concrete debugging, and static analysis. ## Transcript My name is R. Shafanek. I'm head of developer tooling at runtime verification. Uh it's a company that focuses on security and a special kind of security. We do formal verification and developer tooling. So and this talk is specifically about the last bit like the developer tooling and one specific tool that we are building. It's free. There's some other tools that we have that you may know us from or not. So we have KVM which is the uh longest standing and still maintained formal specification of the EVM. Um we have control which is our formal verification tool that runs on top of foundry. And then we have symbolic which is the topic of today. Um so this is what I want to do in this talk. Um so first of all I will give you a little bit motivation why we need debuggers or who wants debuggers actually and then what is the problem with the current generation of debuggers and then um one thing that I noticed is people are using they they are often using debuggers only for a specific task but there's like I think many applications where you can use a debugger so I want to talk a little bit about some applications for debugging that um might be not known to you. So, but let's start with the motivation. So, we are doing this solidity developer survey every year where we the Ethereum Foundation or now the Argot collective uh they are asking solidity developers, hey, how do you like solidity? What is your pain points? What do you like about the language? H in which direction should we move on? And since 2020, like since the first year we do this survey, um we always got response that said debugging is one of the most dreadest aspects of the language so far. And this repeats every year and 2024 is not on this slide, but let me spoil you, it's the same story. So also 2024 people complain about bad debugging tools. Um, so are we just too dump to build them or why why didn't we solve this problem? It's like I think it's the um most important developer experience problem that we have to solve. But are we just too dump as an ecosystem to solve it? And let me show you like what the current debugger generation looks like and then you may understand why solidity developers or auditors don't like them. So this is one of them and you see there's a lot of low-level details like you get some bite codes that you can see uh there's some I don't know some memory some low-level memory a stack uh and what's very nice about this one is you get actually to highlight the source line where you are stopped um but it's a very low-level tool you have to be comfortable reading EVM bite code which most people are not Most solidity developers, they know very well solidity, but they don't know how to read the bite code. And that's fair because bite code is not meant to be human readable. Byte code is meant to be machine executable. So there's a gap here. This is another tool. This is from Tenderly. Um and also you see like lots of low-level information uh spitted out in this output. Now these tools um I don't want to call them out here. They they are doing basically uh it's not their fault that they need to show us these low-level details. It's just the solidity compiler is an optimizing compiler and optimizations are making debugging very very difficult. Um and the solidity compiler is not giving us debugger developers sufficient information to reconstruct the highle data structures like the solidity variables, data structures, data types. So they can only show us this low-level details. But now the um there is an attempt to fix that and there's a working group in the Arg collective that is developing a new format that is called ETH debug and the goal of this format is really accelerate the adoption of debugging make debuggers better and we recently um open sourced a big component of our debugger that is called the east debug pi library um that is a clientside implementation of the east debug format and we will see in action how it improves debugging. So but because this was funded also by the ethereum foundation we made it all open source so that other debuggers can also use it and I hope we we will see some adoption over the next month or years. Um so it's already implemented in symbolic but the solidity compiler still needs to catch up. So both sides of the tool, like the debugger and the compiler, they need to work together. We now have it in the debugger, but the compiler still needs to catch up. Um, all right. So this is what symbolic looks like. Uh, this QR code brings you to this website where you can try it out in a browser. Um, so you see it's uh I have a laser pointer. It's a uh it's embedded into Visual Studio Code. that all I wanted to say you we're going to see some more examples. So, but let's do it per application. So, the original use case for us as a security company was we wanted we needed a debugger for our own audits. Um because like well you can try to stare down a bug by just looking at the code but that's a very like inefficient way to do it. Um I I think you need to experiment with the code. You need to run the code to see it. You need to be able to pause it to see like to to see the contents of the variable at any point in time to follow the control flow. And the problem really is well smart contracts get written once by a developer team and they are super familiar with the codebase. They know they understand what they doing. But then if you're doing an audit then you're new to this codebase when you're an external auditor and you have very limited amount of time to assess the quality find bugs of the codebase and you don't know where to start like there's maybe like the protocols we see today they are super big they are super complex so where do you start what is the main entry points how does control flow through your protocol and the debugger makes this very very visual and we will see an example on the next slide It makes it very easy for you actually to just start at any external function and then you step through the code and see where the control flows. You can see the contents of the variables. Um you can even go backwards. So but here's a very concrete example. So um in this example we were auditing a dex and a constant product market maker and we wanted to see how does the swap operation change the balances like that's the most critical part of a dex is does the is the pricing formula implemented correctly. So the debugger now stopped at this line where Bob is about to perform a swap. We are now before Bob performs the swap and we can already see what is the balances before two uses um before the swap. So we see okay Alice and Bob they each have um 100 token of 100 tokens of each token in the pair and then Alice in this case is the only liquidity provider. So she owns 100 shares of that pool. Now Bob is about to swap 50 tokens A for whatever amount of tokens B. We want to know. Um and even if you know the pricing formula like doing this calculation, okay, how many tokens will Bob get out there? Um we sure know it will not be 50 because uh the constant product market the the formula tells us no he will get less because well Alice should get a fee for or she get an interest rate for supplying the liquidity but what is the actual number you can do that calculation on pen and paper and actually that's what I did like uh many many times and that's super timeconuming process so but now I can set a break point like why did the return statement here in the last line and I can go there. Now the debugger stopped and now I can see the new updated balances of each user. So I now see okay Ellis now has 150 tokens of the first token in the pair. Fair enough. That's the tokens that come from Bob. Um and Bob uh and Bob's balance has decreased by 50. Okay, fair enough. But how did the the other token in the pair change? And now we see okay uh Ellis um lost 32 tokens and Bob gained 32 tokens of the second pair. So if you do this on pen and paper it's really timeconuming process with a debugger. You just write your test case like this and then you can immediately see it. Of course you still have to do some manual math in the background to see that these numbers are actually what you wanted to get out. Um but at least that you can see it and follow the control flow. So that is um I think that's a big win. So another application for debugger is testing of course. Uh and well testing is like an automated technique. We write our tests and then we can run them on every pull request. Uh the problem is okay what happens if a test fails like how why does it fail? Is it a problem with the test setup? Is it a problem um in the in the in the logic of the implementation? So if there's a mismatch, it could be both. And tracing down the the source for the failed test, that's something that's very difficult to do. Um especially like the more complex the protocol, the more difficult this task gets. But there's an even there's an even worse problem and that is sometimes you can have a test and it passes um and it looks all great but actually it's passing for um uh a suspicious reason. It's not doing what you wanted to test. So I think a debug is a great way to uh run this test interactively step by step and see that the assertions that you want to hit are actually reached because if it's returning early or this says there's a try catch that catches your bug early it's not doing what you want. So test case debugging is another application. Um, and then forensics. I think that is one thing that the tenderly debug is really great at and we always see it everybody like after a hack happened on chain everybody's using the tenderly debugger to follow the transaction see what led to the exploit. Um, you can also use symbolic narrow for the same purpose. You can trace transactions after a hack to do to do a postmortem. Um that's usually very very difficult to do because the hacks we see today they are not just calling a transaction but there's some smart contracts that are deployed by the attackers themselves and they usually don't upload the source code. Um so it's it's very hard to see what the attacker was actually doing. Um and both symbolic and um and tenderly I think are great tools to do that. Um, and yeah, I think the story is even a bit bigger because well, one of the original promises of blockchain was make onchain activity transparent. But I I think this has only partially been achieved. Of course, all the data is on chain. We can follow it. But then we are looking at bite codes and we are looking at big hexadimal numbers and human like output that is not human readable and with a debugger we can make this output human readable. So I think like if you like if you are on the original vision of Ethereum like bringing transparency onchain then debug is also a great way to achieve that. Um, let me show you how this looks like. And I think there's a video that auto plays starts autoplaying on the next slide. I'm not sure. Um, so this is a block explorer. I just open a transaction and I open it in symbolic now. And what I can see now, it brings me automatically inside the code. And now I can like step by step follow what the transaction actually did. So, and I think this is the the benefit that symbolic uh has that it's it's actually step through debugging um and you can actually see the contents of all the local variables. So, that is something new that no other debugger I think can do today. And then this is a very unexpected use case and I we didn't have it on our minds. Um but then when the buy bit exploit happens happened um everybody was chatting about blind signing suddenly uh and yeah and then we realized well it's true like whenever we sign a transaction today we are not really like we are not really making sure that the transaction is doing what we want in the best case uh our wallet or our ledger will decode the AI uh for us so we can the the name of the function that's that gets called. But well, you know, any attacker can deploy any smart contract, call his functions whatever he wants. Uh he won't call his function um uh attack or exploit or steal money, but the attacker will choose a name uh that makes you believe that the function that you're calling is trustable. So if we only look at the AI, we are not safe. Not at all. So what we really need to do is before we sign a transaction, we can simulate it in a debugger and see the actual code execute. And if it's a different contract that executes or the logic is not what you expected, you don't sign the transaction. And this sounds like a really big overhead for signing transactions because you have to be a very technical person even to follow like what a debugger is doing. Um, but with MultisX and the teams that control wallets that are worth millions or tens of millions of dollars, I think it would be great if you had just one technical person on the multisc that runs it through the um runs it through a debugger and actually makes sure it's doing what they want. I think the by bit had could have the by bit hack could have been prevented. Um, but to be fair, this idea we had only after the by bit hack. So the tool just didn't exist. Yes, please. >> Methods do simulation so that they could get around like offcated transactions. So they're doing that in real time and simulating what will occur and figuring out how to maximize the profit off of the transaction that hasn't been scheduled yet and jumping in front of bringing it right up the line and the transaction. So they have this basically real time for me bots. So this is only available for us to follow. >> Yeah, I think but I think the uh well meth bots are um they're sometimes hidden or uh working on like hidden um transaction pools uh that or hidden mess that you don't see. And I think this is complimentary. So you need these automatic checks but I think you also need to have a person looking at the transaction that gets executed. Um yeah it's complimentary I would say. Um so well let me go back before this video starts. Oh no. So this is a dep um and now I'm signing a transaction and again before I sign it it actually brings me uh like I'm calling the remove liquidity function and now I can step through the code actually see okay this is the function that I wanted to call and this is the logic that I wanted to execute not just by looking at the name again I could call any function remove liquidity but it's is it actually removing my liquidity is it transferring it to the addresses I want it to transfer so that's the assurance that you only at when you really look inside the transaction, not just at the API. Um, what does the time say? Okay, I'm going to skip over this DA proposal thing um and this formal verification thing. What I want to show you is what how deep you can actually go with a debugger. So, this is now for the experts. Um I don't know how many of you know how the solidity compiler um allocates a dynamic memory in a dynamic array in memory. You know it great but most people don't and learning this by reverse engineering the compiler is a very difficult task. So with a debugger we can do that fairly easily. So you see on uh on the code here we have a dynamic airway with a with three items. We can see it stores like three strings, hello world and exclamation mark and then it's just concatenating them and emitting an event. Um, so very simple setup. Uh, the purpose is not the contract. It's very it's superficial. It's uninteresting. But we want to now understand how the solidity compiler allocates dynamic memories and aries. Um, and we can see well we can see first of all what is in the in in the array uh just by looking at the variables. So we can see it here. Um but if you don't trust the compiler and there's compiler bugs I can we found several um then you want to understand what the compiler is actually doing. So you want to see what is the how does the memory look how does the array look in the memory. So we can see here now that on offset 60 something there's stored the array length you can see it's three. The next three items are pointers to the elements of the array. So these strings are not stored like uh as a value but stored as a pointer and then you can follow the pointer and you arrive at this offset and in this offset you can see there it stores the length of the string of the first string. So the string hello is five characters or five bytes long. It's bytes not characters. And then on the next slot we can see uh the ASI encoding of the string hello. So this like this blue box here that's the ASKI encoding of hello and then we see the ASI encoding of the of the string world. And then we see the ASKI encoding of the exclamation mark. Um and then down here we see that string that is just the concatenated uh the concatenated message I think with some yeah with some space in between. So the length here is actually one character longer. Um so this is information that used to be really hard to get out of the solidity compiler. You would run basically you would write small examples and you would um compile small contracts and then you would execute a transaction somewhere on your local test net and you would open a block explorer to see what happened um or the the foundry debugger which is really low level but it does not give you the solidity variables. So this is something that is uh has really improved now if you really want to look at the at the bite code again you don't have to do that. So you can just look at the solidity variables, but then if you want to get down that extra level, if you have a suspicion that something on the bite code level is not matching up, and again compiler bucks, they are rare, but they happen and they can be critical. Um, okay, I'm going this would be another example. Um, but I I think I save some time for questions instead. >> Amazing, Ro. And I know we're going to have a lot of questions right here and they're starting already from the front row. >> Uh so does the debugger follow execution through contracts? >> Follow execution >> through contracts. Yeah. So if a contract calls another contract >> Yeah. Yeah. >> Amazing. >> It does that. Yeah. So if you have uh Yeah. I think that is pretty standard. Um if because well all the contracts we have today the the protocols that are uh that we're seeing today they are not just a single contract like back in the days when we had web ETH it was just a single ESC20 contract but all the protocols we see today they are like complex head apps composed of hundreds sometimes or dozens of uh smart contracts and yeah it follows the flow of the of external calls also and even if there's some um external call that um is not source code verified, it would let you at least allow it to debug it on the bite code level. >> Okay. And how does it handle storage like do you take a snapshot of the current block latest? >> Um we are getting yeah we are getting basically what we are doing is basically lazy forking. Yeah. >> So when the debugger sees uh a storage operation as load or as store it will go to the uh JSON RPC node and request that latest storage slot and then it will do it own internal tracing because it needs its own in well the story at the um at the block level the storage you don't get you want we want to have a finer grain model of the storage. We don't just want to have the storage of the beginning of the block, but also we want to trace it as the transaction keeps updating it. Thank you so much. That was actually very hard to implement because uh even like it's not sufficient to get the storage of the beginning of the block but there might be a transaction uh before the transaction that you want to debug that accesses and modifies the same storage slots. So we also need to trace the transaction uh all the transactions in the block that happened before. Um so this makes it really hard to implement but uh well that's not of your concerns because we did this hard we solved this hard problem. It's not theoretically hard it's just engineering hard like it's time that needs to be invested there. >> Did you get your question answered or you have one as well? >> You're good for now. So we have two that came in. I can't see for the lights up here. What makes symbolic fundamental different from traditional solidity bugger debuggers like remix or x had built-in debuggers? Yeah, so I I think there's multiple things. First of all, uh symbolic is integrated into visual studio code that is by the solidity developer survey the editor that is used the most. Um then solid the debugger allows you to really inspect local variables. That's something that no other debugger can do. And then there was this slide that I skipped about uh formal verification. Uh that means our debug is not just a it's just not a classical debugger but the name also symbolic comes from symbolic execution which means you can use it to formally verify your smart contracts. Um, so well being a formal verification company, that's one thing that we do. It's basically using math to prove that your test cases cannot fail on all inputs. That's a very simplified way of thinking about it, but I think it's a very intuitive way to think about it. Um and then yeah especially um um also I think remix and hardhead they don't have this rich ecosystem integration where you can use your debugger to um uh for example to inspect to simulate a transaction before you sign it. That's something that is I think unique to us. But I'm big fan of and I'm a user of these tools. So um I I I think but better use one of these tool one of these debuggers than than none of them. Like if symbolic doesn't fit you. If you don't like it, just try Remix or just try the hardhead debugger. Fair enough. Uh I think each of the these tools provide great value. Obviously I'm biased. >> We always are specialist coders. >> Well, thank you so much, R. If anybody have more questions, do catch him outside. He's going to be around the most of the day, right? Or do you want to fast go through the last question we have on the board? >> Uh, if we have the time, I want to go through it. >> We can make Mr. Smith wait a little longer, right? >> So, uh, >> how can symbolics support smart contract audit? Is it primary for developers or also useful auditors trying to validate assumptions? >> No, it's for both. Um it was born originally it was like runtime verification is also we also do audits and it was born out of our own need um to like to be better at audits and to save time on audits because audits are always time boxed. It's really hard to get into a new codebase. So our original um our original motivation for developing symbolic was really just to support our own audits and but then we quickly noticed okay developers find this equally useful. Um but yeah it's it's definitely for both groups equally. >> That's perfect to hear and thank you so much for everybody please give a hand for rule for amazing going forward. Thank you.