Off-Chain But Not Off Radar - DeFi Security Summit 2025

Transcript

Thank you Maxi. Hi everyone. Um, is it working? Right. Um, so yeah. For being here. I'm Paulina. I'm the CEO of Runtime Verification and I'm here to talk about some of our recent experience with doing infrastructure audits beyond smart contracts and share some cool advice that I hope you guys would find useful. Um, so what I mean by crypto infrastructure? Um, essentially the whole execution stack that enables the interaction between the user and the smart contract. If you do look at an example that is here, which is deploying smart contract source code, we'll realize that it does go through a lot of different components and it would be good to make sure that they are actually implemented correctly. So, for example, the smart contract first goes through

compiler. It gets compiled to bytecode that is included in the transaction deployment. It is being sent to the JSON RPC node and it should be up and running for that to happen. Then it gets included in the mempool, then it gets included in the block. Finally, the instructions uh, from this bytecode actually get processed by the virtual machine, where it is also very important that these instructions are being executed correctly and the blockchain state gets updated. So, I did list some of the examples of the components from this execution stack here. Um, like compilers, nodes, you know, virtual machines, consensus protocol, the whole ZK EVM infrastructure. And there are a lot of them and that is pretty much the point I wanted to make that all of this is code that is governing whether your

interaction with the blockchain is actually safe. Um, I did include this picture because I find it funny. Um, and it is true that uh, smart contract security has been pretty much the spotlight in this industry in the past years. Um, but to be fair, we do get a lot of inbound requests for this like infrastructure types of audits recently and I think that is genuinely the trend um, in the industry so uh, yeah, I think protocols actually do security seriously these days. Um, so what I want to talk about it in general? Like what is the difference between these types of audits and the smart contract audits. And there are a few um well, fundamental factors that are different. And the first one being the code base size. So, different from smart contracts where a few thousand

lines of code is, you know, pretty much the whole project. Um this code base is a very different. I ran cloc um a couple of days ago on some of the some of the clients. And here's what I got. Like, Reth, the Rust implementation of um Ethereum client, is 97,000 lines of Rust. And that is like the modular, compact, you know, efficient implementation of it. Uh guess the Go implementation is even bigger than that. Lighthouse, the consensus client, is 150,000 lines of Rust code. Uh that is excluding tests. You might think maybe there is a problem with like Ethereum infrastructure that is so big in size.

But if you look at Fire Dancer, which is Solana client, that is even bigger. It's 340,000 lines of C and C++ code. And of course, like with smart contracts, generally the current um you know, the idea of the audit is that someone, like an engineer, looks through every single line of code. But that is infeasible if we're talking about, you know, this magnitude. Um with these code bases. Uh >> [snorts] >> so, we kind of have to find some more efficient solutions. I mean, infeasible in the time frames that we usually, you know, operate with realistically when we're talking about audits.

Uh so, there are some solutions to this. I'll get back to them later. One more thing I want to highlight is that there are also different threat models and areas of concern when we talk about this type of software. So, um different from smart contracts, we do take care of things like um chain split, you know, denial of service, memory exhaustion. Um it depends depending on the purpose of the component we're looking at. Uh we also are trying to identify different potential issues. Like, in the case of consensus, um we are worried about like leader election. We want it to be fair. We want it to like not be gamed, you know, we want um consensus and execution layer to be aligned. So, you know, all these sort of things um that we have to consider. And in addition to that, um these components can also be implemented

in different languages that have different memory safety. So, you know, just a lot of things to be familiar with. Um so, what are the techniques like what instruments do we have for actually reviewing? And well, generally all the usual suspects, similar things to smart contracts. So, first of all, of course, manual review. This industry is pretty big on that and like having a human actually look at the code is still, you know, uh I think highest guarantee that we can get other than formal verification. Uh but it does scale less as we've discussed to this size of the code base. So, we have some other techniques that we can use to scale this. Um like static analysis, testing, fuzzing. I'll talk a a bit more um later. So, what do we do with manual review? The thing we do at Runtime Verification is we found that for us the

best thing to do is to have like a sequence of shorter engagements where we do very focused manual review on high priority code portions. Um having this like 6 to 8 weeks uh does help us avoid like auditor burnout. And then in addition to that, it also gives the chance uh to the developers to like fix some of the issues we've identified in the previous round um and then we can move on. So, how do we figure out what are the high priority code portions uh we are looking at? Depends on the project, but it can be newer code. If uh some components of the code are well audited and tested, we can focus on like points of interaction to make sure that they interact well um between each other. If we are looking at a refer at a something that has a reference implementation,

like there is a client for an EVM chain and then there is like an EVM compatible chain, we're looking at if there is some difference between them, then that is something for us to focus on. Um like one example being if um like an EVM compatible chain has a different uh gas pricing, like if it re-prices some of the opcodes, then it might lead to the denial of service. So, we want to look at it like really carefully. Uh and then of course, like really important code. Like really important or um unsafe. So, one example being that Rust generally is considered a memory safe language, but there is a keyword unsafe that helps you like avoid some of the safety. So, what we did for one of the project is we went through all the mentions of this unsafe keyword and we made sure that the assumptions that

developers are making um about it being safe are actually true and we documented all of this. Um and then also another approach to like identifying what is really important is to uh define a set of properties or invariants that are critical for this particular piece of software. Um that is why we strongly advocate for doing a design review first. So, we spend a few days or a week, you know, depends on the project and the timeline trying to understand really well what does this project do and whether the design makes sense. Um and uh try to identify some some properties, put together the specification because it does help a lot uh in informing what is the review being focused on.

Um in addition to that, like to scale it somewhat beyond just these key points we're looking at with manual review, we also use um tool-assisted review. There are static analysis tools depending on the language like cargo audit scans dependencies in Rust projects, which is very important especially considering this like recent influx of uh supply chain attacks. Uh and we do use AI quite a lot to look at like other parts of the code bases. So, like anything that, you know, we don't do manual review of in in that as well. Um just so we get, you know, just in case it can uncover some more issues and honestly it does. We are working with Almanax that is like an AI tool um for smart contract and like not smart contract infrastructure security as

well. Um and yeah, it's been working really well for us. It does identify issues. Uh one trick that we've learned is that work better if you provide specification. So, if you try to ask it not only find vulnerabilities it can think of itself, but also the difference with between the specification. And one example of an issue we found this way uh that cannot be more specific than that, but essentially it found uh a bug where the function was making assumptions about something like something would be invalidated in the upper function that was calling this one, but it wasn't. And it would be really hard for the AI tool to well, just infer it in the first run.

Uh so, yeah, having the specification helped a lot and that is something that we actually um come up with during the design review stage. So, yeah, it is has been extremely helpful with like both parts of um this process. Then, um what else can we do? So, um fuzzing is another well-known technique, extremely efficient, really nice way to, you know, also scale the security of uh guarantees that that you're trying to provide. So, uh there are different flavors of fuzzing. We do all that I am mentioning here, but the first one is panic focused. So, that is like you try to uh invoke parts of the code base like you call functions, you try to interact with the like node through RPC, and then you just feed, you know, random like pseudo-random inputs and you hope that

it crashes. So, that is what fuzzing is. It also identify different types of vulnerabilities like out of bound access, uh resource exhaustion, all types of crashes. The example that I have here is not from our review and it's not blockchain specific, but I couldn't help like I think it would be illegal for me to not include it. That is from the Cloudflare um well, issue that disabled half of the internet on Tuesday. And the reason for that was that uh there was a panic in unwrap call in Rust that is like a panic in function. So, it just it it just crashed uh with the bad input. So, that is exactly the type of issues that we are trying to prevent with um this type of fuzzing.

We can go beyond that. We can do property-based fuzzing where not only we make sure that when we call the function it doesn't crash, we also assert something about what it actually does. So, one example of that uh that we did in our audits was round trip conversion between types. And um I think uh so, generally the idea is that we convert some value to one type, then we convert it back, and then we make sure that the result is the same. Um we can do like we can serialize some value and deserialize, make sure it is the same, and we can also do like more high-level uh stuff that we can come up with if we do design review properly.

Um and then one more type of fuzzing that I really want to mention is differential fuzzing. So, differential fuzzing involves running um two pieces of software alongside each other and checking that on all inputs they do behave similarly. Um that has been proven very like extremely efficient in identifying bugs. It does require having a reference implementation. So, depends on the situation um you we can do, you know, we can set it up differently. So, one type of differential fuzzing that we have been doing uh is running different clients for the same chain alongside each other, making sure that they do not disagree. Because if they do disagree, then you know, some of the nodes are rejecting a

transaction, the other considers valid, it can lead to chain split or halt or, you know, god knows what. Um so, some example of that is like checking that Rust is behaving similarly to Geth. Um the guys from Sigma Prime also published a report about a very nice engagement that did a very similar thing to one of the L1s, so I highly recommend checking that as well. And we did find an issue where uh essentially some of the like node implementation for Solana was rejecting empty transactions and the other wasn't. So, that is obviously an issue. Um we can do that for uh just different chains that, for example, are EVM compatible, making sure that the parts that are common between two blockchains, um you know, really do behave similarly.

Um we can check if implementation adheres to specification if you do have, you know, specification or a formal model such as KVM, which is our uh EVM implementation in K, that is the formal language. Uh or you can just, you know, generally if you do have two implementations of the same thing, you can, you know, differentially fuzz it. So, we did this for um the Rust implementations of WASM interpreter, and it also uh helped identify some of the bugs. So, a couple more notes on on fuzzing. Obviously, this setup is very language specific and component specific.

An important thing to keep in mind is that it has to be meaningful. So, as like some examples are that in order to test asynchronous execution, we really want to have like more than one transaction or more than one blocks depending on what is asynchronous there because we want to make sure that we exercise you know the execution path that corresponds to that functionality. If we are looking at the virtual machine that executes instructions, then we actually want to feed it valid instruction sequences that would mimic the actual code that is that is going to execute. And of course depending on the language you're working with, that is going to be different. So, if you work with Rust to generate the structured inputs, we use arbitrary that is a crate that has been very helpful. You know, it is different in Go. So, you know, there is the whole

toolkit attached to all every language. Every language as I mentioned before has its own like potential issues. So, we didn't really find a better solution than just you know spending a lot of time looking at the making sure we're really familiar with the with the code base, with what the protocol does, with the specifics of the languages we're working with. And then another thing to keep in mind is that when I'm talking about design review like understanding the protocol is very important, but that is something where AI has been also extremely helpful for us. We have been using Deep Wiki quite extensively especially the early stages of the engagement when just trying you know, put together a good idea of what the project does, what are the components, how they interact with each other.

So, that being like cross validated with the client team has also been like extremely extremely helpful in speeding up this process. And well, I wouldn't be myself if I didn't mention formal verification. So, that is the process of mathematically proving that the software is correct. As we all know, probably software formal verification is challenging, it is resource consuming, time consuming, requires a lot of groundwork. Um it relies on tools that are inherently like either not very scalable or have really challenging UX.

Um but there are still components that can be formally verified um if we are strategic about it. So uh I mostly focus this talk on the off-chain things, but uh some of the infrastructure uh does rely on smart contracts. So for example, bridges or L2s uh sometimes do use smart contracts that emit events for these events to be um received or like triggering some um off-chain infrastructure as well. So for these contracts, you know, we can formally verify that events are emitted correctly, we can formally verify that if they are paused, then they cannot be called successfully anymore. These are all things that we have proved for uh some of the L2s, and there are production-grade formal verification tools like um well, our control certora prover, um halmos, that are, you know,

that can deal with that. Uh and then one more thing that I think we did at RV at like 2019 uh was the verification of the deposit 2.0 smart contract that stores like 200 billion dollars or something like that right now. So that is important to make sure that it is correct, and while formally verifying it, we actually did uncover some viper bugs, and compiler bugs generally are really challenging to identify, so that is where like formal verification does um help identify issues that would be hard to find otherwise. And I think Certora uh the guys from Certora also identified some compiler bugs by doing formal verification of smart contracts.

Um if you go deeper, like the on-smart contracts, uh we can do things like like formally verify equivalence between different implementations of EVM. That is one of the projects we worked on. We proved the equivalence between KVM, our formal model, and Nethermind's EVM Yul, um making sure that the opcodes are implemented >> [clears throat] >> and represented similarly. Uh and it we did identify some some places where that was a bit different. And we can also do that with uh other EVM implementations like RV and the Rust one, which is also one of the projects we were doing, which is very important because RV and powers a lot of ZK EVMs. So, uh we actually would like to make sure that it works correctly. Um and then yeah, of course we can do things like we can model protocols, we can model consensus protocols and

formally verify them. Uh that is something we've done before and that I personally believe is better done at the like earlier stages of the development process. Um and yeah, finally we can also select uh some specific components uh that are, you know, small for us to reason about them efficiently like data structures, like important operations on data structures, um and this sort of things. So, I would like to wrap this up with some practical advice uh based on our experience at RV. So, what works for us best is shorter engagements or like sequence of shorter engagements because as I've mentioned, it helps auditors stay focused, it allows some uh leeway for the protocol developers to actually fix issues between that.

Um and with priority in the quarter audits given to complex, critical, new, important code, um unsafe. So, something that is very important for a human being to look at. Um and then we do recommend starting with defining specifications, threat model, invariants, um you know, putting together the specification basically and using that to inform the review. So, we do both AA review and manual review against these properties because that does add like an additional dimension um to code review that we are doing, helping identify uh differences between the intent or specification and the code, not just vulnerabilities that are, you know, present themselves in the code uh per se.

We do recommend obviously building a fuzzing harness and well, first of all because it does help identify issues. Um and then it also helps with uh the code getting evolved. If you can reuse it, uh then you can continue running this um and see if that doesn't cover any new issues. Although the challenge with that is that it is very like stack specific and target specific for which we also should have a very good idea of what the project does. And then for formal verification, you know, we recommend applying it selectively. It doesn't fit very well in this like 6 to 8 week engagement depending on, you know, what the what it is the formal verification that we are doing and what it is focused on.

But yeah, generally speaking, of course, it does provide the best security guarantees out of all of this tooling. So, yeah, cannot not recommend using it. Yeah, finally we do use AI assisted review as I've mentioned for extra breath. It does help us look at the parts of the code base that just would be infeasible for us for like human beings to look at. So, it does help identify issues that perhaps, you know, we would not have been able to find otherwise within this like very short time boxed type of engagements. But it does work best when you do provide the specification. So, yeah, I would recommend doing that.

And yeah, that is it for my presentation. Thank you so much. I hope that has been helpful. And please let me know if you have any questions if we have time for that. >> Thank you. Thanks, Polina.