Streamlining Security Audits with AuditHub - DeFi Security Summit 2025

Transcript

All right. Uh do people So hands do people have internet here? Okay. So I'm going to have a hands-on experience uh with our platform. Uh so you can scan this QR code to get access. Um and Ben is going to on board you to our uh platform. So I'm going to do a very brief uh presentation about like you know the platform and what it does and then uh once you submit this form uh Ben over there is going to onboard you to the platform and after I'm done with my little spits

uh you guys will be able to find bugs uh in the protocols we going to play with um All right. >> Okay. So, of hands, how how many people have run an audit here or be a part of an audit?

Okay, few few people. Uh so, okay, I'm here to present today our platform. I'm KTOS. I'm the CTO of Veridise. Uh we are a security firm. We do a lot of audits. Uh but we also develop a lot of automated tools uh internally to help development teams and researchers to find bugs on their own. Uh and we do that for both DeFi and ZK. And so we recently um released our platform called audit hub that houses all of the tools that we have developed like internally and it also has some cool auditing features.

So let's go and see how what motivate us to like do release this platform. So if you have ever participated in a audit process or any kind kind of audit review as an auditor you know that typically there are two phases. you have the first phase where you do uh the code review. Uh that's when the main action happens when like you know auditors go and find bugs uh and uh communicate with the clients. Uh and then there is like the fixed review that happens sometime after the audit has finished. So during an audit uh an auditor usually has a communication channel to communicate with the developers of the protocol that they're auditing.

uh and then they usually have a different communication channel to coordinate uh with the auditors that they participate uh in the audit with and sometimes they might run some like you know external tooling. So they're going to interact with the tooling as well. Uh and then at some point the review is going to finish going to start uh the fix the fixed review is going to start for uh audit a that is the audit up there and then another audit is going to start while you do the fixed review for the previous one where you're going to start communicating with another auditor for the new audit and the new developers for the new protocol and on top of that uh it might be the case that

uh the developer from the first audit starts submitting fixes. So you go you have to go back and remember what was the issue uh see if they fixed it properly uh and so and so forth. Uh so as you can see as a single auditor on your day-to-day you might have like a lot of interactions with like you know tools uh developers from different teams and uh auditors within your team. So, uh your day-to-day might end up like looking something like that where you have to track a gazillion of conversations between different uh platforms and then also kind of like you know remember uh who submitted a fixy a fix for an issue if the fix is okay uh

and so and so forth. So uh what is the result of this uh whole process? You have a very fragmented communication between like you know um you know doing audits uh talking to clients. You have to context switch between different software where you kind of like you know track your auditing workload where you share the uh issues with your clients. Uh and from a client's perspective the audit feels like an entire black box. They don't know what you're doing what type of checks you are doing on their codebase. they cannot help you get unstuck that quickly if you are kind of like you know looking at specific area

of the code that at the end of the day they know better. So how can we fix that? So we tried a lot of solutions internally kind of like you know configuring different type of like text stacks to kind of like create a smooth auditing experience and all of them fell short. So we decided to build our own thing uh to help kind of like you know auditors untangle uh this uh mess. So this is where our uh auditab platform comes in place where security concepts are a first class citizens. Uh so all it have like a set has a set of um uh key features

uh where you can run automated tools. At the time being uh we offer uh tools developed by us internally but in the future we have plans in incorporating more uh security tools. Uh it also gives you uh an efficient way of managing the audits uh issues. Uh and also you can uh use audit hub to uh track and resolve conversations on any security topics. You can have conversations from uh things on a specific line of code to like a finding reported by a static analyzer to uh the issues themselves, right? like you know because sometimes

the client might argue that like you know something uh is not correcting the issue or like you know the uh the issue itself is not valid. All right. So what's the result of that? So uh first of all uh we have a very increased transparency from the client's perspective. So they can following along uh with you as you audit, track conversations, see what checks are you running, what tools have you run and also uh it creates a more streamlined and efficient uh uh process for the auditors. The auditors are more

efficient. they don't have to context switch as uh as much and overall audit have audit hub serves as the main communication channel instead of like having uh a few different channels where you communicate with different entities at the time you use audit hub and you do everything in a single uh software. So we have kind of like a win-win situation here with where both the clients uh are happier and also the auditors are more efficient and uh they don't have to kind of like track all of these dependencies uh and incur a lot of like cognitive load.

Uh and we have been using audit hub uh internally for our audits uh for quite a while now. And uh developers that get an audit with us, they always feel uh more happy to see kind of like you know what's going on during an audit with something they have paid for. And overall they report that the whole experience is smoother and it's kind of like you know replaces this kind of like you know uh bland PDF that comes at the end of a security review.

So uh as I mentioned earlier uh currently audit hub hosts uh uh several security tools developed by uh our engineers and we have uh security tools that can help you find bugs or uh uh or prove that things are correct in your codebase for both ZK uh and uh defy smart contracts. Specifically for ZK, we have a static analy analyzer ZK vanguard uh in Pyus uh which is a verifier that helps you uh prove that your circuits are properly constrained and if they're not going to return you a counter example and on the

D5 side we have uh D5 Vanguard which is a static analyzer uh and Orca which is a guided specification uh a specification guided fuzzer. Uh and all of these tools can either uh work out of the box. We have some kind of like you know predefined checks that they can do in order to detect bugs or they can be customized uh uh for your uh specific protocol for the protocol that you're currently either developing or reviewing.

Um, oh, and all of those like one more thing that I want to mention here, all of those tools are built uh on top of this theoretic framework that comes from these branchs of academia called formal methods. So all of these tools come with formal guarantees. So for example for the static analyzers if the static analyzer tells you that uh a uh a buggy pattern doesn't exist uh it means that like you know your code base is free of this uh bug uh and if the verifier for example pyos if it tells us that like you know the uh the uh the circuit is properly constrained we can take that as a proof of approval

from the verifier. Um all right and then we have been using like this thing uh internally and also like you know our clients have started like using it themselves. We have several success stories for example risk zero uh when they came to us for an audit we used uh we adapted and used pyers to find like several bugs. If you count count if you have counted pyus as an auditor you it will have been the best auditor of the of the audit as it found uh nine nondeterministic circuits uh and the majority of them they were critical and high we have some uh blog post there where you can read uh more stuff uh we have done uh kind of like a similar engagement with sustain not

during an audit but during their development process uh we have help and find some interesting bugs as they develop circuits uh and so forth. Okay. So, uh I'm going to do a quick demo of the platform now. Uh I'm going to put this uh um uh this slide back again after I finish with the demo. An important thing for people who just came in. Uh if you wanna uh use the platform uh with me to find bugs after I finish with my demo, uh click this uh scan this signing up sign up form and we're going to onboard you to the platform. Uh my colleague has to go give another talk,

but like you know after I'm done with the demo, uh I'm going to let you kind of like play with the platform. I'm going to stay around for questions and if you haven't been or on boarded already, I'm going to on board you afterwards. Uh and then if you want to read at any at any moment uh anything about audit hub, we have the documentation site here. Uh if you're using OpenAI, you can also search for a custom uh chat CPT called audit hub GPT and you can ask it questions about the documentation. It's going to help uh it's going to help you answer and also it can help you uh write specifications and custom detectors which I'm going to talk about them uh in a minute. Uh after the workshop uh if you want to uh talk

with us ask questions about the tools or anything you can join our uh audit hub discord. Uh and more information about audit hub can be found uh on this site. Uh so for people who just joined if you going to if you wanna uh get access to the platform scan the sign up form there it's very easy just email name uh and affiliation if you want to and we'll give you access to the platform. So let's uh let's uh uh do like a small demo uh with this u uh a small demo about audit hub. So once you get into audit hub this is kind of like you know the interface that you see everything is

organized in uh groups of projects like it's uh each project belong to an organization. Uh if you click inside the organization you go and see kind of like you know the the code viewer here. Um and uh you can kind of like you know uh auditab gives you the ability to start conversation on any uh code of the of any piece of code. For example, you can say here uh this uh seems suspicious.

Uh and then write something here. Uh and then create a thread. And then like you know once you create a thread uh you can see it here and like other people can join in uh in the conversation. Um one other thing you can do is like you can access uh the tools uh we offer within uh audit hub and you can like you know set them up uh to run. So for example here orcha is our fuzzer uh you can set up basic uh parameters here u other advanced settings uh select some stuff and then like you know uh you can uh make you can launch a task and the task will appear uh here

down here or you can access it from uh this uh uh this panel uh once a task. This is a test that uh I I have like run in the past. Once the test finishes, you can get like you know the results. It will show you uh uh it will show you kind of like uh a findings if it found one. Uh you can also access it uh the the findings from like this view that is a bit like you know easier to to navigate.

Um so this is kind of like you know the basic things you can do. Right now we are working on more views instead of like you know the code view here we're going to aggregate like things like you know findings from the tools uh issues and so on and so forth. Uh oh also findings and issues from the audit uh are also available uh here. So uh for the exercise I want you to go uh today uh we have uh a we have a protocol uh here. One second.

I need to uh I need to move some uh uh some uh um some windows to show you my VS Code, but I'll show you it in a bit. Uh so uh we have two types of projects. One defy project. This is the resupply finance uh uh project. It's a solidity project and also for people that like you know no zk zk. We have like circuits from uh a risk 5 zkm. Uh and then like I'll show you how you can kind of like you know use our tools to find some existing bugs in these systems. And then uh we have injected some more bugs inside these uh

protocols and you can use our tools to kind of like you know play around and see if you can find uh the bugs uh yourself. So uh let's go and and see how uh we can find the um uh the bugs uh with audit hub. So if you have been following the uh if you have been following like recent hacks there there has been recently the the in like mid of this uh year there has been like this uh hack on the resupply uh

finance protocol uh which was kind of like a combination of uh oracle manipulation attack and some loss of precision. So the root cause of this uh the root cause of this bug was that in this uh in this division here uh the protocol got the price from uh this oracle and this oracle returned a very high price. So this uh division got truncated to zero. Uh and once then it went and store this exchange rate in a storage variable which then uh it flew into the issolvent

um function. Okay, here. So yeah then this exchange rate uh when here we checks whether the user is solvent and then if exchange rate is zero uh then the LTV is going to become zero because we uh you know uh calculate that uh on top of uh you know directly here with a uh multiplication and if if LTV is zero then the user is always solvent even though even if uh they're not solvent. So that's that was kind of like you know the root cause of

the of the hack and then they lost around like 10 millions and the tricky part here is that like you know essentially you have a division before uh a multiplication uh but this type of bugs cannot be caught by uh static analyzers like slither because of two reasons. First of all, uh there is a storage right uh in the in the beginning from the uh from the first function that I I showed you. And second of all, uh the uh the flow from the initial uh initial division to the solveny check here is interprocedural. So slither does have a a detector for like you know checking

division before multiplication but it won't detect like this bug because as I said you have interprocedural uh control flow and there is a store right in the middle. So let's see how we can use uh one of our tools to find like actually two two of our of our tools to find uh this hack that cost um resupply finance $10 million. So uh we have a static analyzer D5 Vanguard uh which can be specialized uh for your protocol and um you can write custom queries to detect patterns that you uh suspect

might be that like you know uh they might uh they might present buggy exploits in your in your protocol. So here uh you can provide our static analyzer with this uh little file that shows you how uh you can detect like this interprocedural define divide before multiply. So this is kind of like a generic uh uh detector that you can use uh with our uh with our static analyzer. Uh and essentially you can see more details in the docs but on a high level uh this first part finds all of the divisions that write to a storage

variable. Then this second part finds all the multiplications that read from a storage variable. And then finally this work close uh tells our static analyzer to keep uh only the division and multiplications that refer to the same storage variable. So this is essentially a a very sophisticated divide before multiply detector. And in in if your protocol has some kind of like you know high critical storage variables you can further customize it and say you know I only care about variable exchange rate as the uh as the resupply finance hack uh shows us.

So I have already uh run our static analyzer from uh from our uh in our dashboard here. Uh, and if you go to this uh oop, sorry, it's this task. Give me one second. Okay. Uh, this task. Okay. So, you can go uh in the findings and then you can uh search uh to see if it found the if it found the bug. And as you can see, it points exactly to to the exploit. So you go um here and then you can interact with the

finding. You can go to the check and then you see you it it first points to the to the division that caused the loss of precision. And then uh it points you to the to the multiplication that received this zero and like essentially could make every every user solvent if that division uh return uh returns zero. Um so this is kind of like a way of like you know writing custom detectors for your protocol uh to kind of like detect buggy patterns. But as we know static analyzers might uh return kind of like you know warnings that are not exploitable. They might be uh false alarm.

Um so uh another thing we can do is like you know we can use our fuzzer uh to see if this uh if this pattern is actually exploitable. So our faser is very uh highly customizable and uh all you need to do is provide it with a deployment script to deploy your protocol and you can do that either like locally or like on a blockchain. uh it works on on both uh in both modes and then it can get like a specification that is very uh very declarative and it can kind of like you know uh encode the

solveny check uh very easily. So you don't need to kind of like you know understand much about the language right now. uh there are more information in the docs that I have provided uh earlier but essentially what it says us what it tells us here is that I want the user to be solvent whenever uh these three functions uh terminate. So if you run our uh fuzzer against this protocol uh you can see that it kind of like complains that this uh uh specification can be violated. Uh actually let me access it from the other dashboard here. So um okay and then our fer is going to uh

return uh a counter example that it shows you like you know the test that can exploit your protocol and it shows you which uh uh which functions must be called and what uh with what values. Um okay that's for the defi stuff. Uh I want to show one more small feature before I end. Uh a complicated thing when you when it comes to uh static analyzers is going over uh their results and kind of like filter them out whether they are uh false positives or uh true uh true bugs. Uh our uh dashboard here lets you do that uh very conveniently.

And also uh I wrote I wrote I run this very standard use before definition detector here where uh it checks for cases where you use a variable before it was initialized. Uh this can generate a lot of warnings and it might be tedious to go over them you know one by one but our system uh gives you kind of like the ability to kind of like mark root causes of like these issues as invalid. So for example here you might know that this initializer here that our system kind of like you know detects automatically is guaranteed to call before this uh variable is going to be used. So you tell that to our system and then it's going to propagate this information to

the rest of the findings and it's going to eliminate like other uh false alarms on its own. uh and not only that if this same root cause uh appears in uh subsequent runs of the static analyzer our system is going to remember that and it's going to apply these actions uh automatically. Um so that's kind of like you know the small tutorial on the DI side. Uh you can start playing around uh if you care only for DeFi. I'm going to do a very small uh tutorial on the ZK side because they are things are uh more straightforward.

Uh so our platform supports several uh ZK languages. We have developed this language with the theorem foundation and intermediate representation that you we use to lower several uh DSLs and frameworks uh that use uh that are being used to uh kind of like develop ZK circuits. Right now, our platform runs on top of the intermediate representation. We haven't uh integrated the front ends yet because uh they're under heavy development and they say all the time. But like I'm going to show you uh here uh how you can um uh use our static analyzer and our uh verifier to find bugs or kind of like you know prove

that your circuits are correct. Uh so uh we have like a very small uh circum uh file here and uh it contains some bugs. Uh you can run our static analyzer. Uh you can select whatever detector you want to run and then you just like you know hit uh you hit uh you select uh what file you want to run it on uh and you send run and it start running. I have a result already uh so we don't have to wait for it to finish. And then you can see in the findings it points two uh two places in this less than uh power uh uh template.

uh and if you kind of like you know read the uh if you read the definition of the circuit everything is completely under constraint out um doesn't does not capture uh the intended behavior of the circuit and as you can see in here does not participate in any constraints and our and our uh static analyzer points to both of these facts. Uh so uh let's see also how pyus can be used to uh find uh uh bugs inside circuits.

So we have this oops sorry wrong uh okay so we have this uh this circuit from like risk zero's internal uh uh internal representation uh and we have intentionally like you know inserted the back here uh that uh uh a constraint is essentially like missing. So I have already run pyus on on this file. Uh, and oops, like yeah, yeah, that's the wrong um on this file. And as you can see, it can like return like a counter example

and it essentially shows you uh the bug for this specific circuit. And then it it kind of like returns you for a single input uh multiple output values that can kind of like satisfy uh this uh that can satisfy this constraint. Sorry, I'm like hearing like all of the sound uh from outside and it's hard to speak. Um, and then uh then if you go and fix the bug if you introduce the constraints bug uh you can uh run the uh you can run pyus and it won't find any counter examples and it will like uh tell you that everything is okay and that the

circuit is verified. All right. Uh I think all that's all I had uh in terms of features. Uh one last thing, if you are an auditor, uh you can also uh create issues for your clients to like see uh you can enter a title here. Uh select like uh likelihood, you know, what's the impact severity uh what type is it. It keeps track who raised the issue. Uh you you have to select like a location and then uh you have like um a markdown editor to write the issue and then once the issue is created

uh you can like you know go view it. The clients can go view it. You can have conversations either publicly with the clients or privately uh with other auditors. So like these conversations will be hidden from the client and uh you can then uh you can use some actions we have like down here to notify other auditors and then like you know keep track of fixes uh and so and so forth. All right. So that's all I had in terms of bon in terms of demo. Uh I'm going to leave this uh slide up uh where it has all of the information uh you need to start playing with the platform. Um you can go to the documentation site. Uh

it has like informations on how to like you know write specifications, how to write write custom detectors uh for our uh tools. Uh it can show you how to create issu create tasks and stuff like that. I'll be around if you have like any questions. I can uh answer them. Um, and yeah, we have injected a few fun bugs uh that you can use uh the uh you can use our platform to find them with our tools. Uh, I'm going to on board whoever hasn't been on boarded uh yet in a bit. Um, oh, one thing I forgot is that if you want to create custom detectors or um or specifications

uh to run with to uh use for with our uh with our tools. You just have to go to this organization settings here uh on top of your bubble and you can create uh v specifications hints which like you know we describe in the documentation what they are and and custom detectors. Um, all right, back to the slide and start playing with the platform if you haven't started already. Uh, we're going to give you access throughout like the next week. Uh, if people is anybody who doesn't have Ethernet and wants to kind

of like uh join the platform like later on. All right. Okay. If everybody has Ethernet, just submit the uh the form there. Otherwise, I can get your email and name and like I can add you like later. Um, and yeah, I'll be around for questions. Uh, and happy hiking. also give you before you before we start

people leaving. If you give us feedback on the platform, uh we're going to give you a month uh to access the platform and you can upload whatever code you want. Right now, just to make it easy for people that participate in the workshop, we have locked down the code that can be run, but if you give us feedback, we're going to give you a month to do whatever you want. Uh Heat. Heat.

Heat. Heat. Charles. Hey,

>> thank you very much for the workshop. >> Yeah. Yeah. Thank you for Yeah. I would have to go to a now, but that's why I couldn't stay. But I'm super