DeFi Security Summit 2026: Amber Room, Day 1

Transcript

foundation. Thanks for helping us. Thanks for helping us. It's an event which is for the community. Uh Defy Security Summit is a nonprofit organization. Uh of course we have been uh sponsoring DSS and helping it and creating it and actually putting a lot of the people in our team and thank you all for coming. I'll have Rajiv here [applause] GM So I don't have much to add after uh MUI. I mean this is uh been a fantastic community DSS this is uh the fifth year and uh it's it's always fascinating to meet the community in a different part

of the world and it's the community has grown in the last 5 years. It's somewhat shrunk and in some sense distances are real. uh you know visa issues are real, travel is real and this is I think the at least for me I I'm I'm based in India so this is the shortest flight that I've ever had to take for a DSS uh but for many of the others uh really appreciate you guys taking the time and effort to fly from you know half the the other side of the world right um 24-hour flights and jet lags and so on so yeah Thank thank you all for coming. Um and

like Mully said, we have u two days of fantastic programming. Um like they say, there's never a dull moment in crypto and I'm sure all of us have been following the news in the last uh couple of days. Uh it's just uh tragic in terms of all the incidents that happen and what we have here um in the security community is we keep you know trying to come up with technical solutions raise awareness and in many ways um I don't know if you have heard of this phrase it's um the Cassandra's curse if you know that right so there's there's this funny story you can look it up I mean it's a myth

logical story and security folks are known to keep um warning people that hey you know bad things will happen. Um but it's it's it's like a failure at many levels. Um a lot of technology, a lot of psychology, a lot of um sort of mismanagement of risk. Um but but that's that's why we are all here, right? Is to help try to fix these problems. um meet with the community, figure out what's the latest stuff that's gone um gone right, gone wrong, and how can we really raise the bar? And like like we all know in security, it's it's not a binary thing. It's not a zero or one. We just

keep trying to do better. But of course, the attack surface keeps getting better. I mean, keeps getting bigger and um things fall through the cracks, right? So the Swiss cheese is real. So um you will hear a lot of talks uh fantastic speakers. We have um long talks uh 15 minutes long. Uh we have short talks that are really hot and crisp topics for 5 minutes and then we have some of the best speakers um give keynotes in the mornings and we'll have more logistics but we have two rooms here. This is Amber. There's Pearl upstairs and we have parallel sessions going on. So please look up the schedule. Um QZ and

team have done a fantastic job with the entire operations. So take a look at the website. It it should be fairly accurate unless we have uh a few key you know speakers drop off. Um but yeah so that's um that's the next two days for you and there is also a third day if you remember for people who have been how many of you have been to uh how many of for how many of you is this the first DSS? Wow. Okay. Uh the second third. Okay. We have quite a few repeats as well. Um so >> yeah. Yeah. [laughter] Um so we have had uh this concept of D5 101 which used to be on the first day of

DSS and introductory workshops for uh people coming on. Uh but this time we sort of flipped the script and D5 101 is really going to happen on the third day. It's going to happen on uh Tuesday at the DevCon venue and this is a set of uh panels this time, right? So really some heavyhitting topics in security with some of the um you know people leading people in the space. So the only clarification is that to enter so you would need to enter the DEFCON venue.

You will need a DevCon ticket u on Tuesday to attend these panels. So just make sure you get that clarified but but otherwise yeah um welcome again and I'll um hand the mic over to QZ. Hi everyone, thanks for coming. Um, so I'm QZY, otherwise known as the ops email that's handling all of the speakers. So, thank you everyone. No worries. [laughter] Thank you everyone for u being on time for working with us. Just wanted to say a few words. I think um my background is in running events with like Ethereum Singapore uh DAC day. Um and actually I started out as a security researcher. So

I always have a soft spot for the security community. I think security is kind of like a form of care. Um thank you for keeping Ethereum DeFi safe. Um, this is very important because as we take on this big journey to try and bring people onto Ethereum, onto better systems, we need to make sure that they're well taken care of. Um, this is especially important, but more importantly, I think that we are entering a very interesting time where what we learn in the Ethereum space can actually be applied outside of Ethereum. And I feel like security is the best way to go because um it is very provable and also it's something that you can have a real conversation with without talking about tokens or you know all that stuff.

So I love folks in security you guys are the most uh sharp uh intelligent community I've seen and what I believe when putting the event together with their folio is that I think we should be community in spirit but professionally run. So I hope you enjoy what we put together and uh let me invite Denver to say a few words. >> Thank you. Um and I'm co-founder of Defolio. Defolio originally started off as a hackathon platform and we have been running uh hackathons, grant programs, fellowships u here in India across the world um for the Ethereum community since a while now. And um it was simply amazing uh when we got together with Qi um and Muli and Rajiv to put this

together. DSS is a summit that I've looked up to um for for a while now um in in in all our travels and so glad that we could make it um happen here in India and so so glad to have all of you like like Rajiv and Mully said fly halfway across the world uh to make it here. It's a very special uh moment in time and I think the work that um you all are doing here is like extremely pivotal um to to to the fabric of of humanity in a way right because um that's the common substrate that all of us are going to depend on in the future

and it's our responsibility to ensure that everything is uh secure so that people can reliably build on top of it. So that's why really excited for D5 security summit and um just last one one last bit as an organizer I'd just like to remind you everyone here is governed under um a code of conduct. Um you can find it um on our Luma page and in communications that we have sent out. Um but it's like it's not rocket science. It's just we just like to be nice and respectful to to each other and as long as we have that um we're going to have a great show. Uh but yeah, thanks thanks everyone again for coming here together.

Okay, thank you for your support. [applause] >> Someone has to say >> all right. Um so yeah so we are uh we try to keep time here. Um so like we said there are two rooms. This is Amber there's Pearl. Look up the website. All the talks are there. They're going to be running in parallel. And uh yeah so we're going to kick this off with uh a

special opening keynote by the one and only Peter. >> Thank you. Thank you. [applause] >> Hey folks. While we're waiting for slides to load all right, welcome everyone. Namaste India. It's so good to have every single one of you.

Welcome to the state of DeFi security. It's an honor to give this talk now fourth year in a row where we look back at the industry and learn. So in case we haven't met, my name is Peter Cashinsky. I'm the editor of the blockchain thread intelligence newsletter for the past eight years and also a security adviser to some of the projects out there. So before we begin, a quick announcement. In light of everything that was happening in the past two days, I decided to put the blockchain thread intelligence newsletter out out there as a public good, freely accessible, so you can subscribe, learn, and hopefully get the lessons to not get hacked.

So, let's begin our story. Usually, when we gather here, we jump into the statistics and the threat models and all the case studies. But I want to do something different today. I want to tell you a story. It's a western. It has a nasty two gangs operating there. There are lots of rob banks and some of you are in it as well. Maybe the slides.

There you go. So, get to get an idea of how we got to these pretty tough times. We have to start at the beginning, the drought. Our story begins in the winter of 2025, 2026. Just as we all coming down from the hangover of the bull market of the past year, Bitcoin just hit 60K. And all of the projects out there are starting to really tighten their belts. The budgets are getting cut, especially security budgets. Audit jobs and contests and other security work that used to be a plenty in the past year are really going down.

Suddenly, all of the security researchers out there who used to be really busy and could make a decent living find themselves unemployed without a job on a curb with no future prospects. Some of the smarter of you switched over to bounty hunting and that worked for a little while until bounty programs just like the rest of the world were overwhelmed by the AI slop and started introducing various types of friction especially the submission fees. And just to give you a context of the world both inside crypto and outside crypto, what was happening with the AI craze invading everyone? Managers and founders realize their ultimate goal of

having employees who don't sleep, don't eat, don't require any asks and just work, work, work all day. So AI is going to write the code, test the code, audit the code, and that's how the layoffs begin all around the world. And just around that same time when the whole AI seems to be taking over the world, the frontier models introduce excellent models like Opus 46 and GPT53 where a year ago these models could not even tell a difference between re-entrance and price oracles. Suddenly you could get readymade foundry PC's

that you could just run on the mainet and hack whatever you want to. And it is in this context where you have a whole bunch of security researchers who are wellkilled and now very well equipped out of the job in the down market. What do they do? Well, a lot of them they left the market altogether. They moved on to other jobs. But some of them they burned the whole town down. We went from three or four hacks a week to three or four a day.

The last time we met here in in Argentina, we had just 24 hacks a month. By April, as we'll call it bloody April, we hit 67. That's more than double. And how is everyone getting hacked? Well, guess what? AI is really good at finding bugs like signature verification, which wasn't even registering in the past years. seeming inability by projects to properly verify the message integrity. They don't know how to check for nonsense. What should be in it? What shouldn't be? What can't be the highest bidder who are not necessarily the the projects themselves?

We don't want to see that here. So, is there hope for redemption to all of this? I think so. All the things that I'm going to share with you, they already exist. They've been tried this year in the past year and they work. We just have to choose to adopt them on AI and defense. If you are a defender and your idea for what you're going to do this year and next year is to just throw AI at what you're already doing, you will lose. You will fall behind the race.

Instead, I want you to step back and realize that as a defender, you are the ones that are setting the terrain for the attackers and AI and their bots or whatever to operate in. So, why can't you design a terrain that is so difficult to operate in, so difficult to navigate that it drains even the most wellfunded attackers? How can you burn their tokens to the ground? And before we even start talking about AI, I want to reintroduce some basics.

How can you lock down what you already have? How can you set hard rules with invariance, setting hard privileges, allow lists? If you can't lock it down, cap it. There is no reason, I've been saying that for years, for your vault to be drained in a single transaction. Set the outflow limits, time locks, multi-s. Last but not least, add a human element, which is the most difficult part for automation to bypass. Cheapen your mistakes. Realize that you will mess up and that's okay. So, what can you do to make your mistakes not existential?

Set your guardian accounts that will save you at the last moment. set automatic circuit breakers. If you're if you're an exchange and one of your chains was already drained, maybe a good idea to automatically shut down everything else or drain it. Last but not least, with a Black October especially, just operate under the assumption that you are already hacked. Your laptop is hacked. Your developer is already hacked. So how can we build a resilient security program that can survive not one or two but more compromises of your machines of your keys and still survive then and only then can we start talking

about AI and I'm not talking about saying Claude hack me do not do not fail that's not going to work build a threat model no one else understand the weak points and the most critical parts of your protocol and your project. Then you and once you identify those sensitive points, then apply AI to it. Run models 247 against it. When a new model gets released, update your harness, run it again. Do that before someone else does it for you.

And speaking of models, a reminder from the hugging face interface. You cannot rely on commercial models for security work. Even the most expensive and permissive models that you can obtain today will still have guardrails. Worse, those guardrails may be applied to you at a moment's notice just at the time when you most need it. In the middle of the incident, you must practice self-reliance. either run your own infrastructure or rent a redundant one. Practice with it, build the harnesses so you know exactly what to do to analyze the locks to reverse engineer contracts.

Have that infrastructure on the ready so when the worst hits, you will be ready for it. And of course, what do we do about North Korea? Well, for that I invite you to look back in history at traditional finance that we so like to make fun of. The thing is exactly 10 years ago they were in the exact same spot we are right now. In 2016, North Korea attempted to steal $1 billion from the Bank of Bangladesh. How many of you are familiar with that incident?

Right. The Jonathan Mevs. Uh, are you here?

Jonathan Mevs, >> that's you. >> Oh, sorry. So welcome back everyone. Can you be seated? So the next speaker is Jonathan Mvs and the talk is about AI FU sloper prop exploration in agentic formal verification.

Oh, can I get a clicker? >> Thank you. All right, let's see. You think this would be easier? How do I click it? >> Okay. Um, well, hello everybody. Uh, thanks to Defi Security Summit for having me here. I'm John. I'm a senior engineer with Quanstamp. And the topic I'll be talking about today is like formal verification and how far can AI

support such uh, and some experiments we did uh, surrounding a couple different tools. Click Okay, great. So, these are the guiding questions that inspired the talk and like what we'll be focusing on today. And we wanted to see like to what extent does AI make existing formal verification tools accessible to experienced smart contract auditors. And to do such, we like ran some experiments on three prominent tools like autoprovert checker by the solidity team. And then ultimately we wanted to conclude where does formal verification fit in the audit cycle and like some takeaways that

we can have as smart contract auditors. Next please. So this was sort of like the starting idea right like over the past year um with like LLM and like agents getting really really good we've seen like non-technical people be able to produce like some legitimate technical output. So this is like your typical business guy like sitting down with Claude and being like, you know, build me a 100 million ARR SAS, make no mistakes, and actually getting a website output. So there's like um this non-technical person doesn't really need to understand anything about websites in order to like actually get a website um out there and

sort of running with it. So next slide, please. So then uh we wanted to take that a step further and see like with us as like pretty technical people, bug hunters, reading a bunch of solidity code, um you know, breaking apart systems, stuff like that, could we make a similar leap to the extremely technical realm of formal verification? So often times people that are like experts in formal verification may be studying mathematics at like uh the PhD level or um having like many years of this like targeted uh study. So if we spent like years uh doing smart contracts, can AI help us get that leap?

Uh similar to like the BD guy to the website, the smart contract auditor to the formally verified expert. So if thread guy can do it, maybe I could do it right now. That's just a meme checkpoint. Okay. So a a slight primer on formal verification. So let's say we have a spec uh like a deposit never decreases total shares. So if you were to write a unit test for such, you would just like do something like deposit 100 and make sure that the assets you got back uh was greater than or equal to 100. If you were to fuzz that spec, you would probably or you would run it through a fuzzer and then it would test a deposit of 100, test a deposit of a thousand,

test a deposit of uh,0001, so on and so forth, thousands of random deposits. But with formal verification, you want to mathematically prove that for every deposit from any state, the shares will never decrease. So now let's take a look at to what extent uh did these tools actually make uh formal verification accessible to experienced smart contract auditors. So this sort of sets the stage for how we went about this experiment. Like just sitting down at the computer, hey Claude, formerly verify this a vault.

Believe in yourself. Make no mistakes, right? So in order to do so, we needed an ideal code base. So this was one that was like simple for the point of like experimentation. So if and when we needed to look under the hood, you could go read the code. it was like uh had a manageable line of code so that the prover didn't run forever which was actually something that I underestimated how long those things take. Um and then we this was really important here is we needed like a public human formal verification report that actually had some real bugs in order for us to catch.

So what we landed on was this a vault that audited both with formal verification and a manual code review in 2023. It's a simple ERC 4626fold where deposits are in yield, the owner can take a fee, and it's just shy of 700 lines of code. And there were 11 known bugs uh to see if the formal verification tools actually caught it. So now, how do we pick the tools? Well, the ideal tool um was tailored specifically to Solidity smart contracts. It was open source so we could use it and download it or um tinker with it. It was already like adopted by the community in some extent um and had already undergone several

client engagements. Um and it was thoroughly documented so that we could basically build agents uh to use the tools without uh having the agent to figure too much out. So we ran each of these tools on their own EC2 instances. So they had tons of resources and didn't need to share anything. Um and they could sort of just run the provers on and on and on. So the first tool that we you uh took a look at was Cura's auto approver which came out this past summer in July. Uh this is the only tool that we looked at that was a gentic out of the box. So Certo has had their prover out for some time but in July they actually released this agentic solution. Um what's unique

about this tool is that it's written in the certo verification language. Uh so that's their own language where you write the specs. They're verified at the by code level and they support uh several different solvers and the technique that they approach to formal verification is verification condition generation where per rule you build one formula and ask the solver oh is any input going to break this rule. So this is an example of like what the agent would actually create. Um this is the tool wr or a spec written in uh certra verification language never decreasing shares. Um so this is what would actually get fed to the solver.

And humans don't usually read this part but it's just good to sort of like get a look at what's actually being fed into the solver. Um which which is this assert statement is trying to be proven holding true for all inputs. Could you go next? Thank you. Uh the next tool uh is really interesting. It's controlled by runtime verification. Uh what's cool about this is it runs on the bite code in the KVM which is a mathematical definition of uh the solidity EVM according to the yellow paper. So uh it verifies bite code. uh

it uses the Z3 solver and what this tool focuses on is symbolic execution which is uh running each test with like these symbolic inputs at each branch in the test. You uh traverse each path and you're either going to get to an error that's going to show that the spec doesn't hold or you're going to get to a terminating condition and see that the spec does indeed hold. Uh I think this might be out again. If you could go next. Thank you. So this is what um you would get from or what the agent created for running the control test. We see that it's extending uh this control test library and actually running um the test within the KVM

directly. Next please. And yeah, this is an example of what was being uh fed to the solver. Um, and you it's not too important, but you could see that like there's actually a different question being asked to the solver versus what uh Ctora asked. Next please. So, this one uh SMT checker, it's actually just built directly into the Solidity compiler. So this tool is actually like most native to solidity and probably like easiest for like a solidity smart contract auditor to jump straight into. Um so this is provided by

the solidity team. It uses a constrained horned clauses model checking which is just asking um a solver for an invariant that holds for like all deployments for every call and then if that holds it rules out the bug. Please go next. And like I mentioned, this is like most native to Solidity because it's in the compiler itself. So there's no extra libraries. There's no um other languages that are used to write the spec. You can just extend a vault uh make a call to the contract or the function that you want to test and add an assert afterward. So uh we know that like usually as solidity devs you aren't too

keen to having asserts like within uh the contracts or the functions themselves. You'll usually tend towards require statements. So you would usually just extend and put in the assert for the condition that you're looking for um and then run it through the compiler and then yes it will create uh an output that you can ask the solver. Next please. So this is just kind of wrapping that all up. I'll invite you to take a look um a diagram like comparing all three of the tools that we looked at. So all of them are open source. All of them generate counter examples and all of them support the Z3 solver which is like the main solver being used here. Um, as

I mentioned, Stores is the only one that's agentic out of the box and the only one that has a um separate language used, the CVL. Both control and SMT checker are written in solidity and they each have their own uh separate technique for verification. Next please. Okay. So, now for the exciting part uh hardness development. Could you go next? Thank you. So the idea when we started to write the harnesses to test the formal verification tools was we assumed like okay sir's auto approver that's like sort of the template right uh that's what an agentic solution to

formal verification would look like right now so we extracted the properties and the architecture from certra autorover and then basically in conjunction with the documentation on a specific tool either control or smt checker we fed them um into claude to actually write the harness and then hold on let me not get uh let me not lose my train of thought here. So like with auto approver we wanted to basically like take what they were doing and see if it could also work with control and SMT checker um and then like compare the results of such.

So that wasn't just enough to write the harness. Each control and SMT checker came with their own like example code and test cases to work with. So control I think they had uh like a simple counter contract and a WT 9 contract uh that we could fine-tune the harness on and SMT checker I think it was like a mutex like a lock uh contract and ERC777 that we got to fine-tune on. So SMT checker was actually fairly straightforward with fine-tuning, but what we found with working with control, if you read the control documentation for like that formal verification tool specifically, a lot of it is focused on

um it's written so that there's a formal verification human expert like frequently in the loop. So a lot of the control documentation talks about writing a test, okay, it fails, go back and like tweak it a little bit, add a lema, so on and so forth. Um, so that actually didn't do too well with the agent, which we'll see in a little bit. But after we basically fine-tuned it to actually solve the example contracts or example tests that were provided within the documentation for the tool itself, it sort of graduated to move on to the data set. [clears throat] Next, please.

Okay, now the exciting part. So, how did each of these tools actually perform when driven by state-of-the-art models? Next please. Uh, so actually one thing on the models before I talk about the metrics. Um, for Stora's auto prover, there's the ability to uh change what models you were running it on, but we so like out of the box, it's running on Opus 5 and Sonet 5. And then once I wanted to go tweak the models a little bit, they have like a high like a high power model and a low power model. So, their high power was Opus 5 out of the box and their low power was like Sonnet

5. When I bumped them up to the newer generation like 5.5 and Sonnet 5.5, uh, for some reason, SA 5.5 like didn't extract the properties the right way that Son of 5 did. So, then I was like, all right, let's not mess with this and just test autorover. So, control and SMT checker are checked on Opus 5.5, but autorover is just coming right off the shelf. So perhaps if I had more time I could tweak and try to figure out what's going on with Son of 5.5, but for the sake of experimentation, we just let it run. Uh just a small note before we look at some of these metrics. So we wanted to test like recall. So of those 11 bugs that were in the original report, like how

many did the tool actually catch? Precision. So like we know with like AI scanning tools, one of the worst things you could have as an auditor is like noisy results that like end up wasting more of your time. So we wanted to see like out of everything that the tool ended on, how many of them actually hit a known uh hit a known bug. Soundness is a really interesting one like can the finding actually happen. So we extended all the provers to actually ask an agent to write PC's in foundry saying oh based on like this a vault deployment is this bug actually feasible within like uh the execution of the contracts and rule recall was like okay out of all the rules that the provers themselves checked how many were

actually also written by a human and then we have some cost and runtime metrics we'll look at. So yeah, I I talked about this a little bit, but it's just basically like a recall of the bugs caught by the tool. How many were actually in the report? Next please. So this is a really interesting slide here. It sort of highlights like uh the medium, low, andformational bugs that actually made it to the report and how each tool did. So auto approver's tool off the shelf actually did pretty well as compared to their human teams that reviewed the A vault. It caught two of the four um medium bugs and um one of theformational bugs and scored the

highest among the other two um tools. Uh SMT checker got one of the mediums actually one of them that auto approver didn't uh and control scored a couple of the info findings which was like good. Uh next please. So, uh, this one was like trying to see how noisy things were, right? Uh, could you go next? So, this shows like all of the findings like after the tools completely ran through this was like auto prover gave us nine findings, control gave us five findings and SFT checker gave us three findings. Two out of the nine of auto

approver actually made it to the final report. Two out of the five for control made it to the final report and only one uh of from SMT checker made it to the final report. Which is really interesting here is actually like you could see an auto approver and an SMT checker like one formal verification break or spec break actually led to two separate bugs in the finding or in the report which I thought was pretty interesting. Um and also speaks to the fact that like the human is still very involved in this because you as the auditor would have to see the formal verification expert and then uh formal verification um output and sort of determine okay like what more can I break with this if this spec doesn't hold what contracts are really going to

go wrong or what problems are really going to go wrong in the contracts uh once they hit production. Um, and then this like the auto prover doesn't have this out of the box and um, like it just sort of came to my uh, mind when I was uh, like developing these tools kind of like just to like lazy, right? Like just to be as lazy as possible and see like give as much to the uh, AI as possible. So after like the formal verification actually found some breaks in the spec, it got fed to another agent and like I'd mentioned earlier, I had the um agent write a P um in foundry to see like oh can this

actually happen from the forked block like from the A's test suite. Um so surprisingly all the tools were actually producing sound bugs. Um, so all of the things well like they have high percentages for like what could actually happen in the code. So these things weren't like very noisy. It was actually very valuable input to like guide the uh smart contract audit itself. Um, we know sometimes that if you're like reading the smart contract and you're going back and forth with claude, you can waste hours being convinced that there's a bug somewhere where it's not. So, this was actually pretty cool to see. Um, you could go to

the next slide. And the caveat here is that like some bugs, well, many bugs are sound in the report, but it is actually like you wouldn't want to bring it to the client because it actually like doesn't mean much to the client. One very simple example here is like abuse of owner privilege. Like when you're working with a client, you're probably going to assume that they want their protocol to do well. and um that you know they're going to be treating owner functions uh with like at least some responsibility. I'll let the OPSET guys talk more about how you can make sure those owner functions are working the way they should, but there wouldn't be any blatant abuse of owner privilege. So that's why some of the bugs were sound

but didn't actually count to being in the report itself. Another thing is like unrealistic deployment conditions. this one vault that was um being reviewed by these tools was an upgrade. Um so you would assume like the proxies in place and some of these things are already in place. Um and some things were sound in the context of what the agent saw but they were actually just handled by the dependencies or elsewhere. Um so if you could go to the previous slide actually thank you. So like yes, many were sound but not all of them made it to the actual report because of some of the things we talk about. All right, two slides forward. Thank you sir.

Okay, so now we wanted to see like out of all the rules that the AI produced, how many of those rules actually matched what the human did versus like all the rules that were in the human report. Okay, hold on. Let me say that one more time. So like the AI produced a bunch of rules like way more rules than the human did. So of those rules that actually matched the human. So if like the formal verification tool produced 100 rules, 10 of those were also produced by the human that divided by all the human rules.

Okay, I hope that makes sense. Next slide. So they actually performed fairly fairly low here. Um I think I have some ideas why. we'll see like once we actually check um some more results later. But on the left side, you could see like all the rules that the human wrote or at least groups of rules that the human wrote um and the rules that the um agents were actually able to come up with. And for time sake, I'm going to go to the next slide. Um yeah, so this is just sort of you can go to the next one. Yeah. Uh this is just a breakdown of runtime, token spent and cost. And I think that this uh slide

is a big takeaway. And it sort of shows why auto approver performed well in uh several different of the tests. Um probably because it's spending like almost a magnitude of 10 more tokens than the harnesses we were able to develop. So that's probably a testament to auto approver being a more mature piece of software. Um, and there's still being work to be done on the harnesses uh themselves. So what was unexpected to me as an auditor was just how long these provers take to run. Like 58 hours um is a long time. And yeah, you've got to hope your CEO is funding

your tokens. Next slide. Okay. So, is this slop or prop? Is like can we actually have AI power and experienced smart contract auditors access to formal verification tools? So, if we look at the numbers, it's tending towards slop. But honestly, as an auditor that worked on it, I am tending towards definitely a value prop here. Um, at the very least as an auditor you have like access to sort of start to learn this new specialized skill like at the very least. Um, go on the next slide. Uh, actually could you go to the slide after this?

Okay, I'll go here and then I'll go back. Um, I think the biggest thing why I think it's prop is that you get valuable results for edge cases that can just sort of further guide your manual review. Um, so we saw that like the soundness scored really high. Um, so you could look at some of those bugs and then like see, oh, okay, like how bad is this really? Um, another really cool thing you could do with this is if you have like the formal verification running sort of maybe alongside like your manual review. Um, maybe you give the report to the client and they come back uh and they fix a small part. You could like run your specs again and make

sure that nothing else broke. Um, I do think that like the results alone do not suggest that like LLMs could drive a proper standalone formal verification engagement right now or at least that that could be driven by a sole smart contract auditor. I think it's still a very very specialized thing that's going to need like practice um and expertise. Could you go to the previous slide actually? Thank you. Uh, so this sort of goes to the shortcomings. It's it's hard to learn. Um the results that we got are actually dependent on the harness. So you could tell me to just prompt better. Okay, that's sort of like the next step. We'll work on it together. Um results are on the whim of the model itself. So you can

see a real screenshot that Claude gave me. Like this is probably the worst thing you could see after like 59 hours of proving and hundreds of dollars spent on tokens. Um, luckily like it was in the conversation history, so the fallout wasn't too bad, but like there's always this risk of like the models going rogue and just sort of like, you know, how much can you really trust them? Uh, we'll go forward uh two slides or Yes. Okay. So, like the next step uh would be like open sourcing some of these harnesses we developed. So once that's like out and shared with the community,

like we can all sort of like take a crack at it and like tweaking the harnesses. Also, the workflows um that we did were ultimately like prompt output prompt um and like a workflow instead of like a truly agentic solution. So eventually I would want to like develop towards that where you sort of had um either like one agent or a swarm of agents sort of like really really looping through all these different stages instead of just like a prompting workflow.

And then of course there's a lot more work that should be done with like testing on multiple models and multiple code bases. Next slide. Okay. Well, thank you all for the time. Um, and I hope you learned something. I'll be around like today and tomorrow uh to talk more and I'm interested to hear your thoughts. Thank you. Thank you. The next speaker is Pablo and the talk is about two FA owned save you dead top and stolen sessions.

>> Thank you. >> Hey, hello everyone. How are you? So today we're going to talk about many things. We have many slides. Uh but we're going to start with 2FA. First question, how many of you saw my presentation at dark mode in February about this or similar to this? Not so many. Great. So let's start with this. H very briefly about me. If you don't know me, I'm the founder of OBSC. I'm a member of security alliance. I'm a signer in Arbitum, Optimism, Polon and

ENS Security Councils. We froze a lot of money from Kingdom two days ago. And uh I'm also the host for the blockchain security series podcast that will come back in a few months. So let's start talking a bit about 2FA and then we'll see why this is super super important in our industry today. We like when we start talking about 2FA the most basic thing is mobile phone numbers right. So um what happens if we use mobile phone uh for 2FA basically we know sim attacks right someone is able to go to the telephone company impersonate us and get our uh phone number and access all of

our codes hacking our accounts. Second method to hack our phones. I don't know if you know it, the voicemail attack. All telephone companies around the world have an special phone number where you can call to listen to your voicemail and the pin to to listen to your voicemails. You know what it is? The last four digits of your phone number, right? So basically anyone here can listen to anyone's voicemail. So instead of choosing, hey, I want to receive the code via SMS, you receive it through a call. is recorded into a voicemail because they do it at 4:00 a.m. while while you're sleeping and your Telegram account is gone, WhatsApp account is gone, Google banks, etc.

Third way to intercept SMS codes every time a company sends you an SMS for example uh Apple, they do it through a company called Twilio. Most of them, this company uses lots of intermediaries, right? Tier one, tier two and tier three companies. These companies have a zero opsec and usually their servers are with five or six different thread actors groups that are seeing all the SMS going in plain text. Right? So what we see with this is that basically FA with phones is a joke.

Right? So what do we learn from this? Very easy. Never use your phone number anywhere for 2FA. You remove your phone number from any platform where you can. And for the few places where you have to use it, Apple ID, Signal, Telegram, and some banks, you have to use a private phone number that nobody knows that belongs to you or from companies like a funny that make it uh very very difficult to SIM swap, right? What's the best way in my opinion? Just ask a friend to get a phone number under their name. Use it and don't share it with anyone. Know that your phone number will be taken over. It's super easy and cheap to do it.

So, uh, TFA with SMS is So, the next step is TOTP, right? Timebased onetime password. We know all these apps. Oi, Google authenticator, Microsoft authenticator. What's the issue with these apps? Starting with the Google authenticator. First of all, they offer backups in the cloud, right? Those backups are not encrypted. So when they hack your Gmail account what which will happen they will have access to your codes right but that not that's not the only issue that you have to check the also the other issue that uh we have is the Google ecosystem right we use Gmail for our emails we use Chrome for our passwords that's also

synchronized with our Google account we use Google authenticator for our 2FA also synchronized with our Google account if you have Android you have your pass key synchronized with your Google account. So what happens? You have your passwords, you have your 2FAS, you have uh you have your emails and your pass keys synchronized with your Google account. Your Google account gets compromised. You lose absolutely everything and you are not going to get your Google account back. Another very very bad idea is and this is done by approximately 30% of people in crypto storing 2FA codes right inside password managers. So you have one password Apple passwords etc. and you

have your passwords and the 2FA together. It's not the 2FA anymore. What's the issue? The the other more important issue with tootp codes and I will show it easier here. Let's say that that you receive this Twitter fishing. You click on the link. It asks for the password. You put the password. It says it's wrong. You put it again. You are logged in and it asks for the 2FA. Right? So after it asks for the 2FA, you enter the 2FA. The codes that are generated by these apps, Google authenticator oath Microsoft authenticator, etc. are not fishing resistant. And we have to know all of you have to know that eventually you are going to click on a fishing link and you

are going to enter your credentials. Right? So these codes are not fishing resistant. We cannot uh consider to keep using them anymore. So what's the thing to do regarding this hardware authentication? Right? You all know about this. I am all the time talking about these little products in X UIS. They can be used in computers, in phones. You have to know that at least you should have two. And if you are here, you should have three, right? One, this one very small always connected to your laptop. This other one always in your keychain and the third one backed up at home, right? As they cannot be backed up, you should cons uh con uh

configure all of them in every platform where you sign up, right? But these devices could be lost, right? So what we do and you'll have the slides here because I will publish them is that we will configure them so that the pin is always mandatory, right? So if one day I lose my UB key, it cannot be used by anyone because it it requires a pin like this, right? So you touch it, you push a pin, you touch it again, you are logged in. How do you do to have the pin as mandatory? You open the terminal. You run eekman. Here you have the the exact comments that you have to do. This is a

very bad user experience from uco but we cannot expect too much from them aside from making good hardware. Um and this way the pin will always be required to you. Okay. So what's the other very good thing about these devices is that the login is much faster than with Google authenticator for example right you have to unlock the phone open the app put your fingerprint look for the code copy the code enter the code it's lots of steps with these ones you touch it you put the pin you touch it again you're logged in now something important about UB keys UB keys have many interfaces right you have

the OTP P that is that long code that you'll see uh when you touch it and those codes are fishable. You have a 502 that is basically to have like a pass key inside the U key which is not fishable. You have 5.2 which is not fishable. And you have oath or tootp that is basically to generate these codes inside UKs but are also fishable. Right? So when you configure them with UV key manager, you can just disable the um the ones that are not safe and just keep fight U2F and 502.

So OTP codes, maybe it happened to you that you touch the U key by mistake and you see all that string. Well, those are the uh famous OTP codes. The problem with them is that these ones are not only very easy to fish, but the same code if you if you have a registered your UB key with this in three different websites, one website can steal it and it can be replayed in another website, right? They are super super unsafe. So, we do not recommend this at all. Um, so then you have OATH or OTP codes, right?

This is can you can you like put it so that it's Yeah. Okay. Thank you. With uh with this codes what you do is to basically configure the traditional Google authenticator or auth. But let's go to the more interesting ones. PhD U2F, right?

So PhD U2F is the first one from Ubico that uh is fishing resistant, right? Because it checks who is requesting this code. So the day that you get into a fishing website and you enter your credentials and the 2FA is required, this will not this will not work. So you you will be protected, right? What's the issue with this? that no pin is needed by default, right? So, we have codes that are fishing resistant, but no pin needed. So, if your UB is stolen, it's useless.

But as we were seeing, it's always checking that the website that is requesting the code is the real website. If it's not a real website, it will not send the code. So, then we had pass keys, right? A good idea, but implemented like like always. So pass keys are 10x better than passwords, right? They cannot be fished. They should not be able to be shared. They cannot be repeated. They should not be stolen from the user's device. And definitely they cannot be stolen from the service where you signed up. Right? Because if you signed up to Coinbase and you put the password in Coinbase, then Coinbase gets hacked. Your password is in the dark

world, right? It it doesn't happen with this. So how does it work? In every service where you sign up, there's a private key and public key generated in the secure enclave of your device. The public key is stored by the website or the platform and the private key in your secure in your secure enclave. Every time you want to login, you do a biometric. This is this an enencrypts the private key from your secure enclave. It signs a message and the platform identifies you. Right? So then again pasis were designed to be stored where in secure enclaves right but the industry had a great idea of synchronizing them right with your

iCloud your Google account or your password manager right so this is now in the cloud and hacking an iCloud account a Google account or a password manager depending on your obssec it could be pretty easy so it's not a way anymore As we can see here, Apple wants to save your pass keys. One password also likes saving your pass keys. And after all, why shouldn't we keep it, right? So, what's the other issue with this type of ask keys? Many platforms like X and Google treat pass as both the first and second factor, right? And this is

super super dangerous. So if you check in your Google account you will if you check in your Google account you will see that you have an option called skip password when possible. You should always disable that because if not that means that someone gets access to your iCloud account they have your pass key and with that they access your account with nothing nothing else. So uh there we go. As we said, pass keys, the ones that are um that can be synchronized can be stolen from the can be stolen from the cloud but cannot be

fished. Right? If we use ph2f, they cannot be stol uh stolen from the cloud. They cannot be fished but they do not enforce a pin. Right? which Pascis do and the UV codeb cannot be solved from the cloud but they can be fished so there's no good solution right this doesn't seem to be working so what is the solution 502 plus U keys go one more so what is this it's basically basically saving your pass keys inside the UB key,

right? In this way, you have fishing resistance and the codes are not stored in the cloud, right? And then you have a PIN that that protects the UB key from any physical attack and it's required every time you want to use it, right? Every time you touch it. Um so with 502 with a PM forest, right, you combine three factors. something that you know your password something that you have the UV key and something that you know from the physical device that is a pin so even if someone steals it it cannot be used let's continue if you something that is also very important because the problem with UV

keys is that how they are implemented by different platforms is a disaster is that if you go for example to your Google account and you say okay I'm going to configure this you would say you have two options. Create a pass key or use a security key. Right? What would you do? Use a security key, right? Because you have a security key. No, you have to choose create a pass key and then the option use another device. Continue. Then click on USB security key. You put your PIN. You save it. And that's it. So continue. One more please. This is how Ubikis look at Google authenticator users just pathetic.

Continue with more. So the conclusions for this part right mobile phone number we always we obviously see that is a nogo route. Right. Cloudbased OTP they can be stolen from the cloud. So and they are not fishing resistant so useless. UGOTP codes cannot be sold from the cloud but are not fishing resistant. Useless. OTP cannot be stolen from the cloud but are not vision resistant. Also no. Ph2f fishing resistant but does not require a pin. Synchronous passets can be stored from the stolen from the cloud. So also useless and 52 uh 50.2 in our devices is basically the only way to do tofa safe

in my opinion. One very important thing whenever you do this is that you should always save the backup codes for your accounts in paper right or in an encrypted drive never in a password manager. So with this we were go back please we were able to protect our accounts right the login. So now the accounts are safe right please continue. No way. They are not safe. What do you think that these hacks have in common? Binance bybit and running and many many many more. What's a common thing here? It's pretty easy, right?

Continue. It's a BRK. It's a PRK. Continue. But not only the BRK, right? That's not not the only thing in common. Continue with one more. N nearly nine out of 10 attacks in crypto start with a very stupid thing that is a developer laptop infected right they start with this then someone that that is far better than the guy that did the social engineering for this starts moving laterally gaining more privilege etc that is more advanced but it always starts with the same thing so now we're going to see what happens when you protect the login right so we protected the login with UB keys passwords pin UB be keys and blah blah blah blah blah. But the real threat is

here stolen cookies. Continue please. So a cookie is basically like a door key, right? Not an ID card. Whenever you log into a website, that website gives you gives your browser a cookie. And every time you want to login or you want to request something, it sends that cookie and the website says, "Okay, it's you." Continue. So what happens? What always happens? Some developer, some founder, whatever downloads some malware. And this will happen to all of us. All of us. All of us here, everyone in this room in the next three years. We are going to get

malware in our devices. It's inevitable that malware will steal the cookie and after the cookie is stolen, the cookie will be imported into the device from the attacker and the attacker will will basically replay it and now they will just open your session. Right? Continue. So we basically have did password MFA device check risk engine and we have the cookie and the guy the attacker starts here, right? They start at the finish line. They have this all of that doesn't matter. Continue with one more.

And this is an industry that is growing a lot. These numbers are from are from last year and I bet that this year it would it will be like at least 3x uh this. Last year there were 50 um 52 million stealer lock packages. And a stealer is basically a type of malware that gets into your device and steals passwords, private keys, seed phrases, cookie sessions, files, whatever. 25 million devices infected and 98% of those packages came with usernames, passwords, and cookies included. Right?

So this is super super dangerous. In the last decade, there were many attempts to fix this thing of what do we do with these cookies and we have HTTP only, abound encryption, token binding, risk heristics. None of this worked. So what do we do to make those stolen cookies useless, right? Because remember this will happen to all of us including myself. Continue. There's basically a new technology developed by Google and Microsoft, right, called DBSC. And to explain it simple, what we do here is you log into a website, the website gives you a cookie. And now in the secure enclave of

your device, there will be generated a private and public key, right? The public key will be sent to the website and the private key will stay stay in the secure enclave, right? So now these cookies that the website will send you are short-lived cookies for 1 minute, 5 minutes, 10 minutes. And when you want to renew the cookie, right, the website will require the secure enclave to sign again. This means that if the cookie is stolen, the attacker will open it and if it if it went by more than 1 minute, 5 [clears throat] minutes or 10 minutes, whatever, they will have to sign again.

And if they do not have access to the physical device, they will not be able to do it. Continue. Continue with one more because I already explained this. So what does this stop? Right. DBSC the replay of the stolen cookie. Right. So if my device is infected and the cookies is stolen and then is sold like the market for stolen cookies is huge huge that will be stopped right because they steal it from me they sell it and when they get it this cookie requires the signature it doesn't work useless. What it does not protect you from is if your

device is still infected, right? Because you have the attacker inside the device and they will be able to keep sign in, right? Or to have access to the new cookie that is being sent to you. And it obviously does not protect you from other stuff that can be stolen from your device, right? Private keys, seed phrases, API keys, etc. So, where are we today with DBSC? In Chrome, in Chrome for Windows, it's public since April since Chrome um 146. In Mac OS, it landed on August 2026 and now it's on by default in all Google accounts and Google Workspaces account, right? Octa is uh already doing trials.

Firefox declined to use it. I don't know why, but let's stop using firefox. Safari is still evaluating. Safari is a disaster as a browser for objects. So I highly recommend you to not use Safari ever. And now the web 3C uh is creating an standard for this. Right? Create go one more. But what's the thing here? Right? Because remember that in security we always know we are never 100% safe. It's always about adding layers and layers and layers for what? To make it more difficult and more expensive to the attacker, right? So, what's the other layer that we have to add here? EDRs.

And this is a huge problem in our industry. We have an industry where privacy is very important, right? And I agree privacy is important. But I see a huge amount of teams that oh no, no, no, we don't use CDRs. EDRs is a problem for privacy because uh they will be seeing what I do in my computer and blah blah blah blah blah my privacy my privacy my privacy and then they have their computers infected. Kim Jong-un has access to to to absolutely everything and their privacy where is it. So who knows what does it what is an raise your hand.

Ah we have an issue. So an antivirus is the classical tool that searches for files that are known viruses, right? So we know that this file is a virus because of the signature. That's it. Very very easy to bypass today. An EDR which stands for endpoint detection and response is for example crowd strike or sentinel one. But the number one is crow strike by far watches behaviors right it says okay there's a new process here that is trying to read the memory from this other process and connect to this weird IP so it will detect most of this stuff and stop it if in this industry we used edrs at least 95% of the attacks that we

saw in the last three years would not have existed right it's super super stupid not to do So what's a recommendation for small web three teams? Every laptop. Every laptop unless it's a super specific laptop only for signing. If you're in very big multi6 or security councils and you don't have anything but signing every laptop should uh should have uh an edr as I said the recommended the recommended brand is crowd strike and crowd strike is super super cheap and you can buy from one license for you right $150 per year per user nothing

it should be managed not do it yourself that means that there should be someone watching the alerts, right? And then obviously the ADR is not the only thing that you should have. You should have a good hygiene, right? Good object in your device, MAC was properly configured, separate signing device, uh no obviously please no set phrases and private keys. It seems to be very basic but 25% of people that we audit at OBSC 25% stores it phrases were in password managers and I bet that that 20% of you still do it.

If you have to do one thing this month start using an EDR to install it. It takes you literally 30 seconds. You just open the sensor you give it permissions to access your full disk and network and that's it. It's installed. Go one more please. And then so we said we have unique passwords. We have UV keys properly configured. Um we have DBSC, right, to be able to kill the cookie if it's a stolen. And we have an EDR to protect your device, right? In case it's infected. Because again, if it infects you, if you're infected once and

it's stolen is one thing. If you keep on being infected, if you have persistence, that's a great issue. In fact, many people the other day I was talking to a friend and uh the guy that hacked me for the first time when I was 15 years old. He's a great friend of me now. Uh and he told me many people think that they realize that like how many time goes by between you get hacked and you realize about that right and many people would think would think okay I get hacked and five minutes later I get my metam mask drained right but if you didn't have money in your metam masks six months eight months nine

months can go by and you have no idea about this right so this Also another thing that is very important, right? Every time an stealer steals data from your device, that will be first used by that threat actor specific to target you and to steal whatever they need and then this will be sold in the dark web, right? So you should be able to monitor, you should pay for a service that is monitoring threat actors groups and the moment that you see the domain from your company, the name of an employee, a phone number, an email or whatever that belongs to someone to someone from your team, you don't go and rotate passwords.

No, you block completely that person because you know that that that person was infected. The thing that you have with this that is tricky is that if you really want to be the first one in knowing when someone from your team was infected, who should you buy that data from? The threat actors themselves, right? So it's kind of tricky, but it's the way it is. So let's go one more. Four layers as we said 50.2 two plusic is to secure the login right and this bits fishing DBSC secures the session right and the cookie replay the day that

it's stolen remember that this is what happened to bbit right the developer from safe was infected they stole the session from Amazon web services the session cookie and then all that happened then uh layer number Three, the EDR to secure your device to catch whatever happens and after something happens, you will have evidence to really understand what happened. And fourth, monitoring, right? So at as soon as something as someone from your organization was infected, you will be the first one to know about it. One more.

So five things to remember. First, this cookie theft uh is the way to bypass MFA, right? And it works at a scale. This is super super fast the way it works. It's not manual. Like when they steal a cookie from you, a checker will go and try to to replay it automatically. When it works, it will pass it on to a to a manual operator. Fa verifies your login, but it never sees the session, right? It will not protect it. DBSC does not hide the cookies, right? It will only stop the cookie, the short-lived cookie from being renewed.

Then the EDR covers what the DBSC cannot, right? So remember, put it in every device. Again, this if if companies in crypto had to do one thing in this industry that we have that is basically a joke would be to insert an EDR. That's it. Only thing that you do today in an EDR and then and then one thing connected to this many people tell me no Pablo no I will not fall for a fishing. I bet that for sure nine out of 10 people here are convinced that will not fall for a fishing. And I tell you, you will fall for fishing for sure. I don't know if you saw the last emails from Google that come from Google, signed by Google, ma

bailed by Google, everything is from Google and they have malicious code injected. And the other thing is many people say no, I will not get my device infected. I do not download so many stuff. Well, go and check how many processes you have run you have running and how many dependenc dependencies those processes have. For sure, we are all going to be infected. It's just a matter of time in the next year or two years for sure. And then number five, mon monitor your domain so you're the first one to know when someone was infected and go very fast and block every access that this person has.

Is there anything else? I think that no. Thank you. Thank you. >> [music]

[music] [music] >> Hey, [music] hey hey. [music] Hey.

[music] Hey. Hey. Heat. [music] Heat. >> [music] [music]

>> Hey hey [music] everybody. Hey hey hey. [music] [music] [music] >> [music]

[music] >> Hey, hey hey. >> [music] >> Heat. Heat.

[music] Heat. Heat. >> [music] [music]

>> Hey, hey, hey. Heat. Heat. >> [music]

[music] [music] >> I'm a good [music] [music] >> [music] >> You are the one I know you

need. [singing] You touch me so, [music] but you're the one. You know that I'm [music] the one to see your eyes. I'm the one. I gave you all. [music] I gave you home. You gave it all.

I gave you I gave you things you [music] changed and [music]

[music] >> [music] [music] >> Heat. Hey, Heat. >> [music] >> Heat. [music]

Heat. Let's try again. Hey.

Hey. uh for emphasis but um today I will be

So, welcome back everyone. Can we be be seated? Unfortunately, the next speaker could not make it. So, here is a video from DSS 2025. So, next up we have uh Sam CZ Sun uh who's going to be piping in. >> Well, hey. So, I'm Sam. Unfortunately, I couldn't make it in person, which means that uh I can't, you know, emphatically bang my head on the desk uh for emphasis, but um today I will be here to talk to you about a question that is uh you know, by the numbers plaguing your

industry, and that is how exactly do you even write secure code anyways? Uh and so you know obviously if we look at the [laughter] if we look at the numbers it seems like this problem is kind of hard but um you know usually when we're faced with a hard problem it's worth checking if anyone else has solved this. Uh after all there's no point reinventing the wheel. And for that I'd like to take a quick stint to talk to you about the Curiosity rover. This uh little project was proposed in 2004 launched in 2011. And over that time uh NASA spent a total of about 3.2 two billion or you know maybe like two or three D5 hacks uh on this project and with a team of about 30 people they wrote over 2.5 million lines of code in

C no less and you know with a project this big NASA would obviously want to make sure that their investment wasn't going to be wasted and so you know they they did this by enforcing what's known as the JPL institutional coding standard for the C programming language now obviously this is a coding standard C and so some things are going to you see specific, but as it turns out, there's actually a lot of things that can uh translate into solidity. Um, for example, here's a few that I have picked out of this uh these coding standards.

For example, uh all code must be statically analyzed. There must be no resulting warnings or errors even if you have false positives because the logic being if your code is complex enough to introduce a false positive, then clearly something needs to change. Um you're not allowed to have any loops with dynamic bounding. You're not allowed to use recursion. Any declarations you make should be scoped as tightly as possible. Any return value should be used or explicitly discarded. You should always validate every parameter at the start of every function. You should always use assertions. And instead, the standard mandates that uh if your function has more than 10 lines of code, it needs to have at least one assertion. If you have an expression that has more than one operation in it, you should use parenthesis to make the order of operations explicit. And the last one's

a real doozy. Uh it says that unless you have unless it's in special circumstances, your function should not be longer than 60 lines. And so you can imagine that if you followed this guideline uh your blockchain protocol will be extremely secure. The downside is that you know as you're following this guideline all of your developers uh will sort of look like this. And so you know I think the real question that we should be asking is how do you write secure code anyways? but you know for the regular person right and so that's what I'm here to talk to you about is I prepared uh five different ways that I think uh or five different tips that I think would help uh you know throughout the entire developer process to sort of make sure that your code output is uh less susceptible to bugs and you know

hot take the first one actually you know maybe coding standards are good and so I think to get a sense of just truly appreciate uh how coding standards can really elevate a codebase. I think it helps to take a look at uh one that does not. And so here's a snippet of code that I've taken from a D5 protocol called BZX. Um you know, this function at first glance might seem, you know, short and sweet. It's really nice, but then you see that oh well, we get this nice uh address array called sent addresses, and you just kind of have to memorize that uh you know, send addresses sent addresses at three is receiver, and you get like five more unit values, and you just have to memorize that sent values at two is torque interest. And then uh once you do some you know high level validation you

get you jump straight into borrower trade. And in fact I haven't bothered including the rest of the snippets but if you were trying to review that code uh and you wanted to review the interest calculations you would actually jump from borrower trade from pool into borrower trade into initialized interest into settle fee reward for interest expense into pay fee reward into yet another static column into another contract. In other words luck with that. And so the question here is well how exactly do we write code that does spark joy and you know there's some simple guidelines here uh from things like using descriptive variable names uh because you know this is 2022 and we aren't limited by we aren't limited by eight characters per variable name. We can limit that number of active

variables so that code reviewers and auditors don't have to keep as many things in context at once. We can try to eliminate redundant logic and we'll get we'll get more to that later. Uh early exiting as much as possible. uh we should put related code close to each other so that we don't have to travel with too far um within the code to maintain context. And of course, we're all using git, right? We can go ahead and delete all that unused code. To give you a sense of what that looks like, here's a snippet of code from a protocol that uh I think has much cleaner code, maybe one of the uh cleanest uh code bases I've ever seen so far, and that is of course Compound V2.

Um we can see here that you know we have this really nice almost linear uh progression of logic right as soon as we encounter a failure condition we immediately break out meaning that when someone's reviewing this code they can immediately see that you know by the time you get to say the line with uh that borrow index there's really only one way to get there that and that's to meet the two conditions uh required above. uh the only in fact the only bit of branching logic we had is when we sort of calculate the repay amount um if the user specifies to repay negative one uh you know we see that every variable name you know is very descriptive we have repay amount math errors amount account borrows etc it's really I think you know any auditor would be happy to

read this code um barring of course for their their usual fee on the other hand you know you might come across something like this where we had this variable called essay which you know it's not immediately clear what that means. It's you know it's actually some scaled down. We have this boolean check which gets set in both cases making it you know a bit redundant. We have some code left over that has been commented out. It's not really clear. Uh okay. Um yeah I mean here we're we're a bit short on time so let me just I'll just move on from there. Basically the idea is like you know if you if you have good coding centers it sort of makes sure that the code writing is uh easily digestible for other people both reviewers and auditors uh as we're

reviewing the code. Okay so let's try to get through the rest of this in the next 9 minutes. Uh obviously testing is a huge deal but um you know testing is only effective if you're doing it correctly. Uh one example of not doing correctly is if you write tests uh that solely [clears throat] try to achieve 100% coverage. And the reason for this is because coverage is not the end goal, right? If you're if you're writing tests purely to hit that hit that magical 100% coverage, you're you're doing it wrong. Um coverage should help you help guide you in finding the things that you want to test. Uh some good ways to actually, you know, keep 100% coverage. And the reason for

this is because coverage is not the end goal, right? If you're if you're writing tests purely to hit that hit that magical 100% coverage, you're you're doing it wrong. Um coverage should help you should help guide you in finding the things that you want to test. uh some good ways to actually you know some a good way to actually think about how to write tests is you know obviously you want to write positive unit tests right these are unit tests that test that the function is actually doing what it's supposed to be doing. Um you know if you're writing a script function you should probably write some unit test and make sure that it you know when you pass in four it returns two when you pass in uh 9 returns three 25 returns five right uh but you should also write negative you be clear to them how exactly you

think about testing right what is square root of six of your function actually return does your function handle floating point numbers or does it return only integers round up or down um what if you pass in zero what does that return when you pass in negative one do you handle negative numbers right and so writing tests for things that you exactly fail and asserting that it actually does fail means that you're not only testing uh happy case you're also making sure that if something bad happens uh the blast radius is limited now I think you know what integration tests are because you know your your default protocol isn't just going to be this one function it's going to be something that's built on that builds on top of it like for example some sort of pricing algorithm and so an integration test to make sure that the entire

pricing algorithm works or the entire buy or sell uh function ality works means that you don't just make sure that individual building blocks are secure but you make sure your entire protocol works. Uh but the fourth tech test that I'm sort of I sort of came up with a name uh of this weekend. Um I I'm I'm calling these active tests. And what I mean by this is when you're writing code, there's a there's a few things that you know you might assume is true, right? Like if you're doing testing on local network, you might sort of assume that uh you know the indop pool has sufficient liquidity, right? you're like, I'm going to settle that out cuz that that's not that's at my control. Or you might assume that your chain link

oracle is always returning a price. You might assume that your proxies are initialized. Uh but once you're on mainet, these things might not necessarily be true. And you know, it is 2022 and we all have the technology to make mainet forks and run tests on forks. So why don't we get in the habit of writing tests that assert that the conditions on mainet match what we expect, right? And then if these conditions ever don't match, if one day we find that our implementation is not initialized because we called implementation on our proxy contract, we tried calling initialize and it worked.

Well then, hey, that means that our active test failed and we should probably go do something about it. Now, I think the last two are fairly selfexplanatory, but I think once again, unit tests are where people tend to split uh tend to slip up because it's not immediately clear to them how exactly you think about testing. And so for that, I'd first refer you to this wonderful tweet by Bill Sen, which describes how a QA engineer might order a beer. Uh, and I think we can take inspiration from this by contemplating how a QA engineer might test the factorial function. Uh, if you're watching at home, go ahead and pause the video if this is being recorded. If you're not watching from home like right now, um, unfortunately, you have no time to think about this because I'm going to

jump straight into the answers. How did you do? Well, you know, again, we should obviously test the positive cases. Factorial of 2 of 1, zero. Uh, what about -1? What exactly is factorial of negative 1? What about factorial of 1.5? Uh, if you give it factorial of 2 to the 32, what do you get back? Do you get back a really large number? Is it truncated? You get back maybe infinity. Speaking of infinity, what if you try to take the factorial of infinity or not a number? What about the factorial of lizard? Right? These are some things that you should be thinking about when you consider how to write this unit test for the simple factorial function.

Uh but of course we're not limited to things as simple as a basic math function. Here's a quick excerpt from some code that allows you to buy a ticket. It assigns you a ticket ID, returns you ticket ID, and then there's this function that presumably uh lets you claim a prize if one of your tickets is winning. Once again, if you're watching from home, go ahead and pause this. Otherwise, we're going to jump right in. Now the variable was called tickets. So obviously we would pass in an array of tickets, right? If we pass an array containing one element our ticket, that's probably the way the value >> [music]

[music] [music] [music] [music]

[music] [music] [music] [music] >> Heat. Heat.

[music] [music] Heat [music] up [music]

>> [music] [music] >> Heat. Heat. N. [music] Heat. Hey. Hey. Hey. [music] [music] [music]

Heat. Heat. [music] [music] [music] [music] >> [music] >> Heat. Heat.

[music] Heat. [music] Heat. N. [music] >> [music] [music] [music]

[music] >> Hey, hey hey hey hey hey hey hey hey. Heat. Heat. N. >> [music] >> Are you [music] Heat. Heat.

Heat. Heat. [music] [music] >> [music] [music] >> Heat.

Hey Heat. [music] >> [music] >> Heat. Heat. Heat. Heat. N. >> [music] [music]

[music] >> Heat. Hey, Heat. [music] >> [music] [music] [music] [music]

[music] [music] [music] >> Heat. Heat. [music] [music] [music] >> [music]

>> Heat. Heat. [music] [music] Heat. Heat. [music] [music] [music]

>> [music] [music] [music] >> Hey, hey, hey. [music] [music] Heat. Heat.

[music] [music] [music] >> [music] >> Heat. Heat.

[music] >> [music] [music] [music] [music] >> Yes. So, welcome back folks. You can be seated.

This so the next speaker is Yuri and the topic is audits don't end at publication. words that says don't trust verify but somehow uh in one of the major things uh meaning audits it doesn't work like this let's see how it works so uh about me I'm Yuri head of defy engineering in Lido and basically basically everything that's related not to staking but to defy part of lido goes through me and as a part of this process uh

uh last six months I was uh deep into uh investigating how other protocols works. So let's see uh what I found. Oops. First let's uh understand how the what are what what do we mean when we speak about audits. It's just a paper. Is it a PDF with some findings? It's in fact uh externally verified uh scope of contracts of lines of code that we uh that were reviewed and uh presumably doesn't contain any bugs and uh uh things in them. But uh how do they transpile on the real contracts that are deployed to the uh mainet? There are some steps that we have like uh we

should have like commit and uh byte code and uh verification of the ezer scan but uh do you see do you see the gap here at the moment like among those stuff? I'll give you the hint the code that was audit not always the same code that was deployed. So when you have uh when you enter the site for some protocol and you see the security page with some audits with reputable firms like Serto and other guys uh it it doesn't mean that exactly this code was deployed on the onchain and in most cases like in 60 plus% it's not like that you cannot verify that the code that was

audited was actually deployed. The reasons for this uh are very simple. In fact, it's mostly sloppiness as I think because most of the protocol just hide the the the repo. They hide the commits. They they don't uh uh they don't have the final commit and the audits. This is uh the call to auditors. Please add a final commit. Why why don't you do this? And uh and the most scary part sometimes actual code that is deployed is different from those that was audited. So the idea is simple. How will we fix this? And uh this is uh like a call to the guys from the protocols from the

auditors and from the integrators. So if you are uh the protocol, please do a public uh uh repository for your code that matches the commits that actually uh was audited. Uh update your docs, update audits, update uh like do do it maximally transparently for the researchers. If you see that protocol doesn't understand how it works, please help them uh just uh push them to to to make to make uh the audits transparable.

So the this chain that I was previously on the previous slide was uh can be recreated. So we can trace the all the steps from it. And for integrators like before the kelp incident I think it was like trust me bro mostly like okay you have audits nice uh we go and put fund into you but uh after this incident uh what we do in Lido we verify and it's difficult to verify something that cannot be verified because of these problems. So for integrators please push also the protocols you are integrating with to be verifiable uh and it's not very difficult to do

actually uh as I as I told you just public uh repos uh just using some tools that uh other guys like lido aragon consensus diligence provide like uh bite code verification tools or uh source uh contract verification tools all combined And that's it like 5 minutes maybe 10 with your uh AI agent and it's it will done it will be put on uh I don't know in GitHub repo or somewhere and can be then reproduced by others. So uh my take my like main purpose of my speech was to shift your vision from the audits it's something that is like just

published uh on some security page to be uh verifiable chain of uh of artifacts that you can be that can be verified by other guys from other protocols other security researchers and uh yeah basically uh don't stop at the report make sure that uh it is verifiable it can be proven like uh onchain by other people and basically that's it I think from my side uh I have advertise a slide here for uh guys from LA uh Eugene will be after me and I think in in five minutes and Sergey later they will give you a sneak peek how uh AI based audits work.

So please welcome and thank you up. Hello. Hello everyone and welcome to my small talk on the dangerous hidden in the fog uh and degree integrations. Now what do I mean by this? If this light moves [laughter] one okay

ah okay so what I mean by this uh when we do our work as security auditors we always get a bounded scope a piece of code that we have to verify if it is working correctly. This can be a completely new protocol or an update on an existing protocol, but it's always small and locally bounded. So, we make sure that the code does what it is supposed to, that there are no unintended consequences, and that every integration is working correctly because nearly all protocols in DeFi are integrated with external integrations.

However, due to our limitation, uh, however, every integration has its own integrations. You can integrate with a, but a can be dependent on on specific oracles or you can integrate with uh, chain link or with an AMM pool which depends on the lending market and we don't really check these extra integrations because we don't have the time. But even if we go beyond this, beyond this, where do I point to get this work?

That's too much one down. Yes, we go technology. So but even if we go beyond like this internet connected mesh of protocols underneath we also have a sea of liquidity all the assets and asset pairs and the different protocols which also affect the workings of protocols somewhere else. So even if there is no direct or indirect uh contact in the code, if liquidity in one's asset pool in one protocol gets affected somewhere else, this can change a state which can become a a problem for another protocol.

And when you look at the big picture, what we actually do as security researchers is we verify manually or through co through testing a very small local piece of code and the direct integrations. But DeFi is one gigantic connected graph and we implicitly trust that everything else is supposed to work or we say well I hope it works because I don't have the time or the ability to check this. But this is a problem even those more so today than before because flaws which are multiple integrations away can affect the code that you're verifying and you can say well in my opinion this code is safe I haven't

found any flaws but those are based on dependencies and assumptions which you can't really check and dependencies multiple hops away can affect you and destroy the the code that you're verifying and we see this more and more this year we've had like kelp and resolve last year's stream and a few years ago uler very complex hacks where the root cause was multiple hops away which makes it very difficult to verify now why don't we do this why don't I simply audit everything well one naturally because I don't have the time the work that I have to do is based on the amount of lines that I have to uh verify with some adoption for the

integrations or complexity, but I simply don't have time. And secondly, well, if it integrates with a or for example lido, I'm not really going to check Lido or A itself. I'm simply going to assume that it works because it's a known and trusted protocol. If it's new, I might spend some time, but it's also limited. And testing by itself doesn't really solve this because this also is dependent on assumptions. form of verification also at some point you have a specification which says look the these inputs can be code this minimum and this maximum and not beyond so that doesn't solve really the problem it's a difficult problem and like every presentation today we always have AI

because I think a reason why hacks like these are becoming more prevalent is that before it was really difficult to find it because if one protocol has five integrations which has five and five and five we have so many paths you can't really explore them manually but you can build a harness which checks every single path one out of 10,000 and finds the one isolated path where there is that vulnerability or that dependency which a manual auditor can't really find but as white hats we can also build harnesses so I think um and some companies already doing this we also have to enable this and utilize this to not only check the code locally uh or with the if integrations

But somehow map all the possible integrations and make sure that to the second degree, third degree, fourth degree we can't find an exploitable path or we can at least map the dependencies and the assumptions that we have to have to make. So three quick takeaways for all the security researchers. So when or developers, so when you're verifying something, it's important to take into account that your code is not just an isolated thing. It is a small node in a vast network and you can't really see far beyond a flaw many degree degrees away can still destroy you. And lastly, AI can help us in the sense that it is lifting

the fog. The black hats are doing it. So must we. Thank you. >> Okay. Hey everyone. Okay, here's my presentation. So, uh I'm going to talk about Evergreen concept uh we built together with the mind as uh the thing that probably every protocol should have in the industry at

the moment. Uh I'm Eugen. I'm look for engineering at lighter labs. Uh you can follow me on Twitter. Uh nice to meet you all. U sorry I yeah technology. So agenda is simple. I will start with numbers then what we did with about that numbers and what you can start doing on Monday as a protocol.

I'll start with audits and continue the line you restarted. Uh LA did 30 audits this year uh with eight independent security firms. We have zero critical, zero highs audits work, but that's still not enough because like you said, when you finish audit, it's just the beginning, not the end. Next one is lighter bug bounty. Uh so far uh from the very beginning of the program we paid $410,000 for white hats submitted. However, you

can follow uh this particular error that um initially white hats claimed uh to have like 180 critical security findings. after triage on our side uh it ended up with three critical payments actually made. So most of the work here unfortunately is saying no but still carefully uh what changed recently. So that's the whole graph of intake we have in bug bounty. You can see that starting from 2025, most of late 2025, intake has uh largely increased and you

can't uh just basically automatically beat up every submission. You have to have um uh a senior engineer who who should say yes or no and why. And ideally, you should have a second opinion about each uh particular about each material finding. Uh what else? So it's not only the code that should be audited and reviewed and put on scope of bug bounty. It's also external world change while your code stays the same and it might be even the state of code uh remains the same. What

I mean uh it might be dependency change. So suppose you rely on bridge aggregation and one of the bridges decided to change the uh approach for the for their relay mechanism. It might be your offchain stack dependency. Of course you can think about oracles first but that's not the only offchain tooling you might have in your protocol. Uh I mean it might might be auxiliary service which could also have its own weaknesses uh like race conditions bugs and things pretty hard to debug. And last but not least uh you still rely on something when you build a protocol for lighter staking. It's Ethereum itself. It's consensus spec. So when Ethereum

undergoes hard forks we must be sure that protocol uh would work correctly would work according to the spec and we won't be affected both from consensus layer side and from execution layer side so that we start testing every hard fork early with dev nets with our very own dev nets then public dev nets and public test nets and so on and so forth. Lately we found pretty interesting vulnerability in Glamsterdam hard fork and consensus layer spec. Uh the thing is that if you had a deposited uh like not yet deposited but pending validated deposit it could have been attributed to a

builder with the same pup key resulting in uh fund loss for this deposit. Uh luckily this was fixed. Huge shout out to Cordavos. Huge shout out to folks who supported our effort to make it fixed and on mainet this year we expect Glumpsterdam it will be fixed. Uh so that's why we started to build evergreen. Uh it's the idea of audit that never ends and that is um always aware of everything happen around.

Uh we started with two tracks. One is external track. We had a pilot with nether mind and another track is internal. We built very like our very own tool lighter lens. Uh starting from pilot uh nezamine team helped us to build uh a concept for lighter core code base. It's like uh 19k of code. Uh it was four weeks with two security researchers, two AI engineers.

Uh and the most of work was not about like picking the bos the best model. Of course, the most work was about properly uh gathering curated documentation and context. Uh so uh as a part of this experiment uh it was measured then when you have a proper context you have a real leverage over the model quality. So both uh detection rate increases and false positive rate decreases uh with you gathering context about your protocol your dependencies and so on.

uh three lessons we learned from this pilot. The first one as I said context is the lever. So pay most attention about like uh what your design intent write it down because design intent is something that uh not agent not security auditor not a white hat can understand pretty well from out of nowhere unless you written it out. Uh and of course don't rely on on any particular engine. Use bunch of tools.

They might be overlapping but if you have a whole family of tools um working together you get the most of the coverage. Uh you can learn about this uh particular pilot uh on nezine blog numbers appro uh particular results everything shared. So uh it it's available for like I async investigation. Uh for our internal track we built lighter lens. Uh it's the over like it's the engine that works over the clock. It has 39

uh repositories or projects at scope and it has like just four uh separate uh AI models underneath. Uh that allows us to sleep better than we slept before. Uh okay. So the follow up about lighter lens will be provided by Sergey. Uh please stay tuned. It will be in an hour or so. Uh what you should start doing on Monday like prepare your context pack. Uh if you don't have a team to spin up this particular like never ending audit then

try to gather external team and of course agents propose people approve approach works here. Uh, audits is a snapshot. Security must be evergreen. Uh, that's pretty it. Thank you. If no questions, I'll go otherwise uh like ping me somewhere. Thank you. Nice work.

>> Oh yeah, I want that guy. Hey everyone. Oh yeah, it's hot. [clears throat] Mike is hot. Okay, so I want to talk about securing DeFi together and a way to for all of us to actually spend less and be safer. We are doing an incredible job at coordinating. Uh looks like the slides off the top here. Uh but there take a little bit off the top. We are killing it sometimes, especially with Seal 911 coordinating all of us to respond to incidents. I mean, what we did with Defi United was nothing less than heroic. It It was just incredible. Putting together $300 million to rescue a hack in 9 days.

It's that's that's insane. But let's see. How much do we coordinate to fund security in advance? How you know, have you in the States, we have this uh this phrase, an ounce of prevention is worth a pound of cure. I think in DeFi it's more like an ounce of prevention gram of prevention is worth $300 million is a lot guys. How much are we throwing into the shared security initiatives that we really need in this in this space? Oh no man it's really oh it's better here. I mean we have so many problems in DeFi. It's not just incident response where we need to coordinate. We have scam compounds. All of our money that's being stolen from us is not only

being taken from our users and that means we have less users. It's also being given to just horrible people around the world that are kind of just this is not good. I I wonder sometimes is is crypto even an positive for the world. We're we're are we doing more for financial freedom or are we doing more for funding North Korea's nuclear programs? >> [snorts] >> Come on, keep going. Ah, so many memes. Here we go. No, there's one more. There it is.

I I want to propose that we try to raise less than a million dollars to fund 17 epic initiatives that can make really move the needle in DeFi. Oh, come on. I really don't know how to use this thing. Uh, one of the biggest problems that I think we have and the reason why ETH is not 10K is because we haven't crossed the chasm. And the thing that's really keeping DeFi from crossing the chasm is safety. It's just not safe. I mean, are you really going to tell your dad to like, yeah, self custody, go for it, right? No, of course not. He's going to talk to a MetaMask support person and lose all his money in no time. Like it

is not safe to onboard the early majority yet. We haven't done it. And whose job is it to do this work? Self- custody is just this is a requirement for DeFi. This is a problem we need to solve. We need to make self-custody safe. Sure. Like I the thing is I'm I didn't even have a bank account for 2 years. Okay. And I'm over here recommending people sign up for Coinbase. That's how bad it is in our industry. I do not want to tell people that. And I when I tell people that they can't access most of DeFi anymore. But yes, whose job is it to fix self-custody right now? This is what it looks like.

If Ethereum is an apartment building, everybody is sitting around guarding their own apartment. They're putting up cameras in their own apartment and being like, "Hey, look, we're all safe, right?" But you're not. hackers just go through the lobby, up the stairwell, through an air ga air vent, and then boom, they're in your apartment. Great work. You know, we we need to be more like this. And you know, it's really tough. Come on. Next slide. Who wants to help me out over there? This thing doesn't work. Maybe I need to stand over here. One more. There it is. Uh oh, no. Back.

Back. I'm just going to point to you guys because this thing sucks. Uh yeah. Next one. Now, if you look at this, no, back there it is. Okay, new apartment building, right? It has only three people with cameras on the inside. These are the people paying for everybody to have security in the apartment building. And I know it sucks. Freewriter problem, right? Suck it up. This is what we have to do. I'm sorry. You know, these guys don't have as good a security as the people who are paying for it. They don't have the internal monitoring, but they do all benefit from the shared security of these groups paying for the lobby.

But if you count the cameras, there's only seven cameras here. There were nine cameras in the other one. There's only one person monitoring all of the apartment building where in the other one you had nine. It is cheaper for these three people to coordinate to secure the whole building and they get better safety. This is the reality. This is the economics of scale when we work together to build security for Ethereum. Next, I know securing the lobby. Whose job is it? It's your job. It's your job. If you are providing security for a protocol and you want them to be safe, secure the lobby. Work to secure all of Ethereum.

Prevent the attackers from getting into the front door. This is our job next. And I'm going to help. We're going to help. It's not just on you guys to coordinate, self-coordinate. This is where the Dow Security comes in. The Dow Security Fund comes in. We're making 100 Oh, yeah. This is good. We've already funded uh 135 projects with a,000 Ether, but we didn't do that alone. We actually only make about 1,500 ether a year that we're dedicating to fund Ethereum security. We are doing this by coordinate coordinating with you guys and and beyond, not just the security folks, but actually the whole community

to try to figure out what even should we fund? What are the problems that need to be solved? Like I love what the Ethereum Foundation is doing. They're doing an incredible job, but in the end they are kind of top down deciding what to fund. We want to go a different route. We want to work with you guys to figure out what should we fund, what what are the most important problems to solve. Okay. Next, uh we have quite the epic group uh in the DAO the Dow security fund. Uh you guys know these names. I mean we have a really great perspective but it's not our job. We we've what our this the role of our curator group is to really decide like what are the most important strategies for distributing our funds

but we don't do the nitty-gritty details actually we leave most of that work to the ETH security badge holders who here is an ETH security badge holder raise your hand yeah basically it's all the rock stars in the room right uh the ETH security badge holders are 200 of the most epic security experts in Ethereum and they're going to do the nitty-gritty details of deciding where these funds go. Okay, next. Uh, but we need to work together with the community right now. I mean, these there's not really good stats of how much we spend on security. So, I had to kind of cherrypick a few points, but you know, in forum posts with Dows, you can see these things. Compound spent $4

million with Open Zeppelin in 2025 to uh create a security partnership. A sent $1.5 million to Certora in 2023 for a security partnership. So far, we have 76 initiatives on the Dow's board and we only have half a million dollars to support them. Now, if you scale this up, like we can do better. We can do better and it will be very valuable and important for our shared security. Okay, go next.

Okay, I want to talk about the security round that we're running right now. Uh, basically anyone can propose an initiative. Many of you in this room have proposed initiatives. uh they can be either for a grant for your team and you can propose as much money as you need to do whatever you want or it can be for an RFP where you don't know who needs to do that work but that work needs to be done and then we'll do a bidding process for it. Now, once those initiatives are approved, and I think I've approved about 70% of them, the others were out of scope or too expensive. Either way, once they're approved, they need to get 25 at least 25% of their funds committed from external sources. This is how the

DAO uses market dynamics to decide what to fund. We're only going to fund the ones that other actual companies say, "Hey, we need this, so we're going to stick some money in, too." We're going to be one of those people who are paying with who have a camera in our room, you know, we're going to suck it up and support the community once and then we actually have a vote. So all the badge holders who raise their hands they're going to decide which of these initiatives get funded and then the you know once they get fully funded by the DAO or the community then uh then we start the build process and the everyone gets paid all the initiatives only get paid upon milestone delivery and at least 33% of the money

is held back for real usage real security impact. Okay, next. These are the 17 initiatives that I loved on the board that I think are really valuable for a DeFi. I mean, obviously I don't have time to go through all of them. Cost 975K. And you can see just the top three are right really most of it, but one that I just want to point out is L2B for OBSSAC. It needs this is a really cool initiative that would allow OBSC build uh like the people who are doing OBSC audits to hold people accountable to actually executing on their recommendations. OBSC auditors are telling me constantly, oh yeah, we do

the audit and then the people are like, I'm not going to actually listen to you cuz there's nothing holding them accountable. If I [snorts] got five OBSC auditors to each put in 10K, we would have enough to get that on the board and pass it with the DAO. uh and and then there would actually be they would get more money. Those auditors would end up getting way more money than 10K because most of these are actual businesses that help the security space. Okay. Next. Uh so we can raise $300 million for DeFi United for one hack. If we had $10 million that would pass 76 initiatives without the Dow spending a dime. And if we just throw down 1 million, less than

1 million, we could put 17 seriously impactful DeFi initiatives on the board for the DAO to choose to fund. Okay, next. Thank you guys so much. Check out the initiatives that we have up there. They're seriously epic. Most of them are actually starting businesses that will be shared security services that we can all enjoy. Uh please check it out and talk to me if you have any interest in supporting the Dow Security Fund. So we have break for 1 hour for lunch

and then we come back after 1 hour. >> [music] [music] [music] [music] [music]

[music] [music] >> Heat. Heat. [music] [music] Heat. Heat. [music] [music]

[music] [music] Hey hey hey. [music] [music] [music] Heat.

Hey Heat. Heat. Heat. N. [music] [music] Heat. Heat. [music] [music] >> [music]

[music] >> Heat. Heat. Heat. Heat. N. [music] >> [music] >> Heat. Heat. >> [music]

[music] >> Hey, [music] [music] hey hey. >> [music] [music] [music] [music]

[music] [music] [music] [music] [music] [music]

[music] [music] >> Heat. Heat. [music] [music] [music] >> [music]

[music] [music] [music] [music] [music] [music]

[music] [music] [music] [music]

[music] [music]

>> Heat [music] up here. Heat.

Hey, heat. Hey, heat. >> [music] >> Heat.

[music] Hey Heat. [music] Hey. Hey. Hey. Hey.

Hey. Hey. >> [music] >> Hey, hey hey. really hey.

>> [music] [music] >> Wild. [music] [music] Hey. Hey. >> [music] [music] >> Hey, hey, hey.

[music] Heat. Hey, Heat. [music] Hey, hey, hey. [music] [music] [music]

Hey. Hey. Hey. [music] Heat. Heat. Heat. Heat. N.

>> [music] [music] >> Hey, hey hey. >> [music] [music]

[music] >> Heat. Hey, Heat.

Heat. Heat. [music] [music] [music] Heat. Heat. [music] [music] [music] [music]

>> [music] [music] [music] [music] [music] [music] [music]

[music] [music] [music] [music] >> Heat. Heat. [music] [music] [music]

Heat. Heat. Heat. Heat. Heat. Heat.

Heat. Heat. Heat. Heat. N. Heat. Heat.

Heat. Heat. >> [music] [music] [music] >> Heat. Heat.

[music] [music] Heat. Heat. [music] [music] [music] Heat. Heat.

[music] [music] >> [music] [music] [music] [music] >> Heat. Heat. N.

[music] [music] >> [music] >> Hey, [music] hey, hey. [music]

Heat. Heat. N. [music] [music] [music] Heat. Heat.

>> [music] >> Hey, hey, hey. [music] Heat. Heat.

[music] Hey hey hey. [music] [music] [music] >> [music]

[music] [music] >> Heat. Heat. [music] Heat. Heat.

[music] [music] >> [music] [music] [music] >> Down.

Down. >> [music] >> Backy. [music] Hey. Hey.

>> [music] [music] >> Hey, [music] hey hey. >> [music] >> Hey.

[music] [music] [music] >> [music] [music] >> Hey.

[music] >> [music] >> Backy. [music] Hey. Hey. [music] Hey. Hey. Hey. [music] [music] [music]

[music] [music] >> [music] [music] [music] >> D. [music] It la.

[music] Hey. Hey. Hey. [music] [music] Heat. Heat. N.

Hey. Hey. Hey. [music] [music] [music] >> [music] [music] >> Heat. Heat.

Hey hey hey. [music] >> [music] [music]

[music] [music] >> Hey. [music] >> [music]

>> for hey [music] baby. Hey >> [music] [music] >> way. [music] Hey

>> [music] >> Hey, [music] hey hey. >> [music] [music] [music]

[music] >> Heat. Heat. N. Heat. Hey, heat. Hey, heat.

Heat. Heat. N. Heat. Heat. N. Heat. Heat. N. Heat. Heat.

Heat. Heat. N. Heat. Heat. N. >> [music]

>> Hey, [music] hey hey. >> [music] [music]

[music] [music] [music] >> Heat. Heat.

[music] >> [music] [music] [music]

[music] [music] >> Hey, hey, hey. [music] Heat. Heat.

[music] >> [music] [music]

>> Heat. Hey, Heat. Heat. Hey, Heat. [music] [music] >> [music]

[music] [music] >> Heat. Hey, Heat. Heat.

[music] Hey. Hey. Hey. >> [music] [music] >> Heat. Heat. Heat. Heat.

>> [music] [music] [music] >> feel.

[music] [music] Hey Heat. Hey. Hey. Hey. [music] >> [music]

>> Heat. Heat. >> [music] >> Heat. Heat.

>> [music] >> Happy. Hey. Hey. Are you ready? [music] Heat. Heat.

[music] [music] >> [music] [music] [music] >> Hey, hey, hey.

[music] [music] [music] Heat. Heat. N. [music] >> [music]

[music] >> I wanted to go. >> [music] >> So welcome back everyone. Next up we have Sumanjit security improvements and oper operation operational sessions from P py lip P2 and py IPFC light.

Hello everyone, my name is Sumanjit and I am an open-source developer from India. Currently I am the maintainer of pilip which is a python implementation of lip P2P and I am also a maintainer of unified testing where we do all kind of interrop testing between different lip implementations. Recently I was auditing the security layer of Python lipid and there I have found some of the security gaps and today I want to share about those security gaps with you. What was the gaps how we have fixed it and what lessons we have learned from them.

So for all the people new to lip P2P, lip P2P is an open-source project which is used to create peer-to-peer applications, every peer has a unique identity called peer ID. And the peer ID is derived from the public key of that peer and lip P2P allows these peers to discover each other and create connections with each other. And along with that there are some security protocols like TLS using which these peers can create secure connections.

So while auditing the security layer I have found that these are the three issues where I have found the same pattern. We are not correctly verifying some of the certificates due to which we are getting some of the security gaps. So the first security issue was related to quick module where we are not uh correctly verifying the remote peer certificate. So that's why we can have a connection from remote peer even without that peer is correctly giving us certificate. The second issue was in TLS module there also we are getting some inbound connections and even if they are not giving us certificate then also we

are accepting this uh connection. Third issue was in peer records where we are not verifying the signed peer identity like we are not verifying who has correctly signed that certificate. The peer records issue is more important. So what is a peer record? A peer record is an identity or better to say it is an signed identity of a peer. It also contains the address on which that peer can be connected. So it is a very important thing. So if we are not correctly verifying who has signed the identity or the peer record then we are storing this peer record in our routing

table. So if we store this uh peer record in our routing table without verifying what things can go wrong. Okay, we can have wrong address of other peers inside our routing table. So our node can become isolated from the entire network. We might be connecting to different peers and we will think that okay we have connected to the correct peer. So we always have to uh verify before storing any kind of peer records and if we are not doing this then we are isolating our our peer from rest of the networks.

Okay. So there are some places or there are sometimes when we have one specifications and we have to create different implementations out of it. Talking about the lip P2P, we have one specifications of lip P2P and we have to create different implementations of it for different use cases like we have rushed lip P2P, go lip P2P and all other kind of implementations like Python lip P2P. So where we have to verify that whether they are able to talk with each other not each other or not. Even if we are able to create different implementations of lip P2P it will not verify that whether all the

implementations are verifying the uh nodes identity or not. Just imagine a situation where we have two different implementations. one is Python lip P2P and one is gol P2P. So they may be interoperable. They may be able to communicate with each other but then also it is not confirmed that whether both of them are doing the same security checks or not. So we have to do a deep analysis of each of the implementations that whether they are doing the right security checks or not.

So these are the four PRs which we have merged for fixing all the security issues security issues. The first one was quick then TLS then PR restore and there was one more security issue which was related to circuit uh relay. So we have got some more issues like the four GitHub advisory we have got we are working on it and we will fix it soon. For anyone working on decentralized systems or anyone creating some more applications I just want to say that before negotiating on any of the application uh level protocols you must verify whether the remote spears

identity is correct or not. Okay. Thank you. Thank you. Next up we have Sergey and the topic is the audit that never ends evergreen security in the age of LLMs. Hello everyone.

Yeah, that's worked badly. That doesn't work, I guess. Sorry. I guess we can start finally. [laughter] Um, yeah, I'm Sergey. I'm Solidity developer at LA and I'll show you how we approach the idea of a never- ending

audit. We all need audits, but I think we are doing them wrong. We still tread audits as a one-time check near the end of a development. um we write a code uh freeze it send it to auditors get a report uh fix the bugs and then just repeat uh but what about the offchain applications UI integrations and a lot of that code commonly never gets audited at all um what if audit became a part of a development process uh starting from development after the release and even further we can keep looking for problems even in the code that is already live

and um Frontier LMS allow us to do so. Um they are pretty much capable of doing security work today and finally with Frontier LMS you don't need a complex system to start doing this work. Uh they can easily check invariance check assumptions and u check how components interact with each other. So that's how we build lens, our internal defensive system that uses just uh a common coding agent such as cloud code and codex under the hood and uh we just give it the right context uh ask it

the right questions and it tracks our projects. It runs checks and gives us one place to review all of the findings. Um, we don't just run uh audits once. We um we react on all of the changes. Changes in the code, changes in the documents, maybe information about the upcoming hard forks and even just new LLM releases. All of that give us reasons to check our code again and try finding something something new. And um between these checks um agents just keep researching your questions to go deeper

and try to find find something deeper. Um we don't just collect findings. They have their own life cycle. Something's fixed. Something is still open. Something can be reopened to recheck again by humans. And um let's continue please. Yeah. As well as um we check all all of the snapshots of our code development branches upcoming releases as well as production. So we can find problems earlier at earlier stages and uh we don't need just to wait

for the final audits to uh discover security problems. So uh what's lens actually code for us um more than we can cover in two minutes of course but I'll just show you two public examples. First one is uh when we checked our code for a gloss compatibility lens just found a bug in the consensus specs but basically validated deposits could go to our builder with the same public key and here's the proposed fixed and it's already been merged a couple of days ago which is great and um this one is uh interesting. it it shows us why we still need um checking the code even if it's not

changed. Uh basically wormhole stopped its delivery service that our crosschain governance relied on. So we just had to update the setup and let's code this problem. So um that's what we built in light up but I think you can build something similar around uh what matters to you in house and here's why. Um first is that you know the context around your code better. Uh you know all of your internal documents uh why some design decisions were made this way or just previous findings.

uh you know the the scope and you know which contracts and which applications need to be checked together in one context and you decide when to run the checks. So uh with with that context you should be the first to check your own code to um like researchers and attackers have the same LLMs and the same capabilities. uh you just need to be sure that your goal is just to find them earlier, find security problems earlier before the bounty report or before before an exploit.

And yeah, LLMs keep getting better and your security baseline should keep getting better too. Uh do not hesitate to build your own version of an audit that never ends. Thank you. Thank you. Next up we have Ezra. The talk is about auditing is not bug hunting. Securing system through risk management.

Hi, good afternoon. Um, I'm going to talk today about our responsibility as auditors and how it goes beyond just finding bugs. Um, because when I started working at at the doing the bug hunting and participating in contest, my goal was to find as many bugs as I can in order to maximize my payout. But I didn't have a responsibility for the system as a whole. if I lost if I missed a bug, it was a lost opportunity, not something that that I should be too much concerned about.

And then I joined Storra and I started to do client audits and now I started to have a responsibility for the system as a whole. I had to make sure that I don't miss any bugs and especially those who lead to um who lead to, you know, losses of millions of dollars. So how did that change my work? In two ways. First one is prioritizing. Now in bug volunteers and contest as well, you have to prioritize by severity in order to maximize your payout.

But I would argue that this uh severity is often subjective or theoretical and doesn't actually represent the actual potential damage uh of each bug. And when it comes to um actually protecting the system, you have to be dead practical about the potential damage of each bug. So usually I classify this into like minor issues which are not that significant, then significant issues which you don't want to miss. But then there are those uh issues that make it to the news with millions of dollars stolen. And this is the kind of stuff which you really really don't want to miss.

Now the second way is by realizing that there are some ways to protect the system beyond just finding bugs and this is by introducing new hardening mechanism which would protect the system against some threats which are not due to onchain bugs. So a recent example is the hedron um protocol which I audited a few months ago where they have a propm propriety AMM unlike a decentralized AMM where the price is determined by an algorithm. Here the price is determined by a single owner who owns the liquidity in the pool and also updates the price through an Oracle

service. Now this Oracle service is um you know it has up to like million updates per day. So you can't have like a human approving each update with the cold wallet. So it's a hot wallet which is stored on some server and this is obviously has a potential of getting compromised. Now what happens if it's compromised is an attacker can basically steal all of the funds in the pool. So they can basically set a price so that they can give a very fraction of uh soul for example for the entire USDC and then they give a fraction of use set a price to the other way and give a fraction of USDC for the remaining sold in the pool and this way in a single transaction you

can just empty the pool. So what kind of mechanism did we introduce in order to defend against this kind of attack is the draw down guard. It's basically uh a mechanism which monitors the value of the liquidity of the pool and if it detects that the value is decreasing too fast then it pauses the pool and doesn't allow any for the swap because a slow decrease can often happen naturally due to price changes. Um, but if we see that it's just moving too fast, there for example 2% in 30 seconds, then we should pause the pool and don't allow any further swap.

Now, this slows down the attacker. It doesn't allow them to empty the pool in a single transaction, but it still allows them to do a slow drain over a few hours. Even with this mechanism, they can steal significant amount of the pool. So the second part of this mechanism is to monitor the pool through an external service uh a pa a bot which has the pa role which can only pause the the pool and not unpause it and in case it detects any invalid prices then it pauses the pool and the attacker can't um swap anymore. So those two mechanism together should significantly reduce the total amount of

funds that an attacker can steal in case the uh oracle ro is compromised. Uh because you have only a few seconds before the puzzle bot kicks in and the amount you can steal is should be you know depending on the configuration only a few% um before the draw down guard kicks in. So yeah, so basically this is an example of how we can this is not a bug in the system. This is an additional mechanism uh which we give to the client to protect their system and basically yeah this is this is the reason why the clients come to us. They come to us not just to find bugs but to protect the system and make sure they don't make it

to the news with millions of dollars stolen. So this is what we should deliver to them. Thank you. Thank you. Unfortunately, we don't have the next speaker. So, here is the video from DSS 2025. So morning everyone. Uh I am Arbas and I

have been a smart contract triagger on immini. So immini is a leading bug bounty platform for smart contracts and blockchain. So I will be presenting topic on bug hunters guide to highquality reporting. So using my own triaging experience uh I will be sharing what are those qualities that makes reports truly exceptional. So let's dive into the topic. Okay.

So the whole agenda of the talk is divided into two parts. So I will be doing a highle overview of five key qualities of a great report. Then we will be exploring each of these quality with good examples versus bad example to see like how it goes. So starting with the one of the first quality is the neat and clean title. uh and the whole purpose of having this neat and clean title is it should summarize the whole issue. So just by reading you the title itself you could get the whole picture around the issue.

And uh the next we have this bug description where uh it's all about like what the bug is and where the bug occurs within the code base. And one of the key qualities the white hat follows who submits a great quality of reports is they always explain uh the issues with uh with doing a comparison between the expected normal workflow of the functionality versus the malicious behavior around the functionality. So this is really helpful when it comes to bug bounties. So as a triager and as a judges who are not much familiar with the code bases new code bases. So having this expected behavior versus malicious behavior functionality it it makes a lot

more easier to uh understand the whole issue around the uh around the bug and uh the next thing they do is they use the proper formatting. So whatever the option the platform offers uh like bullet points or the markdown options. So they use all the options with the whole purpose of increase increasing the readability. uh and then next thing they do is they follow this proper referencing of the code. So we know that buck summation could get complex uh because you have to go uh you have to explain the nested structure of the code. So going inside inside of the function going into another internal function. So it's really important to keep the flow and

explain each of each of that flow with a proper referencing of the code lines. So uh that's that's the bug description. The next key quality is uh white hats always go beyond the attack surface. They always focus on the impact. Uh so one of the example is let's say the whitehead reported a a vulnerability where he mentions he found a re-entrance vulnerability in a specific function that's cool but what's the impact outcome of having this attack vector like what damage he could do to the protocol or the user of the protocol that's what the impact is. So they

always go beyond the attack vector. So instead of just focusing on the attack vector they go and determine what what is the final consens like consequences of uh the impact the attacker can achieve. So that's where the impact comes and the next we have this proof of concept. So beside just submitting the code P high quality reports often they provide uh dependencies that is required in order to run the P and as well as the environment setup unit in order to uh run the P. So also it's really important uh to have this P output within the submission because uh it's super helpful for triagers and as well as judges. So

looking at the PC output you can reproduce uh the like you can understand the whole issue around the issues like without even reproducing in most of the cases. So it's super helpful to have this P output failed uh within the P. Uh the last thing they determine is they think about any physibility limitations. So whether uh that could affect the course of the exploitation. So they think about are there any limitations uh that could uh interfere with the course of exploitation. So they be very open, transparent and think about like what are the walkarounds like uh they can bypass this physibility limitations.

So these are the highle overview of uh five key qualities of a great report. U in the next slides we can explore each of these quality with some of the examples. So starting with the title uh here's the bad example of a title which totally focuses on the attack vector which says uh delegate call vulnerability in a proxy manager which does not give much of the context and here's a good example of the title. So good example of a title is always a mixture of three composition that is like attack vector then the source then we have the final impact outcome. So here unprotected delegate

call is the attack vector and source is a proxy manager is a contract. Then we have this delegate function within the proxy manager and then it leads to the griefing. So reading the title it should sum up the entire issue. So you can get the whole picture around the issue. Uh next we have this bug description which it's really important to keep the bug description neat and clean. Just explaining what the bug is and where the bug occurs within the codebase and also explaining this uh uh doing a comparison between this normal operation of the functionality and versus the malicious uh behavior of the uh functionality to

just draw the difference like how it deviates from a normal operation. And the third we have this impact. So here's the bad example of impact or this white hats often do. So whenever they submit their impact uh like in the case you can see uh the white hat reports there's a re-entrance vulnerability in the withdraw function where he mentioned like which can lead to unintended behaviors and unauthorized state manipulation. uh which leaves you a mystery like what are those unintended behaviors and all.

So here's a good example of impact. So using the same example of re-entrance vulnerability in a withdraw function uh the white hat wrote like uh he it would result in a impact of direct theft of funds from the contract. Uh then we have the bad examples of PC's. So generally we see only two cases. Uh the first one is a lab grown P where the white hats develop the PC in a very controlled simulated environment just to demonstrate uh the attack vector and the vulnerability around the issue but it's not uh really applicable in a

real world scenario. So it's not actually demonstrated on actual code base. So we don't accept that as a P because it's not feasible. Uh then certain operations uh which is totally not acceptable because that's not how the actual conditions were are on the uh main net deployed contract. Uh then the another example we have this uh foundry

cheat sheet uh cheat code they use uh I call this as uh unlimited money glitch where they mean like lot of token supply uh capital uh just to demonstrate that hack we do accept the cheat codes but it should be practical uh they should always provide the source like from where they are going to get the uh supply. So it's not like uh using the uh capital which is not actually feasible within the ecosystem. So so here's the uh examples of bat P.

Uh then the last we have this physibility limitations. So physibility limitations are u to think about the uh think about the questions that uh that could interfere with the exploitation of the issue. So the questions you could consider like uh how cost effective the attack would be to carry out for an attacker like how much the attacker is investing into the attack what are the capital requirements he's putting there and how much profit he's getting out out of the attack and things like are there any specific conditions the attacker need in order to execute the attack or if the attack uh is being done or for a long period over

the multiple blocks. Are there any chances of risks of detections or are there any timeline for execution? So you can always determine this factor uh based on like the gas cost the attack is inquiring and as well as the capital requirement the attacker would need in order to carry out the attack and things like the m market slipage effect uh on the profitability the attacker would be making. So and there could be many factors depending on each and every uh different uh scenarios and cases.

So the whole purpose of this having physibility limitation is to be very open transparent to the project that yes there are some limitations and also think about what are the workar arounds they could come up uh to bypass those physibility limitations. Uh finally here are the advantages of high quality reporting. So we have seen like high quality reporting often leads to faster rewards. uh it's mainly because uh it makes u very life easier for our triagers and as well as the projects to go and understand the issue and reproduce as well as this leads to a faster uh resolve resolvement of the issue because it removes the whole

hassle of back and forth communication to gather the more information and often we we have also noticed that high quality reports al also leads to a very high-end rewards. It's mostly due to the effects uh effects of the efforts the white hat is putting into the submission and uh also there has been potential uh chances of getting the goodwill payout like even if your submission is getting duplicate or uh or if it's a known issue the projects always uh they go ahead and they always do a good will pay out for your efforts over there and lastly the white also build this reputation, this trust and this invol

this gives them a more opportunity where uh more opportunity from the project side to get him involved in some private audits as well and priv private programs to get him participate just based on the uh highquality submissions he submitted. So yeah so these were the five key qualities and uh the advantages of high quality reporting. So that's it. Thank you. Next up, we have Julia Hardy. The talk

is about what the block explorer misses using unique money laundering intel to contain active exploits. Okay, thank you everyone. Um, I'm Julia here with Zero Shadow and I'm going to be talking about yeah, money laundering insights and how we can use that to contain active exploits.

Um, okay. So um when a exploit happens I think a lot of times people will hopefully look at the attack vector um and and try to learn from that but really focus on the very first address where funds might have been um deposited into and then that's the end of their journey. uh maybe for some of the larger exploits some people will for example follow movements to Bitcoin for across chain for something like the bbit exploit but um what's unique about zero shadow is that we are looking at every single address that a thread actor uses from the very first deposit uh the very first stolen funds address all the way

through to the last address where we see a suspected cash out and that means that we have a really holistic view of how certain threat actors are moving their stolen funds. And the the insight that I get from a lot of people when I talk about freezing and recovery um along with security is why should we be focusing on the laundering side? By then it's too late. Uh we should really be just doing preventative work to try to stop any kind of um incidents from occurring.

And while that is definitely important, I think that the first or the year so far has really shown us that it can be a matter of when and not if for certain protocols to to be hacked and that knowing who your adversary is can be really important to um actually have a better containment when that exploit occurs. Um when we look at the first half of the year, we had calculated $1.8 8 billion stolen up until October and then of course the past weekend has happened and that number is now up quite a bit. Um we've also seen that a lot of these exploits are happening because of operational security. So offchain um

even maybe dependency related if you think about things like the Axis client exploit earlier or vulnerability earlier this year some of the different wallet exploits that have been happening where it's really not just contained to your specific protocol and zero shadow launched a new product this year the thread intel platform we have basically taken all of our stolen funds addresses and we're trying to better deliver them to the server services that can block funds. Um, and what that's created is a really big data set of all these different hacks that we look at, all the different thread actors that we look at, every single address associated with those movements, and we

can run analytics on those um, addresses and start to find some really unique insights. So, what does the data show us? Um, I looked at a few different groups here. The first one, trader trader from North Korea. This is the really big most sophisticated exploits. This is most recently Binance um across a number of different exploits. And um this this first stat here is how quickly the initial funds are actually moved out of the first address where they are taken.

And this is not swaps or anything. This is just um actually sending emptying out that wallet and sending the funds forward. And you can see that the ability to react to those initial funds is less than 30 minutes. Um, a little bit longer for some of the Bitcoin side, but um, but generally you're really just looking at a a a very fast emptying of those wallets, moving funds forward to new addresses. And so if you're really just focusing on that initial containment, you have a very small window to try to act.

But what's interesting is that we see that there's a longer window when the funds have been maybe spread out across 20 addresses. We're calling these the staging wallets before they actually start to do the rapid fire laundering. Um, and why does this occur? This occurs because North Korea is actually handing the keys over to Chinese money launderers to to continue with the laundering. So this is them preparing, coordinating with those, making sure that they can actually continue with this activity. Um, and we're seeing that this time of staging is decreasing over time. So it used to be, it used to be more like 6 months than you think look at last year, more like 6 days of this

pause between the initial theft and the rapid fire laundering. Um, now we're looking at more like three days, even smaller. So, why is this window important? Most important, I think for um anyone who experiences an exploit to realize I have only a few days to make sure I have law enforcement prepared, I have all the different services that I want to um know about these addresses prepared, maybe a security firm, any of those kind of steps. This is your big window before the rapid laundering to do so.

And then when we look at just the downstream laundering, so the the movement towards the cash out, most addresses are only holding a balance for about 5 minutes. And so um in in Bybit, for example, we saw 13,000 addresses used. And so again, this is just this idea that you really need the real-time information if you want to try to inter intercept these funds at any time. Um and we were actually able to do that. Um so this is from the Kalpel Kalpel exploit that we saw funds were originally going to Thor chain and um then theers were looking for a more rapid bridging opportunity. So they

switched to other bridges that were um ingesting the addresses that we were sending to them and we were able to intercept $700,000 worth of funds. Um this graph here on the right hand side, this is all the different services that were getting hits off of these addresses. So the launderer is trying to repeatedly send these funds in and getting rejected and trying again. Um so shifting gears here uh to other North Korea groups. Uh this on the screen here is the drift exploit. So uh the the specific actors here is Applejuice. Um, but who are this actor if you're not as familiar? Um, basically

these are not as obvious hacks from um the ex the specific vector that are used but they're always using the same malware. Um, or if you've heard of something like dangerous password where this is the Zoom call where the audio doesn't work. These are not as sophisticated of actors within North Korea but they're still doing pretty complex exploits. So when we look at the fund movements for laundering for apple juice, we see that the initial theft addresses are emptied pretty quickly. Not quite as quickly for from the trader trader side, but still between 30 minutes to 3 hours, those funds are really emptied out. And

again, you really need to be thinking more downstream if you're thinking about disruption. But what's interesting here is that we see that the funds will be parked for a really long time just sitting at externally owned accounts before they move to the next stage of laundering. Um so for two different cases here I anonymize them but we're looking at uh 10 to 11 months 4 to 7 months where funds are just sitting in in wallets. They haven't been moved. Um the reason that we see this um is is partially a re-evaluation of strategy. Um, and that's really allowed us to have a lot of time to understand exactly what we need to be prepared for. So, where do we

expect these funds to move to, what mixers, what lending protocols, get everything in order so that you can have really good results with disruption when that the time comes for those movements. Um, also we were able to see with the data that 86 to 91% of the time that the funds are being moved is between 9:00 a.m. to 6:00 p.m. Korea time. And so unlike with the trader trader funds where we see pretty much 24/7 movement and that's very much being automated with launderers, this is North Koreans moving their own funds, working a working day and then taking a break to go to sleep. Um, and so it's a very different style of laundering and again

gives you a little more time to to act. And then just looking at a slightly different type of actor, the non-nation state actors, um, we took a look at um, a couple of thefts that we've been seeing from the comm. If you've uh heard of the comm before, you've probably heard about these teenagers, early 20s kids who are a lot of times calling you up pretending to be um Coinbased security and you need to move your funds to secure them and you lose all your funds. We're actually seeing that that's not the only kind of attack that they do. Um something like drainer as a

service has definitely been a past um exploit vector, but we're now seeing actually just taking advantage of of any kind of vulnerability that they can see and even doing some more smart contract based exploits. And when we looked at a few different cases that we know are the same group of actors within the comm. What's interesting with the data is that the majority of the funds are ending up going to bridges as one of the first destinations um as a laundering path.

And so this is a really key area to concentrate on um as a victim of of a skid theft is to make sure that the bridges know that these are the potential addresses um of source of funds that you need to be blocking and freezing. if you can um intercept them. Um also as another uh non-nation state actor, there's been a lot more wrench attacks this year, a lot more in the news of the UK best based wrench attacks. Um with these actors, we see that the movement of funds can be 4 hours about between each address. So again, a much slower rate of laundering

and there's also heavy co-mingling across victims, which means the same address is being used for multiple victims over and over. So if that address is on a block list one time, it might have a good result in the future for another victim. And so that's even more opportunity to try to disrupt. And we did have um a recent success with disrupting a wrench attack. Um, so the victim had posted they had lost $800,000 on Twitter. Um, within 30 minutes those funds had gone through uh the threat intel and been distributed out. And ultimately about 90% of those funds were

frozen. And so there's a lot more of that coordination um possible not just with this actor but in general by being really quick with the delivery of these addresses. Oh, and that is hopefully uh the takeaway that you got here today is that data can really help contain your exploit. The common denominator across all these different actors is that time is of the essence. And if you're thinking about how do I prepare for my exploit, the common questions that I hear time and time again are how do I make sure that services know about my stolen funds? How do I move forward? what are my next

steps? What are my recovery chances? And I think the data is really the common denominator here to make sure that that's possible. So, thank you so much. Here are the socials for myself and Zero Shadow if you want to um follow us. And uh yeah, thank you So we have break of 15 minutes.

>> [music] >> Shadow. >> [music] [music]

[music] >> Hey, hey, hey. Heat. Heat.

>> [music] [music] [music] [music] >> Hey. Hey. Hey. [music]

I'm feeling you. >> [music] >> Heat.

Hey Heat. Heat. Heat. N. [music] [music] >> [music] [music] >> Heat. Heat.

[music] [music] [music] Oh, [music] [music] yeah.

>> [music] [music] [music]

[music] >> Heat. Heat. Heat. [music] >> [music] [music] [music] >> feel. Hey

>> [music] [music] [music] >> Heat. Heat. N. [music] Heat. Heat. [music] [music]

>> [music] [music] >> Hello.

Yeah. Heat. Heat. [music] Heat. Heat. [music] [music]

Heat. Heat. [music] >> [music]

>> You're [music] out. Feel [music] [music]

free. [music] >> [music] >> Hey. Hey. Hey.

[music] [music] [music] >> [music] [music]

[music] >> Hey, M. Heat. Heat.

Hey. Hey. Hey. >> [music]

>> Oh, hey. >> [music] >> Hey. Hey. Hey.

[music] [music] >> [music] [music] >> Hey, hey hey.

>> [music] >> Oh, hey. Feel [music] [music] yeah.

>> [music] [music] [music]

>> Heat. Heat. [music] you. [music] [music] [music]

Hey. Hey. >> [music] [music] [music] [music] >> Hey. Hey. Hey. [music] [music] [music]

>> [music] [music] >> Heat. Heat. [music] [music] >> [music] [music] >> Heat. Heat.

[music] [music] >> [music] [music] [music] [music] [music] [music]

>> Hey, hey, hey. [music] [music] [music] >> [music] >> Hey,

[music] hey hey. >> [music] [music] [music] >> Heat.

Heat. [music] >> [music] [music] [music]

[music] [music] [music] >> Are you

[music] [music] feeling >> [music] [music] >> Hello. Welcome back everyone.

Next up we have Neville Gr. The talk is about symbolic executive of math heavy code in the age of AI. >> All right. Thank you for the intro. I'm Neville from DDUB. Just a little bit about our organization. So we are a security company. We do audits. We're very well known in the static analysis and decompilation space. Uh we've built a lot of products that use some of these techniques. And as you'll see today, we're also into symbolic execution, which is a technique that underpins a

lot of the formal verification tools that uh we use as a community. All right. So, okay. So, what is symbolic execution? All right. So I'm going to use this example as a running example. So it's a basically a transfer function. I made this up so you will not see code as bad in the wild as this. But effectively in symbolic execution you don't execute the code using real inputs. Instead you execute the code using symbols and these symbols can represent all the possible values uh of every variable input that you have. Okay. So because of this you end up um when you reach a branch you

end up forking meaning that um you have a branch like an if statement you got to execute the program under both one side and the other side concurrently. All right. So what this means is that you will go down a lot of different paths. Um and I'm going to do a dry run of a few of these paths. Okay. So we start the program. All right. So we reach a condition. Reach a condition. An if statement. This if statement here checks you know that the amount in this transfer is not over a certain amount. Okay. At this point we

fork. So let's fork and go down one uh branch. Okay. Under this branch, we're going to assume that the condition is false, meaning that the amount is less than a th00and. Okay, if we assume that we add that amount to the so-called path condition, the path condition is a set of conditions under which the current under the current execution that you must assume to be true. then you reach another condition.

Okay, we reach another condition. This is a condition about the uh the current fee. In this case, we add also another path condition. Then at the end, we need to send these path conditions over to an SMT solver. And the SMT solver will check whether these conditions are consistent with each other and it will give us either a satisfiable assignment SAT or unsatisfiable. Okay, a lot of people use Z3 which is an external solver but you can also write your own solver. It's just difficult. So in this case turns out that this is ANSAT. Okay. So we terminate the execution here. We need to repeat the same process to all possible paths. In

this case, the program only contains three valid paths. But as you can imagine, real programs are going to have a lot more paths because if you have, let's say, 45 branches and each branch has a branching factor of like 1.5, meaning that you know one side succeeds, the other side has a 50% of continuing. You will have 84 million paths. Okay, which is which is a lot of paths and you know a single query with an SMT solver it can take minutes potentially and actually analyzing D5 protocols is harder. Why is it harder?

It's harder because you find a lot of code in math libraries which uh which combines different kinds of algebbras meaning that it uses both for instance addition, multiplication and subtraction which you need certain techniques to reason about and also it uses you know shifts uh and or or bitwise operations which require different techniques. And so if you go down and use one kind of techniques, you need to convert one kind of math into another kind and that creates a lot of complexity. This is an example from unis swap v3. In this case, it does uh 512 bit multiplication

followed by division. All right. And then on top of that, you also get complexity. Let me show you an example. So you get additional complexity. This is another example. This is also from unis swap. But in this case, it's a function that helps you compute the price of an asset based on the liquidity in a in a particular tick. In this case, you get like 20 possible if statements. And you know, all branches are mostly feasible. And so you get once you enter this function you multiply the number of pads by around 1 million 2 to the 20.

Okay. And the correctness of these D5 protocols really relies on code like this. A lot of tools will not support code like this. A lot of provers will will choke. So what do we do? So we've devised a series of techniques. Okay. Some of these techniques are original. Some of them are appropriated. Okay. Okay. So the first thing we do, okay, uh we are known in the decompiler space. We've written a lot of techniques to try to lift code at a level of representation higher than the bite code. Okay, that's in the DOB decompiler. We've used some of those same techniques to lift low-level code also to a higher level presentation. The

screenshot uh shows a simple program which has been compiled and it doesn't do anything special. It just copies a strct around call data storage and that sort of thing and does some arithmetic. So for instance the uh code in green is you know like checked arithmetic. It really translates to like three or four mathematical operation. So this is the sort of thing we do. There's a lot of techniques which go into uh doing this convert lifting to a higher level of presentation. Second thing we do is we undo the optimizations.

Now this is easier said than done and also you might question why would you want to undo the optimizations? I mean they're there for a reason. Well, the problem with optimizations is that the uh library auditor authors, they have exploited the fact that they're using a a machine, you know, with with bits and that sort of thing. And by exploiting this, they can get better performance and in some cases they can get also better um better accuracy, you know, can they can utilize uh the bits better.

Um but unfortunately these also introduced these mixed algebra um expressions. So we do one of two things when we see an expression which is problematic. We have devised algorithms to either convert these to idealized mathematical representations such as in the first example that's the min function. Second function is the average function. It's simpler to reason about than the one on the left hand side. Or another technique is to convert for instance a bits operation into an operation that operates on data structures. So the operation on the right hand side is a

slice of bits. Now you want to be careful you know the algorithms need to be careful to distinguish between the two. Okay by the way a lot of optimizations you can read about them in this book but this was written for C. It's a good book. All right. So another technique is to write your own SMT solver. Now this is uh not as simple as I'm saying um effect. So you don't need to write your own SMT solver. Z3 does a very good job but it is designed to give you either a satisfiable assignment or unsatisfiable.

and to get a satisfiable assignment that um requires more computation than you might need. Instead, during symbolic execution, often times you're more interested to know whether a uh path condition is completely unsatisfiable or whether it could possibly be unsat possibly be satisfiable. And so writing a solver like that is simpler and also the algorithms that you can pick and choose into the solver. you can make the solver be linear time and you can utilize techniques from computer aided algebra systems which are faster and I know that some of the these techniques

are also used in Z3 but you know linear time versus double exponential but there's a caveat at the end of the day you still need to use Z3 in some cases all right another technique this is actually appropriated. A lot of uh symbolic execution engines they do summaries. Okay, we also do summaries in our symbolic execution engine. So summaries you are actually encoding instead of like um forcing the engine to execute a lot of difficult and complex code. you either reimplement it in a simpler way using idealized mathematical operations

or you just put in there you know the additional path conditions that you would need to add. Okay. So the way we u wrote our summaries is we went through a lot of define math libraries and we asked AI to write summaries. Okay. And our symbolic execution engines have a has a lot of summaries in it now that matches to specific libraries. And obviously we don't trust the AI. So we uh we use fuzzing to you know ver validate these summaries against the actual code. Now you might be thinking why use fuzzing when it can use symbolic execution? Well for small functions small pure functions

um that don't do much. Okay. So these are mathematical functions fers can actually do a good job at uh disproving you and so it's easier. And finally if you accept the fact that your symbolic execution engine is going to be more scalable but as a as a result you might get a few more false positives. Well, you can have an aid agent in the loop that verifies, you know, whether whether a finding is true positive or false positive. You want to be using frontier models, but frontier models are very expensive. But how can you get the cost down of to these frontier models? A lot of tools when they give you a

finding they produce just gibberish or I mean an expert can interpret it but it's like really long okay and really long traces through bite code and through memory operations and that sort of thing and it's a waste of tokens to go through that. So a lot of you can you should dedicate a lot of engineering to try to decipher that and get a more highlevel output from your tool so that the AI agent does not need to spend a lot of tokens on this and it's going to perform better and then you can use a better frontier model.

This is actual input uh output from from our tool. Okay. So everything maps back to source code operations. Okay. It's it's in a familiar format. That's also another thing that you know they uh tell you you know how to integrate with AI models. Well, you make the output familiar to them as well. Okay, let's look at some results. So, we've implemented this tool. It's a molec execution engine and we compared it against HVM and Halmos.

Okay. So we picked 100 random smart contracts, smart contracts that have been used on chain recently and uh we're running these tools offline meaning that you know storage is symbolic and and that sort of thing. Now it turns out that a lot of tools they are not geared towards exploration meaning that they are geared towards you know like um checking a single property not at checking all the executions of of code bases. And so in the case of Halmos we wrote a custom harness and we needed to fiddle a lot with the settings to to make it run uh this experiment. All tools use Z3 120 seconds timeout which is like really low. Um, and all the

exploration parameters, you know, it takes a long time to configure these tools to make sure that they're level playing field that they're all exploring the same number of paths and whatnot. Okay, so in the case of our tool, we managed to analyze 80% of the smart contracts, all possible parts. Okay. Um, except loops in the case of HVM 31% and halos only 26%. Okay. A lot of these tools have partial results. They actually most of the time what they do is they choke for instance when parsing call data or you know moving things to memory that sort

of thing. So because of the loops. Okay. So uh we've uh deployed this tool internally. We're using it for uh auditing at DOB. Uh we also use it for bug hunting. And so it's designed as such. It's it's it's currently not designed to uh to be a replacement of a formal prover, but it could possibly become one in the future. And right now we're also doing explorations you know trying to see whether um you know certain EIPs will break contracts in the future once they are deployed and and that sort of stuff.

All chain analysis kind of like what we were doing with static analysis. Any questions? >> Okay. Yep. on how we kind of cut the cost down in symbolic execution. >> Yeah. >> Hi, I'm Manu uh from LIP P2P. Amazing talk. Just wish to ask how you are kind of optimizing the cost of symbolic execution when you're building a swarm of agents and you're kind of using some of the things to verify and also have some of the agents to kind of do uh the uh like the final job over here. Yeah.

Thanks. >> Yeah. All right. So, first of all, you got to optimize the um you know the interface of the tool, make it appropriate for command line um environment and that sort of thing. The output as I showed on one of the previous slides is very very dense and maps directly to the to the source level. It's like compared to some other tools out there. You know, other tools will generate pages and pages and pages of output. this one will generate you know the very succinct things. So this this is basically heavy compiler engineering right? It's compiler engineering trying to map you know back to source you know get get all the

debugging information through the compilation process. It's that sort of work. So my my question is what would you say is the greatest one of the major challenges in terms of adopting symbolic execution in the generic auditing ecosystem. Your form of verification you got fuzzing. you have so many different things is what was the biggest challenge

you would say? Well, the biggest challenge I thought, you know, when embarking on this project is that most tools don't work well enough to merit, you know, spending enough time um getting them up and running because most of the tools, you know, I kind of like alluded to this. They're not designed to explore an entire contract. They're designed to look at a single function at a single property, you know, like a property on a single variable or something like that. So, that's very very time consuming. um you know tools get better and better and then instead of using the tool you ask your AI agent to use the tool that's going to be free for you right you ask load hey use this tool on this and if it

works you're going to get good results. So basically when you reduce the the type to the integer that will be like more um more CV friendly type that could be quick make the solving time quicker basically like when you convert all these like type to be more solving friendly um for the SMT solver then what's the basically downside cost like when you face all these like bit type and um potentially that could be like forcing the bit factor in the SMT lip language instead of forcing it to be integer that definitely faster but like what's the downside cost of all this

address type all this dynamic factor type dynamic array in the solidity because that must be some downside costs there yeah >> yeah there's there's lots of downsides I mean first of all for instance when when you treat au in 256 as an idealized integer well it's not going to wrap around but if you know that you know that code which which it is in is an checked code all right then you can still treat it as an idealized integer and then you just add an additional check that it doesn't exceed 2 to the 255 26 minus one and it doesn't go below zero for instance. Okay, so you can use some of that type information and then

it's just as sound as using bit vectors except that bit vectors which would be sound in this case uh if you try multiplication and division you're going to break the solvers because it's going to create circuits that are too big. There's a lot of tricks like that and frankly you do end up with some unoundness if any of these algorithms are not perfect. Thank you. Next up, we have Christian.

Don't trust the first model, a methodology of adversal AI audits. >> Thanks, How many security researchers do we have in the room? Raise your hand, guys. Oh, great. I see a lot of you. So, from a security researcher to security researcher, please don't trust the first model. So you know uh LLM models always try to convince us that they went through all the codebase they checked everything and uh that those this is the list of all the vulnerabilities that are in the codebase but the biggest issue

that we have here is that they are overconfident and at security we developed a methodology for doing this adversarily. So how to have models challenge each other in order to reach an agreement. My name is Christian Vari. I'm the the head of a operation and O security. O security is uh spotting vulnerabilities since 2017. Uh we have worked on more than 600 engagements and we have a pool of more than 50 senior security researchers.

So we usually ask a lot of things to LLMs and we got usually good replies. So we get a lot of info from them. But there is one thing that we usually don't know. We don't have the real coverage of what they've done the real part that they checked. So is true that probably they checked mostly of the things but we don't have the observability for being sure about that. So what if some files has not been read? If uh some parts were not been examinated, what if they just keep an entire file? U we're not just thinking about you know smart contracts but maybe we are auditing a full node or

uh you know uh offchain components that then move nodes. So we have big parts large amount of code. How can we be sure about the coverage that they have uh have checked and also another thing u not just you know the the file and the codebase but also the claims. So have they challenged really all the potential things that are in the codebase have they challenged the assumptions we usually just by you know running LLM or a model or something like that we're usually not really aware of that so we came up with you know a an arness a workflow uh we have implemented it and it name is iive but in this talk I will

just uh tell you the methodology I mean you can apply the same methodology ology um we um defining this in five steps actually. So the first one is the scope. So as a security researcher is what we usually do. We prepare a scope. Okay. So we have the commit of the uh codebase that we will review. We have you know the architecture we have the boundaries you know the the the preconditions and all the issues or you know uh things that are already known to the client.

Then we have for each of these block a gate. So for the scope we have the gate that we know the scope. Then we have discover and this part actually is where we use a multiple amount of models. Usually we uh try to run all of them. So from different providers and different type of models in order to check the codebase and spot all the possible vulnerabilities. The important thing for this is that at the end of this part of the process we have some very specified uh candidate of vulnerabilities. Then we next to the the gate open and we move to the next step that is actually the the duplication and we uh actually perform

some uh some execution of the models in order to get a single uh a single candidate. Then we do the validation. I'll explain you why that is one of the most important thing. And we then move to the the human part because we believe that at the end of the process we still need a human reviewer. And this is just you know a suggestion ano a testable hypothesis of what the vulnerability will be. So that's what I was saying before we are creating the scope but our tool should be able to ensure that we check all the all the files all the bots and check all the potential uh precondition and and uh and uh also uh the external dependencies where something is built

on. Uh so for example here in the in in this uh in this matrix we are just checking you know that all the models checked all the file and this is important because sometimes we uh have a global coverage on all the models that are working on that but we are not ensuring that the each model have 100% of the coverage. Oh, another important thing is that models should not be biased and this is really in line with what we usually do with our human auditors. So at O security we have our blinded approach where each auditor actually go through the codebase uh independently so without sharing insight

with the other auditors and we are trying to do the same thing apply to models. So the models have a shared input where they have you know the code base, the revision, the architecture, all this kind of stuff. And then also we kept separate all their work. So the candidate findings the the path that the models uh went through in order to find the the vulnerabilities. Then we start with the discovery that is executed by multiple models and is actually performed in two step. So we have a blind pass where actually the models go through the most known you know vulnerabilities glasses like I don't know uh overflow arithmetics all this kind of stuff and then we have very

informat so in all the the past engagement we got a lot of knowledge about uh vulnerabilities and potential issues so we created a a data set for that and we use that in the informat pass and we actually execute both the informat pass is also very specific depending on the on the technology that we are auditing. Another important thing is that at the end of the discovery phase we have the claim that is testable but that is well defined. So we have to know who is the attacker. So the role and its capabilities what are the preconditions.

So probably uh you know uh that type of attack have a precondition and depending on the precondition depends also the severity uh the boundary the invariance if there are scope the invariance actually it should be checked the location obviously so the code and the related code and the provenence so which model uh found it and which face so the important thing for us is giving an an audit log actually of what happened who found something and the path that has been executed it this is very important especially on very very large code bases where we have I don't know a node that is depending on a big SDK and actually we have to scope the the wall path in order to pass it correctly to the model

and also you know uh have um a feasible type of cost because you know tokens are not free another part that is important so after the the the discovery part we have this list of uh of uh findings, potential findings, we have to duplicate them. And you know uh as a security researcher, everyone has a way for doing the the duplication. Okay. Uh it's a very opinionated thing. And in our opinion, the best way is with the root cause.

Okay. So here for example, we have two claims, but they have the the same root cause and the same fix the same thing. And the model should be a able also to separate the things that that makes each claim uh unique. So for example here it should be able to uh separate the part that are in common and merge them into just one and then also create another findings with the remaining part. It's not working. Okay. Well, just trying by the way even if it's not moving. Okay. Yeah. After that we have the validation and this is the most

important part because uh actually we use this as hypothesis for the uh security researcher and we don't want to waste the time of security researcher. So it's true that we have a lot of harnesses for generating findings but there are a lot of false positive and bringing a lot of false positive to security researcher is actually a waste of time. You know you have 200 potential findings and the security researcher have to spend their time on doublechecking the all this AI crap instead of checking and the good and this is you know is something that we cannot deal with. So the idea here is to rerun all the the the claims that have been found adversarily through other

models. So we create a fresh context with this with all the data that is required all the dependencies and all the the the architecture part that is needed and we actually let those new models try to execute them and validate it. also is very important especially in large code base like I don't know a blockchain node or this kind of stuff to give all the the the path to them so the the the dependencies so imagine a big SDK or this kind of stuff so we have to give all the context needed trying to scope it to make you know the less amount to spend the less amount of tokens and this will be able actually uh our models to um identify where a part

is actually something that is reachable or not. For example, because it's very common, you know, with models when you use them that say, okay, we have this kind of vulnerabilities uh just go through it and you can execute it. But then it's not really true because maybe in a dependency or you know depending on the on the execution uh it there is a difference because maybe it's gated. So like in this example and one another thing that is important in our process is confidence. So I mean we uh have traced all the the all the path that our model our methodology is going through. So we know which model

found something and at which stage and we have all the audit log of this. Having this we have this part of the model that actually create a summary of that uh and also depending on a threshold put the findings in a different way. And the important thing is that we are able then to pass all this information to the auditors. So if we have some models that are supporting it, some model that are refusing it and you know they're not really sure about that actually we gave all their thinking to the security researcher the human one the the real one in order to be able then to to judge this.

At the end of the process we have this last part that is uh you know a sort of health health check. So sometimes you know our models you know we use all of them can you know give no verdict or giving no candidates or just not read the scope. So it's very important that your harness is able to identify that to be aware of that because we are tracking it and then be able to rerun it. So if uh I don't know a part of the codebase has not been checked or if a part of the architecture is still uh not checked or we are unsure about it we have to iterate about that or at least we have to let the auditors the human the human

auditors be aware of it in order then that they can then just go through it manually and check it. So this is our model actually we implemented it through our tool that is called IVE and you can actually get more information on our website that is oxcurity.io you um um our tool is uh something that uh you can use if you reach out to us but the methodology is something that you can they can use as you want because it's something that is not really dependent on models or technology and that's all uh if you want to reach out for uh for trying it or just have any question I'll be here thank

Okay thanks. >> Thank you. Next up, we have Manu Manushil Gupta. What a lipid lipidup gossip sub crash taught us about AI security and defy infrastructure. Thank you. Yeah, I have to press the lower button. >> Okay, button. >> The lower button. >> Okay, sure. Thank you so much.

>> Good afternoon everyone. I'm amazed to see the kind of work everyone is doing in security. uh before the conference uh it's one of the responsibilities when you're running an afternoon session to kind of figure out ways through which we can get everyone energetic and I was actually wondering that over the course of last set of hours uh I think the everyone who was speaking over here they were like really energetic the kind of uh thoughts and the kind of discussions we had it actually gave me the idea that sure Binance attack has happened but that's not the end of the world I think if we all uh come together we can ensure that we can have a better D5 security and a protocol system. So my talk is essentially about the same. I'm Manu

Gupta from LIP P2P uh one of the maintainers and the technical lead and it is all focused on preventive security measure. Preventive security measure means a place where we have prevented some kind of Binance hack not to happen. So I'm taking that into consideration. uh my talk is on gossip sub crash and there are two very key developments which I'll try and cover over the course of talk one is on defi infrastructure and second on AI security which all of you my wonderful friends you have been working so well uh before we get into some of these glitches I'll try and see if uh things work out well just one second yeah okay fantastic so a very quick 101

on the infrastructure level I wish to share all of us uh have been discussing about how we can ensure safeguard of security measures at the smart contract level and at the application level. Fantastic. I mean that's great. But I also wish to share with you there is a very interesting surface beneath every application layer in a decentralized finance protocol and that is essentially what we call as the infrastructure level and the infrastructure level u is one of those things where you do not have to attack. You do not have to figure out keys to figure out where the problem is. You do not have to go for bounties. All you have to do basically is ensure that the network stops talking. And if the network stops talking in distributed systems, we have this very wonderful

concept like there are three attacks which I wish to share with you. One is network partition, second is sele one of these attacks they happen. What we are basically saying is the entire assets that we have in D5 they will not be hacked. You'll not be moving across wallets. basically the network will stop working and that essentially is one of the things which I'm worried about when I look into some of these recent happenings at the uh Binance uh attack case as well as some of the previous ones. So what I'll be trying to unfold is probably a collective discussion and a collaborative uh method. I think that's what we should try and do during afternoon sessions. we'll try and uh kind of figure out what we can do better

at the infra layer and also at the application layer using some of the existing innovations that have happened in AI and without AI which means using fuzzing as was been mentioned uh previously by one of our friends. I would also kind of share some of the key things we need to understand at the uh network level where we're talking about very core methods of publish and subscribe and also of peer communication. So very quick uh 101 at the infra level what we'll be discussing in the course of talk one would be peer communication peer communication via gossip subub flood sub and grid topology second we'll be discussing peer routing so peer routing is via cadmia dht third we'll discuss about some of the

transport methods which we are using in ethereum the most notably is quick which is now now heading towards becoming an ITF standard we'll also discuss about TCP our connection oriented system some of the connectionless systems like UDP websocket secure we'll discuss on web RTC direct which definitely chromium deprecated but we have got a web RTC direct v2 and I would love to have some of you please contribute at the specs of lip p2p to try and see how we can ensure a better participation in that and then we'll discuss how quick uh which is one of the key methods which is used by all the consensus clients of Ethereum how we can ensure a better security using encrypted client hello and ECH ITF standard which is going to be discussed

two weeks from now at ID of San Francisco and uh I would love to meet some of you over there and uh definitely looking forward to catching up on that. So first wish to share with you about uh one of the uh key learnings of D5 security management at infra level. What we see basically is one of the basic problems uh in the way we are writing code and the way a lot of AI work and agentic work is happening is that sometimes the training of data is happening from what I'll call it as not a sane data which means that agents sometimes they're trying to do underfitting and overfitting which is the same problem of like what we see in machine learning they're trying to have

that same set of problems in infa level [clears throat] security management which means If I look in the last 3 months, the number of security issues that have come to me at the infra level, that is equivalent to the total number of security issues that I have received over my career working at the infra level. So that is the number that I'm seeing in terms of the participation of security issues. Now the point is what are these security issues? I'll first mention that and second I'll mention why many of those issues are not relevant and why many of those issues are like meto issues and how we a maintainer how a developer who is working at the infra level they can ensure that they look for those things which means like a in a

funnel operation they look only for those issues where it's a make or break scenario so we'll try and work out the optics for the same so the first thing essentially is uh like if you look through this diagram what I've essentially explained is that if your nodes are out of sync and if there's a panic in one of the nodes. So we have a distributed network. Uh just a very quick question you are all familiar with validator nodes and consensus nodes and how execution and consensus clients work. I mean if there is any problem we'll definitely discuss on that but I'm assuming one particular part while I'm discussing this diagram. So we have a distributed system. We have the consensus nodes. They're all talking to each other. And what happens is there is a panic that is getting triggered in one

of the nodes. Now why this panic would happen? This panic would happen by one of the very basic things integer overflow which was explained in the last to last talk very nicely in the symbolic execution talk also. So that is one of the key things which causes a panic and once that panic happens people like as a longive network or as a fall tolerant network we would expect that Ethereum would kind of come back to its original state very quickly. Well that is what we are trying to do and that's why I'm saying that my talk is a preventive security measure but if that does not happen if there is a quantum attack like what Justin very recently mentioned he's a good friend he shared about let's get into bunkers mode. So just to ensure that we don't get in even if you're in a

bunkers mode we do the security well at uh at the bunker level I do wish to share what really happens is P2P state sync stalls the oracle feeds halt and liquidation bots fail essentially what we are talking about is D5 security coming under serious threat now it's not like I'm trying to make any one of us like I'm so happy to see the energy over here and the kind of discussions and the kind of cases we have discussed that I'm not trying to shift via this example that this would happen in Ethereum. What I'm trying to share is that these are the things that happens when you have an inte integer overflow and that integer overflow causes a trouble in the overall consensus client. So if a consensus client gets broken then essentially what

we are seeing is a defi problem at scale. Now how do you ensure that that does not happen is what we'll discuss. So we'll take a specific case which is a very popular one. uh it got lot of attention at NIST at all the key uh places where we discuss uh about Ethereum security and uh it was being shared by everyone uh who was working in Ethereum and I was essentially the official spokesperson for doing all this discussion around CBE. So I wish to share first of all that uh this was one issue which we faced in Lighthouse.

Lighthouse is like 27% of the Ethereum or 30% of the Ethereum consensus client market. uh it goes up to 43 now. So in the last year you can say that in consensus clients it's like 43% it uses rust lip. We also have prism client which uses go implementation of lip p2p and then we have some of the others like nimbers loadar uh and uh some of the lean ethereum consensus clients. So I'm taking one specific scenario and I'm sharing this because we were able to safeguard well. I I mean generally where we are not able to safeguard well uh it's not easy for me to disclose because there's lot of PR related discussions that happen but it's important to uh openly discuss some of those things. So wish to share if you talk about this

exploit what this essentially was that we have a swarm of autonomous agents and I'll also share how we can create our own swarm of autonomous agents. We basically had a very interesting integer overflow function and that was causing serious trouble. Now the point is if you would think like what would really happen if there is an integer overflow. So the funny part is it basically causes a node to panic and node to then go offline. So the trace is basically the following. You have an integer you have the arithmetic operations as was explained in the previous uh talk. you have either the bitwise operations or you have the algebraic operations and you have a specific node which has not been defined or which has had a memory

overflow or a memory specific issue. So if you have that kind of a specific problem what happens essentially is a fatal panic. A fatal panic means node out of sync and node out of sync basically means your D5 protocol doing behaving or misbehaving for the lack of better word in a way uh that it should not uh behave and sorry I'm uh there is some trouble with uh yeah uh just one second I'll just try and see if we can move slides.

Okay. Wow. Sure. So yeah, thank you. Uh sorry uh sorry for the hiccup. Uh yeah, wish to share that uh essentially what that basically means is that if a specific security operation has happened in a manner that it has caused the node to go out of sync. What it basically leads to is the entire D5 protocol coming into serious problem. I mean this is what we have found with some of our friends working at AWE Morpho and some of the key D5 organizations that some of the key mention points or the spotlight points that they do say is that if you have the nodes in sync and behaving correctly and you have to be right 100% of the time I mean you get one time you get incorrect

and you have like some integers behaving inappropriately. You have the nodes going out of sync and you have the entire network going down. So here is a simple diagram I do wish to share. Uh and there are two parts to it. One is what is mentioned in this diagram. There's another thing which I also wish to explain. So this is essentially a simple workflow on how we ran a swarm of agents to do a code trace to figure out the root cause analysis to do coordination across different implementations. At lip P2P we have 17 implementations. uh seven of those implementations are used in all the Ethereum consensus clients which means if there is a problem at the Ethereum consensus client level then we are to be blamed and we take full responsibility of the same. So

as a person uh who is responsible for the consensus clients I mean we do follow some traces and this is one of that specific configuration. There is one thing which I've not mentioned over here which I would love to explain and I would love to have everyone work and that is how we have set up these autonomous agents. the configuration and the setup is very very important and as we learned from the previous talk it becomes very essential if you have to do the right kind of analysis. So first you should be looking at agency directory service. You should be looking at how you can create a directory service of agents where they have a routing discovery and a communication system.

And I would strongly recommend going back to David Mazida's time at Stanford University where he was working on academia DHT. Use that as one of the key methods for intelligent routing. The second part which I do wish to share is very very significant and important is the messaging between agents. And there are two different ways of doing that. One is in many organizations we see that they have problems with non-HTTP protocols. So there I do wish to share if you're trying to do an A2A or MCP try and do it over HTTP and in many other cases you can create your own secure low latency messaging protocols. Sojit who just presented on one of the interesting talks at pilot P2P uh four five talks earlier. He very nicely explained how we can have these nodes communicating and

talking to each other and kind of sharing in real time. And the third thing which I do wish is to share is identity interoperability of agents. Which means if you want Ethereum nodes to not just function between your computer and one or two computers but if you want to really do it as a collaborative action operation so that anyone who is trying to approach you from a nation state is uh not getting uh their kind of benefits if we start operating together as a team. So the third part essentially is having in identity interoperability of agents form. So there I would recommend try and use some of the ID of standards like AOTH which is O 2.1 or you can use uh open ID for doing identity interoperability. And the third fourth piece essentially is the observability

part. Observability in agentic ecosystem is one of the key essence. I mean it's not just about tracing or hotel or telemetry logs. It's the entire action agent state capsule and uh we would be presenting about it at ITFSF and would love to have your uh thoughts on the RFC that we have. So moving forward uh if I can I think I can. Yes. Sorry I just went one step back. Okay. Fantastic. So yeah moving forward. Why I'm saying that we should try and use AI security? Why I'm not uh talking just that we should look at traditional fuzzing? I think there are some very excuse me uh there are some very

interesting benefits uh from the uh AI models the way they have been approaching. I think one is that it kind of reduces the cognitive load on all of us as security researchers. I mean if you are a researcher and we are working through massive loads of data, one of the key things we face is that the cognitive load is something we all wish to address and triage if you really believe my friend is right now the product. I mean the amount of as a maintainer the number of security issues we are receiving in the last 6 months and I I I can definitely suspect in the last next 6 months it will be almost 10 times more than what I have received in the last three uh previous 6 months. I do feel that one of the key things over here is how we set up the ecosystem. How

we keep a balance between fuzzing that is uh traditional fuzzing and also the agentics forms and try and see where it works and where it does not work. And I do wish to share with you uh the inventor of fuzzy logic was interestingly my adviser friend uh Dr. Professor Zade at University of California, Berkeley and he said something very interesting uh and that is that fuzzy logic is very similar to is very similar to words with computing or computing with words. If you use the logic systems in a systematic manner, you do not need any AI model and he used to openly say that and we have seen that it works very well and in many cases where you have a logic task, I would still say go for traditional fuzzing.

Agentic systems or agentic workflows are fantastic when you are working with differentiation calculus tensors mathematics, isolated algebra. So there I do wish to share the AI systems are doing fantastically well. Why? Because they are being trained on certain things and on those set of things they have the right kind of expected outcomes in reference to logic parts. I still feel the human mind and human brain uh works better and we have seen that across uh across number of examples.

Yeah. Just a second. Wow. Yeah, sorry uh for the hiccup. While this comes up, I hope it uh comes up. I'll definitely share. It's just going the opposite. Yeah, I'll just uh move to the next set of slides very quickly. Uh sorry for the hiccup over here. there is something seriously okay so here I'm discussing uh the security pipeline where we are doing coordination with the security team at Ethereum so essentially what we have is uh we have uh Fedric and we have the

consensus client team who are based out of London and what we have essentially done is that since we work across different implementations and across different uh modules so what we are trying to do is we are trying to ensure that it's a coordinated effort and coordinated effort what it basically means means that we use AI for doing verification, for doing auditing, for doing those set of things where uh we can reduce the overall cognitive load of our security researchers. But for many things we are still kind of uh embarking or following a very simple strategy that anyone who has a good interest or has a good experience in the deep tech understanding of infra which basically encompasses your transport layer, your identity layer, uh your messaging layer,

communication layer, routing uh system, secure communication channels which is TLS, noise and auto TLS. So someone who has deep interest on these things we are basically sharing with them that okay you kind of collaborate with us work on a module by module level try and see and understand from the existing CVE which have already been issued for the last uh I would say 7 to 8 years so we do have a good human knowledge of last 7 to 8 years and I would say the first four five years when there was no LLMs I mean even knowledge at that particular time in terms of triaging in terms of collaborating so we have that 8 to 10 years of knowledge very well developed in terms of how Ethereum security has been managed and how the DeFi security

around Ethereum has been managed. So keeping that into consideration, keeping that into perspectives and building on the learning that we have so nicely uh I would say uh documented and also made it sure uh also ensure that it is available to everyone who wishes to join. We are saying to everyone and anyone who is interested in doing intra-level security, join us, collaborate in some of these efforts, try and see and make it uh try and see on your system whether you can evolve your understanding of how things work at a distributed node level, how you can fix some of these issues and how you can ensure that peer-to-peer security really works. And this uh is one of the key learnings uh which I do

wish to share that there were a lot of members uh who when I was having coffee outside they mentioned that uh the work in AI security or AI research is now getting uh being done more by AI models and less by human beings. I personally believe it's quite the opposite uh in in reference to the infra level security. We can do a much better job uh if we have some of these models. What I essentially wish to share in reference to this case was that we use AI agents to figure out our panicking of a node. Now node panicking is like one of the things which we can easily miss. Why?

Because memory overflow and integer overflow are those cases where sometimes a human brain will say that okay these are some of the calibrations that the original author would have done and I don't have to run those kind of code checks or code traces. And unless you are a symbolic researcher, I mean unless you have built a symbolic uh system where you are doing an if else construct and you're trying to really go at that level, doing an arithmetic level overflow research is harder. So what we found is that if you are using an AI agent and you have a very basic integer overflow, you can have it fixed in one implementation that is trust and then you can have a very clear pathway through which you can share it across all the 17 implementations. So we have in total 17 implementations and the good

thing the benefit of AI is that the security team re remain as it is which means if there are like 20 contributors and 20 security researchers in the overall lipop project the core ones I'm talking about the ones who are being paid uh for doing uh the entire bug fixing maintenance code management so those members are basically coordinating faster and they are able to coordinate faster they are able to ensure that the final code race that is available I mean they are able to kind of ensure that those exploits are not uh very specific to one implementation they're also shared by other implementations why this becomes very important is that the like the attack will not come just from one

specific consensus client that is a lighthouse consensus client it can come from say like teu which is an institutional level ethereum client that uses Java lip it can come from Nimbus which is using Nim lip P2P another very interesting ing uh language it can come from loadar which is using zig lip p2p or jslip p2p. So the point is that the first part is to fix that issue but the second part is also ensuring that whether that fix has been propagated timely to the other implementations and to the other consensus clients because if one of those implementations have that integer overflow or has that specific issue then this entire exercise of using an automat uh automated uh agentic workflow system it does not reap

those kind of benefits. If one of the consensus clients is in problem say it's like one of your family members has a impact then you definitely get impacted by that. So it's the same set of things and I do wish to share uh the final uh piece over here. Sorry we had a tough time uh today but yeah uh this is the last slide. I just wish to share that uh most important thing is that if we have the AI execution done properly, if we have the AI security workflow analysis done properly that there are couple of things to learn from this one is build your triad pipeline so that it is not like let me accept AI or let me accept AI models but it is like where I need AI. I mean that is essentially the

question I would like to share with everyone. It's not the question of I want AI to use security or to do better in security. It's like where I need it and where I don't need it, I will use the regular human brain. I will use my friends and uh collaborators. I'll work with them to ensure that uh we get uh to a good conclusion to a specific issue. So these are like some of the learnings which I do wish to share. I do feel that uh many of the things which I shared in this discussion you might be feeling that hey this is uh very specific to how we work at infra uh level security for the D5 infra uh for the D5 project. Yes, definitely it is very much related to infra level security. But I also feel that it has lot of implications to what

we guys are doing at the wallet level and at the other different levels that is uh essentially your application level your D5 protocols they all are following the similar trend and some of the learnings we did from the infra layer is something which we have kind of propagated to the application layer. So in case if you are working and you are like a do-ityourself person who likes to run nodes, Ethereum nodes, likes to run validators, I would definitely like to share two things with you. That's a friendly uh like that's one of my responsibilities. One is you please upgrade your gossip sub to 0.49.4 4 which is the latest version and if you're using flutter fantastic if you're using grid topology I mean fantastic you don't have to worry but uh do uh the

same and second essentially uh is that uh you also prepare your track pipeline for the AI security swarm so essentially try and uh prepare your AI security uh swarm track pipeline and yeah uh if you have any questions uh please uh let me know and also one uh last request if anyone of you is interested in applying for an AI grant or uh for a infra level grant, please do let me know. We do have some opportunities. Would love to discuss. Thank you. >> Yeah, >> you can speak.

>> I just want to understand that you mentioned that there are multiple lines like Java, >> different implementation languages. Yeah. Yeah. Yeah. So, uh I wanted to understand that it makes sense to have a document >> which [clears throat] has the specs written out and that is verify or figure out if >> absolutely beautiful question I do wish to share. We do have specs uh it's called as lip P2P specs more than happy to share the link and I do uh uh so that is that gives a very so that's a very interesting question I mean we're working in a decentralized environment but at the same time there are points of convergence uh lip spec is the point of

convergence that's where all of us we kind of collaborate we discuss for every specific function how it has to be written or for a specific architecture how it has to be worked on for any spec that uh like for any spec proposal which is shared as an RFP or even if it shared as a PR in our specs repo. Uh so we have a very clear path of review cycle. So it's generally reviewed by all the maintainers of different implementations. We have a weekly spec meeting. Would love to uh have you join that spec meeting also. Uh we are now having it uh more often than usual because of a lot of security issues coming our way. Many of them are minor issues. Many of them are meto issues but some of them are definitely high severity issues. And uh I do wish to share that yes uh having a common spec

is one of the ways through which we can align all these uh different implementations. Yeah. Thank you. All good. Sure. Thank you. Uh we are just running short of time. So uh we'll definitely uh catch up uh outside for coffee if anyone would love to catch up. Thank you. >> Thank you. Next up we have Natalia. The talk is about from production rust to lean for proofs a verification pipeline with AI powers.

>> Hello, my name is Natalie Claus. I work at runtime verification. I'm proof engineer and today I'm going to tell you about our [snorts] uh collaboration with Ethereum Foundation. We've been working on formal verification of zero knowledge EVM. It it's ongoing project uh yeah verification project and we try to build a pipeline which translate source code to lean and we prove formally using mathematical methods that code corresponds to specifications.

Okay, as I said, it started with collaboration uh with Xeron Foundation and this is briefly uh what our pipeline does. So, step number one uh take source code Rust cryptographic uh libraries were our goal to verify or blonkey risk zero. These are uh Starks libraries, right? And step number two, translate library source code to LIN 4. You we could use any instrument. We were allowed to use any instrument which is mature enough to do such translation.

And spoiler there is no such instrument yet. They're not mature. Absolutely. Because for example, we do not support unsafe. We do not support async. We do not support low-level code. And Linux kernel is low-level code. when we have lots of uh concurrency in plon free for example but we had to try right so uh step number three specifications specifications are human written handwritten and we also use AI to write specifications but sometimes AI fail in writing specifications because they can write really often vacuous specifications which are really easy to prove and they state nothing so we prove

nothing so uh Human engineer should check each and every specification we write. And we also used arip and com poly. These are libraries for starks which were also created within this project within foundation. uh we are not the authors of these libraries but we contributed to AR liba and compoli heavily because seven months ago when this project actually started um these libraries also were not mature enough and we had to write math and we had to uh build some we had to fulfill them with bridge lemas which helped us to do verification

and final step actually writing the proofs. So, uh, production rust, we should prove mathematically that production rust matches the mathematics, right? That code actually does what it should do always for all possible inputs. Like we prove theorems in our geometry, right? That's cool. And uh, yeah. And what is in the basis of our approach? LIN lin is a prover. It's a kind of language which we can use to write code and to prove to reason about the code.

Uh so so this is a top level of our pipeline and in more no this is not right and this is more detailed specifications. So how exactly we translate code? Well actually we can play with this pipeline. We don't have to uh well let me be uh more clear. So Ra first step we take rust crate like as it is plunky free. Step number two we lower it. We use special instrument kon which translates code to mir when from mir we take llbc [clears throat]

it's intermediate representation and from llbc we can build lean definitions uh and once we have lean definitions it's uh similar that like we have mathematical model on this step when we have lin we can reason about our model we can write uh specific ifications. We can write theorems and lemurs and prove uh for example for rust code we can prove that code never panics. We can prove for C code that uh code do not have undefined behavior anywhere. And um we also can connect our lean model to specifications on arip and compy. C comp

is about polomials and finite fields. Aralip is about starks in general and comple. Uh they initially should be one in the same project but they are separated and um how we write proofs. Uh we use AI provers and we use uh engineers. Uh we also use specialized AI provers like uh Aristotle from harmonic and ALF from logical intelligence. Alf is AI prover which should work only vin and it has all math flip vin and it can do the proofs really quickly because you know

like before AI era like um 5 years ago or four years ago I had to write all these proofs myself and it was horrible amount of work. It's like digging land with your bare hands. And now with AI, we have like exoskeleton and we can walk really quickly. We can do more in shorter time. I really think that AI is something incredible. It's progress and it's unstoppable and it will help us to cross this ocean and ocean is huge actually.

So this is example of simple behavioral lema. For example, we have x and uh our function simply divides x on two and then plus one. And this is theorem. We prove this is very simple example, right? Just to show case. Uh and here we prove that uh for all possible inputs our result will be first of all it will never panic and our result always be more than zero not equal to zero and we will have such result right it will exist. So this is example of simple behavioral lema and arip and compoli as

I said we have complicated mathematics here which describe how starks how cryptography should work and our goal was to prove our lean model against these specifications simple and actually cryptography specifications. uh we targeted uh several we we tried everything we tried fry uh mercen 31 horner evaluation and here I'm showing what instruments in pipeline we use with each and every example and what actually we proved all proofs online you can check uh yeah and with one step

folding round we had the most uh interested results because we managed to connect it to arcliffe. It was not that simple because um yeah because all the instruments as I said are not mature. It was like experiment which showed that instruments are not mature. Okay. So what AIs we used during the process? Uh we used clo of course and I have to say that specialized AIS like uh we we can contribute themselves. They can do PRs.

they can uh prove. We had one interesting proof. We had to prove really complicated lema and it took like $200 and uh 24 hours it was running running. We provided it with PDF. We provided it with additional mathematics which is behind and it finally did the proof. um um alf it actually splits proof to several substeps and prove them all one by one and also um what is important here in our pipeline there are a lot of wings

things we should trust right we are talking about mathematics so we would like everything to be proved mathematically and there is nothing to trust right in our pi in our pipeline. But still we have to trust a lot of things. We have to trust translator. Ideally translator should should we should be able to prove mathematically that translator actually that a result code in lin 4 equals to initial code. And it is possible to do such proof. For example, by induction if if uh translation is correct for simple piece of code for one um piece of semantics, it would be correct by binduction for a whole big bigger piece of code. But uh

such proof uh s equality between uh translation and initial code is separate research work which should take take maybe several years. But again with AI it can be done much faster nowadays and also we should trust compiler we should verify compiler we should trust specification itself because it was human written right and all the specifications are in maintainers head so this is collaborative work verification engineers should work together with um maintainers so um yeah and as I said AI provers failed uh in some places because uh instruments which

translate code from rust to lean they are very specific. When you build such instrument, you should decide on many things. For example, what logic to contribute to? Is it separation logic? Is it many sorted logic? Also, you should decide what semantics you should use. Right? Uh and it perfectly it should be executable semantics. So we could do differential fuzzing in lean version, in C version or in rust version to prove uh not prove in mathematical sense but to show at least with fuzzing that our translation is accurate.

Um yeah uh building the pipeline was not trivial task itself because each instrument in our pipeline is having different lean versions. Uh our clip even compi they both had different version uh NES hawks different versions of LIN. So and our goal was to build it all in one and the same LIN project right. So what we did, we had to connect with all maintainers and ask them to align lean versions into one so we could build our pipeline and they were very responsive and we managed to build it.

Uh yeah and another problem we faced as I said is extraction gaps. um NES is the most mature instrument nowadays uh for uh translation from RAS to LIN but it doesn't support even unions for example uh I'm not saying about unsafe facing code so uh we decided to build translator ourself so this is the prototype of our translator to show um to show C side effects. This is for C language but approach itself

which is having several years of research behind approach itself is language agnostic. We can use it for rust, we can use it for C, we can use it for go but we are doing it for C. First prototype well first prototype was for Go and this one is for C. We do it for C because right now we're target in Linux kernel and we already found several uh bugs in Linux kernel and last one was um uh security bypass in Linux kernel isolation layer. Each and every AI works in this isolation layer uh and we found bypass it was fixed in six hours after we found it. And take a look at this translation. It's I think it's perfect

because they are almost identical. This is also result of our research. The only thing which shows that this is lin is this see done word here and there because we should exit uh free monet actually. Yeah. So to show in purely functional lin uh to show all the side effects we had to use monet. We are not able to use uh free monet because it's not enough to cover all side effects. So we're using advanced free monet and we are hiding this prototype from LLMs because we can stole the ideas. We we don't know what to do with it right now because several years of research behind and you can reproduce it with alarm

really quickly and do use this approach yourself. Uh so uh yeah we also I I described how our instrument works. We translate C code to C to JSON by C lang and then we receive Lind DSL as I said effects are covered with uh freeear monet. Yeah I think that's it. I'm almost in time. Thank you very much for your attention.

Thank you. Next up, we have Kevin. Formal verification of stake poles from general design to a real world applications. doesn't work. Okay. Uh thanks for the introduction. Uh hi everyone. My name is Kevin. I work as a formal verification researcher for is Storra. And yeah uh as was introduced uh I want to talk in the next 15 minutes about um formal verification of ST pools. I'm keeping it fairly abstract.

So I'm starting with a general design of what stake pools are. So mental model of the uh moving parts and of the one of the arguably most important envirants that stake pools should guarantee you. Um from there on I'm going to go to a concrete implementation that we formally verified at Sattorra. And the outcome of this firmware verification was that we found a security bug, a high severity one that was lingering around for a couple of years and survived multiple audits. Okay. Uh let me Well, okay. And there we go. Um, yeah. So, first a quick primer on what's what I mean by stake pools. I think the concept is pretty simple. Uh, say you have some assets and you want to

stake them, but you don't want to go to a single validator directly. So, you can go to a stake pool and it much like behaves like a uh like a standard wault. So, users deposit their assets into the stake pool, they land in a reserve and the stake pool um means back shares proportional to whatever you deposited into it. Um, but then on top of that, there's some kind of operator that moves the funds out of the pool uh to one or multiple validators where they can experience slashing, but hopefully they only earn uh rewards. So, at the later point in time, users can redeem their shares and get back hopefully more than what they put into the pool in the first place. So, that's a uh that's the

general idea of stake pools. Um and whenever we see something that resembles vaults in any shape, what we tend to prove is or what we try to verify is an variant called solvency. Um so what this means basically is that the shares that are issued at the moment these are always less than or equal to the extractable value and in the case of stake pools that is um whatever is in cash in the reserve plus uh the current value at the validators that is staked. So including the rewards um we ignore uh slashing because that's the only exception that can break solvency. So for for that invariant we simply ignore it. And so what this says is uh if everybody was to redeem their shares at once now at the same time then there

would be enough value in the pool to honor every share. Uh we tend to prove this uh because it um it covers many classes of bucks at once. So for example, if you mint too many shares on on a deposit uh due to a rounding issue or some kind of fee setup that is that is not correct uh then you will probably find this as an v violation to solveny. Same for uh pay payouts or for a state that can where the internal accounting can drift from the onchain state. So we have this solveny the invariance and invariance here means that we want to make sure that the pool um u satisfies this at every uh reachable state. So the principle or the technique that you can use to verify this uh is

called induction and this thing doesn't work. Oh there we go. Um so what you do is um okay uh you prove first that the solveny invariant holds uh whenever you create a new pool. So on a freshly created pool solveny needs needs to hold and then what you prove in the next step is for every uh state mutating function or operation or outside event you take a solvent pool. So you take any pool that is in a solvent state you execute that function and you assert or you verify that the the pool is still in a solvent state afterwards. And if you can do this for any operation and any outside state change. So for example airdrops um then you can be guaranteed that the pool is

um solvent in every state. And you can use your favorite formal verification framework of your liking uh to prove this. For example, you can use the approach with an that was described in the talk before that. Um you can also use fuzzing if you don't want full guarantees. Uh in the example that I'm going to show next what we use is the Storana prover. And in a nutshell, you give it the environment and the code and it comes up with a logical formula that can either be proven making sure or guaranteeing the property holds uh or it gives you a counter example telling you where solveny can be violated.

Okay. So we proved this particular environment for the Solana stake poolool program. Uh that's the standard stake pool program on Solana. It's running since 2021. Um 2 weeks ago there were about 64 active pools. Uh they together had uh 33.1 million soul uh locked and um there was roughly 3.4 billion uh USD so quite a lot and it was audited a couple of times since it was deployed and last year we also formally verified it.

So first how does the Solana ST pool program work? Okay. Uh okay, there we go. Um so it's more or less the same thing uh as the general model. Uh we have users that deposit soul into the stake pool. Um so this was supposed to be an animation. Now I see the whole thing now. Um and the pool uh mins back what's called pool tokens which is nothing different than the shares we saw in the general model. Um then an operator uh the staker comes into play that takes that takes tokens out of the soul out of the reserve puts them to the validators. They land first in the transient stake. There's kind of a buffer because on Salana ST can only enter validators upon epoch boundary. So after an epoch ends, the stake is moved

to the validators active stake where it gains rewards. If the users want to redeem their shares, uh they go back to the pool um redeem their shares, they get burnt and the stake pool uh moves sold back to the user uh what for whatever these shares are worth at the moment. uh what you have to care about is if the reserve has less than some kind of set minimum value. Um this is kind of value that is never supposed to be um um like uh that's always supposed to be withheld in the reserve. So if you if there are not enough funds to fulfill a redemption uh then either you have to wait until other users top up the reserve or the staker comes in and unstake something so

the pool has enough funds available at the next epoch. So we tried to prove uh solvency on that uh particular uh protocol and in that case it's simply like restated that the pool tokens are less than or equal to the extractable value. So the pool tokens are the shares and the extractable value in that case is the whatever is in the reserve minus this minimum balance that I said cannot be touched. uh plus whatever is staked in the validators including the reserve we have already gotten uh the the rewards we have already gotten plus what is in the transient ST. So we were able to prove this but there was a catch uh that we had to assume something about the reserve which sounds a bit ridiculous at

first if you have never like got in touch with the Solana um system which is that the pool can actually move around uh the soul that is in in the accounts so in the reserve and in the stake accounts. Um what this is or why we need this is a is like a regularity of the Solana runtime because on Salana um every every account so every piece of structured data um that is stored has one owner program and that owner program is the only one that can move actually soul out of that account. So in case of the stake pools uh the reserve uh the owner program of that reserve was not actually the pool itself but it was what is called the stake program which is a

Solana native program which is out of scope of the pools or the pools are built on top of that. Well the users interact with the pool. So how does it work? Um, the users go to the pool and they say they want to redeem some shares and the stake pool then goes to the stake program, signs a request for the stake program to move some soul out of that reserve and the stake program then checks the authority. That's another field on that account that is set to the address of that stake pool program and the stake program checks who signed the request and if that is the stake pool program then that request is is carried out. So it's granted.

Um yes. So this is why we needed this assumption. So in other words, what we needed to prove is um that the pool at all times is the authority of the reserve and the validator and the transit stake. Um if you look at the code, this looks like a completely reasonable assumption. Um because you know that authority is set once and then never touched. But it is actually violated. We could not verify this. And here's what could happen. So this is going to be hard to explain now, okay? Because the animations don't work. So um if the user wants, say you have a reserve that has 20 soul, uh so it know shows 0 something something. So it's supposed to be 20 and the user

there's some user that can withdraw that 20 soul because he has enough pool tokens. So it goes to the stake pool program um asking to withdraw the the 20 soul by giving it the pool tokens. And uh so the stake pool program goes to the stake program asking the stake program to on behalf of the user move out that 20 soul and give that 20 soul to the user. The stake program sees that the authority is properly set to the stake pool as it should be uh presented here. But um yeah the [clears throat] stake program then moves the 20 soul from uh the stake problem moves the 20 soul from the reserve to the user. After that has happened, the reserve technically drops to zero soul. And what the stake program then does is it moves the state of the

reserve to uninitialized. So if whenever the stake program sees a reserve dropping to zero, it just moves it to an uninitialized state. And uh even worse after the transaction ended, so when it sets it to an initialized state, um at the same time the authority is set to none. So the stake pool is not the authority anymore of that reserve. And even [clears throat] worse for an account that has zero soul or has sold below a certain rent minimum threshold at the end of the transaction that account gets deleted from the runtime. So the reserve completely vanishes and everything that flows into that reserve by for example unstaking from the validators cannot be accessed anymore.

uh that in itself is is bad enough but it compounds with a different issue which is that um the stake program can actually reinitialize accounts uh before the transaction ends. So this is what this picture here uh presents because if we have a malicious user uh the user itself can uh transfer a minimum value so very small value back to the reserve and um you know then it's refunded it won't get deleted and in the same transaction go to the stake program asking the stake program hey can you reinitialize that account and the only thing that the stake program does is check if it's an uninitialized account.

Uh it sees the uninitialized account because we withdraw all of the soul. So the stake program will happily carry out that request and the user can put himself in place of the authority. So now every funds funding every deposit that goes into that reserve or everything that goes from the validators that gets unstaked into that reserve is now under complete control of uh this user. So that's a very nasty state to be in. Um let's check why this happened. Uh if you remember back I told you that there's supposed to be some kind of minimum value always kept in the reserve.

Um that was good intention but it wasn't properly enforced. Um because there was a check in place that only checked if you withdraw something that at that moment there is more than that minimum balance in the vault. What was not checked is that if you reser if you uh withdraw something then after you carry out that withdrawal um there's still more than that minimum balance left in the in the reserve and that minimum value of course needs to be greater than zero. So the fix was very simple which was to put back or put in that exact check that if you redeem shares and you withdraw the funds from the reserve then there's still more than that minimum balance minimum balance. So once that fix was uh put in which was very like very few lines of code uh we

could prove this invariant. So there was no other counter example to to this invariant uh meaning that it's it's fully proven now and all of the other assumptions that we needed for solvency which I left out in this talk were also proven fully verified and solveny itself was verified um at that moment we were guaranteed that um or we have verified that solvency holds for this Solana stake poolool program. So, quick recap. Quick recap. What we what we've seen is that we found a high severity security bug that allows a user to completely take over the funds of a stake pool um just by violating an implicit assumption that the um account that the pool itself could always move

the funds around. And the cause was fixed or the issue was fixed by a very simple missing check on the minimum balance. So um the key takeaways that I you know think this this shows is that check your implicit assumptions because if you looked at the codebase you wouldn't see that this thing that account removal dropping to zero. This doesn't this does happen outside of the code base of the of the state pools and within uh the runtime itself. And also ideally um do complement your audits with formal verification because formal verification makes you or forces you to make your implicit assumptions explicit because you have to list them in order to prove other invariance. So

once you do that you wonder oh is this really true and you can also like we did in this case uh verify those assumptions uh individually independently and you know in some some cases like in this one you get um unexpected results. Um yeah this is all I have. Uh thank you. I don't think we have time for questions but you can catch me afterwards. Thanks. Thank you. Next up we we have Lilian proving the spoke formal verification of a vforce hub and spoke architecture.

Hello everyone. I'm Liam. I'm working for central I'm doing I do security and for verification for more than a year and a half and if approved by the governance um custom spokes can integrated within share liquidity apps um on a before. So the idea of this talk is to give you an overview of what we formally proved on a and what you should formally prove if

you want to develop your custom sparks and maybe have it integrated one day within the architecture. Uh so let's start where we left last year. If you were there last year in GSS Buenos and you saw the other exot presented by dee from a team and to general from previous this one was about the abs why the architecture why this design or the math works or winding can drift and one headline property the share weight can never go down it finished and I promise um on the properties exist you can check the news box again them so some numbers uh to get your attention are Pro of course is live

uh on multiple networks. It has more than 1.4 billions uh dollars supplied and more than 450 millions dollars borrowed. So it's big and let's see how it works. First at the bottom we have the EBS. The EBS hold the liquidity and the share mat accounting with a separate set of books per assets. UPS are similar to vaults and um and it caps what each spokes can add and can draw. So the draw caps is a spokes credit line. Then we have spokes.

Spokes are similar to markets with our own oracle prices with parameters and user position. Then we have users. Users only interact uh to to spoke uh via simple calls like supply, withdraw, repay. And finally we can have custom sparks that can plug in and reuse the liquidity that they already deserve. Babylon sparks which is a custom spark external to should be the first one if the approval is accepted. It's a basically a landing market for bitcoin vault collateral that draws on liquidity instead of bootstrapping its own.

So um the question for the rest of the talk is what does the spokes have to guarantee and what does the guarantees back? But before the properties, let's see where the state lives. On the left you have what this what the ES stores per assets. So liquidity, shares, index and premium accountings. And underneath it you have um the per spoke slice which is what the ELS believe each individual spoke is holding. On the right you have what the spokes basically stores position per user per reserve. Each spokes has its own storage of course because they have different contracts.

They are just connected or link to the same. Uh and by the way a spokes can be connected to multiple EBS. But um but spokes here are connected to the same EB sharing the liquidity which makes this architecture so powerful. And one things really important on this slide is that um um the the the agreements between her and as sprocks because a spork only ever sees per total spokes. It never sees user position. So the property linking her and a sprock um is is a property sorry the agreement between her and a spoke is a property linking per spokes total up per spokes total to spokes per

user position which has to be formally proved. So let's have a look on what we proved on the app. The first property that was already discussed last year as I said is the share weight only goes up. So total assets over total shares never decreased after any function. The second properties is that the app stays solvent. So total asset cover total shares. What do we mean is that we verify here that the share weight is always at least one. Property number three no spokes all shares the app as in code. So here we verify that every spoke shares s to the epstos and property number four this is a property that makes a custom spokes attractable piece of work at all in terms of formal verification uh because we formally

verified that if that one spokes cannot to another basically so let's zoom on this force property and have a look at what does it looks like from a cert verification language CVL point of view the idea of this no change to the spokes rule is to have this f here which is parametric meaning it can be any function. So we make sure that no matter the function call on the up from a sprock um the state stays the same for a spoke that is different one than the one we target. So whatever [snorts] spoke A does on the EBS um doesn't uh is it cannot add to spoke B's depth depth it cannot shrink spoke B shares and cannot

add spoke A cannot add to spoke B deficit and the table on the right is the idea in one picture for example we have spoke A sorry there there should have been animation but but here we are and the idea is that spoke A borrows is it one shells goes for 100 to 140 And we formally verified that for spoke B and spoke C it stays the same. [snorts] So as I said this is a property that lets a sprock be added without reiting the ones already deployed because if you develop your custom spokes you have the formal instrument that even when added to a new to a it won't be touched by another one.

So that was the upside. Let's have a look on what we prove on the spark. On the spokes we have five families. Family number one is user resolution and accounting integrity. Uh by user isolation here what do we mean is that we verify that if your balance with an hour change it means that you or position manager your approved makes the call and there is an exception here. I let the security researcher in the room guess what's the exception for user isolation. And about non-zero change here we wanted to verify that whatever a user gets it means a non-zero cost come with it. So for example if shares are minted from our protocol we verified that tokens went in. If token are going

out from the protocol it means that either shares were burned or debt was added. And if debt goes down for an account it means that tokens went in. And here again there is an exception. It's due to woundings. Of course, we all know that. But for wounding, we verify that it's never under shells token or debt will live for free. So basically, we verify that woundings is always in the protocol favor. Going back to isolation, here's the exception. You may have guessed that it's it's liquidation. Uh it's well known and has its own family. So it's we will get into it soon. On family number two is spark up consistency.

Um, as a reminder here, the ABS only ever sees one total per sprock. It doesn't see user position. So, um, it relies on the sparks own per user books to decide who may borrow or not. And if those books drifts from what the EPS believes each individual spokes has, it means that um, liquidity can live against positions that do not exist. And this loss would lands on users that never interacted with with this spokes. So that's the reason we have this this family to prove that there is a consistency between spokes and the proof we built to prove a spoke up consistency as three piece. The first piece is a

ghost. A ghost is a running total the prover keeps which is not part of the contract. The second piece of the proof is a hook. A hook as its name suggest is um triggers on every right to drone shares. So on every SS on the codes to drone shares here anywhere in the codes it will keep it it is triggered and the the goal of this hook is to keep the ghost variable we just define up to date and this includes a path that nobody saw to test. That's why this kind of properties is a good is a really good fit for formal verification. And piece number three is the envirant itself that the total equals of the record for the spokes between the spoke and the app. Um

here this environment is proved by indiction meaning it's it's true after deployment and preserved by every call. Again here the exception is liquidation but liquidation sits kind of outside this uh this family this family and as its own family and um and as I said this tree proof pattern uh can be can be useful for other variables like gr shares shares and premier shares and offsets but here the idea for um for drone shares between the spoke and the abs was to prove that they matches exactly because a missing share will be debt nobody owes and an extra one will be debt nobody can repay

family number three is else factor basically when you have a lending protocol you want to make sure that uh no perian lower without a checks so that's what we did and in addition we verify that an account can only move back up and what was interesting is there is that for the function that skip the lakes we verify that they can only add collateral or reduce depths Family number four, position her hair variance. Here we verify that a position never takes a shape the protocol cannot handle. So kind of obvious things but kind of hard to verify for manual audits or LM audits that the depth there is no depth without collateral. The borrowing flags always matches actual depth and there is no balance in a reserve that

does not exist because all the states will make all the downstream calculation meaningless. So what we did is that we rolled them out once as them variance and uh and yeah again this is kind of property that is really good fit for FV and family number five finally uh liquidation here the main goal was to verify that only an NLC account can be liquidated in addition with a fate properties like if the liquidator um receives collateral it means the brewer dep goes down cure and bodies stay bound and there is no uninvolved account between during the liquidation and no bad depth is wide enough while the borrower still has collateral.

These five families of rules we proved on the sparks represent around 60 rules and every one of them called the so the question is if you develop your custom sparks do we need to reprove the app each time because when we when we tried that we had to face the challenge of trying to prove to be cut because the on the spot is ob is obviously a big piece of code and for that uh the answer is no we don't have to reprove the ELS because when we face that we had to use what we call modular verification and for that we created what we call a symbolic so let's have a look at the symbolic app

the idea of this part is that you as I said you don't verify a system this big in one piece you split it that's modular verification and modular verification can be achieved in three steps [clears throat] the first steps is that you prove each component on its own for example for the share weight solveny perpox same isolation properties were proved once uh with no spokes involved. So they were really proved on their own system. The second steps is that your proof become a so when when we we first created the symbolic app.specs we define some variable on it that was that were important for for us like the share to asset ghost variable. Uh a ghost variable is a variable that we let free

meaning it can take any values but on these values we assume two behaviors that we already proved on the abs uh that are the share weight only goes ups and it never drops below one. Those are properties from a few slide ago that we verified on the EPS and that we know that they hold. So at the end we have a free variable which establish the the thes war guarantees that we already verified and share to it is an example. We can define other variable like for example depth index can get the same treatments and and that's proof number two.

Basically the proof become axiom and the aum is what you assume uh that you already proved on the app. Step number three is that you summarize every every call. Uh so when you want to verify something about the spoke about your custom spokes what you do is that you replace every calls the spoke makes by a few line of CVL running through the go variable which establish the behaviors. So at the end the sprock is proved against what the apps guarantee which is strong which is mostly cheaper and easier to prove for the central approver not against one version of its code. And on top of that what's nice is that if you develop your custom spokes you can

reuse this symbolic uh file.spec you can import it on your project and uh and the formal verification part of your custom spokes will be a lot cheaper. So if you want to develop your custom spokes, I hope I convince you. Um there are three steps. The first steps is that you import the shared model symbolic mat summaries present such models. Everything is available on our report. Uh second is that you prove the checklist your custom spokes uh will can be proved [snorts] against five families which represent around 60 rules and a variance. And this is important that you reprove them because I described what an spokes guarantee. And finally um step number

three is that you write rules only for what you change. For example, Babylon will liquidate a BTC vault which is different than other box does. So it's a new behavior meaning you have to develop new rules and for that we can help etc of course on this process. So at the end the answer to how much for modification work is a custom spokes is only the different not the wall which makes everything a lot easier. Thank you very much. Thank you. Next up we have Peter. The

talk is about formal verification in the age of AI. New powers, new traps. >> Okay. Yes. >> Thank you so much. >> This one is >> what? >> Okay. Hello, my name is Peter and I'm the lead uh protocol engineer at Spectra, which is a yield derivatives protocol.

Okay, today I'm here to talk to you about how we are changing our development processes in this age of AI and especially in critical software and I will do this through the talk about formal verification. So this will not be a course about formal verification. Although there are a few things I would like you to retain from this talk and first is a practical understanding on how to use formal verification in the use case of smart contracts.

Uh secondly because my experiment involved an enchanting setup. I know a lot of people are recently interested in that. So you can check it out. And uh lastly the and most importantly the answer to our question today is what are the limits of using AI for former verification. So recently formal verification made quite a lot of buzz and some quite influential people started mentioning it really frequently like Vitalic Buterine. But it seems that a lot of people have understood for modification as some sort of solution to vibe coding. uh some sort of magic tool that that makes your code that was untrusted

suddenly trusted which brought me to think about the two questions written here which is how do we adapt our processes to build safer software today in the age of AI and if AI writes the code can formal verification give enough confidence for my experiment I picked a few cases and today I will present the one that I think is the most interesting one and it involves the inflation attack and uh the trick I used to kind of obuscate the the finding because it's such a popular attack. I'm sure that uh the agents had it already in their data sets. So what I used to a bit trick them is that I solve

it kind of partially. We use the virtual shares which makes the attack nonprofitable for a single victim but without putting any decimal offset. The attack the attacker can still profit if there are more depositors. Yeah. So a bit of terminology for formal verification. You have informal and you have formal specs. So what are informal specs? Those are in plain English defined properties and invariance about your code. And for example for the inflation attack, one could state that a

successful deposit gives shares worth at least what was paid minus a small tolerance. What does that mean in practice? In solid plain solidity, it would be that a deposit and a redeem in the same transaction should return more or less the same amount minus some roundings or some fees. And here below you have the formal claim which is the same property just translated into a more formal statement. And this is what CVL for example looks like in the case of uh Certora which I used here uh because it's the most widely used tool right now for formal verification on smart contracts although there are many other uh and emerging

like varity so I want you to check them all out and here is the pipeline for formal verification in short so you write your code you write the informal specs in English and then you translate them to the formal specs which is the CVL. Then you write some modeling and assumptions and you feed that to the solver which will then return the outcome which is either a green pass that the rules are verified or a counter example.

So we must not forget that AI and LLMs are probabilistic algorithms and that uh never mind how good the results are and smart it looks, you still cannot predict the outcome and most importantly you cannot explain it. You cannot explain why an LMM did a mistake. So this invites us to reason about what steps you should overlook and which which could you trust more that it does.

And here are a list of uh things that I believe LLMs do greatly regarding formal verification. So I use it a lot to understand even my own system to brainstorm more invariance and properties. And um the second thing uh about writing informal specification, I don't let it write completely uh informal properties, but I use it a lot to brainstorm new ones. And uh the third point uh a really useful trick is uh if you didn't already put on paper your properties um you can check your own tests and you can ask the LLM to infer them because most commonly you already thought about

the properties at least implicitly. Then what I believe the LM is really good at it's to translate your properties into formal rules. Although this step also should be carefully reviewed because sometimes the the CVL doesn't correspond really to the to the property you're intended. Then of course it's really good at doing all the boiler plate work and running your proofs and it can help you also understand the outcome. For example, a counter example.

Now we saw how LLMs can help you to do formal verification but what are the its limits? So for my experiment I used a real production code just with a inserted vulnerability and uh the agent's task was really straightforward. It was to find bugs. it was to write first some properties informal specs and then to try to catch them using either testing or formal verification.

So the test involved six completely independent agenting runs with the same instruction just a different starting point and a different tooling to resolve to. So for example, the first group had no documentation at all. The agent was given only the pure raw code and its task was to infer informal specifications and to find bugs. The second batch had uh a simple readme. It's the traditional readmi with the behavior defined of the code and some properties. And the last group had uh the same readme plus some deep

handwritten uh explicit properties and invariance. And the one group had to resort to foundry testing and one to CVL and we compared then how did they perform. So here is a summary of the workflow I used. It's not really relevant for the experiment but I know people are interested in. So if you want to you can check it out on my GitHub. Uh the important thing to remember is that I made a setup so that the agents context is completely isolated. They were completely unaware of the experiment and the intended uh outputs and the agent used was the opus 5.5 which is a frontier model.

Now the two hypothesis I had that I expected was that AI will struggle to define the right security specifications on its own but is really useful at translating from the informal specs to the formal ones. Also that formal verification gives a different coverage compared to testing and fuzzing. But I missed a really important idea that turned out to be the most interesting uh finding of this experiment and that's the interpretation of the output. Uh in fact, none of the agents didn't state clearly that the that the attacker could be profitable.

All of them recognized that there was an issue related to the donation mechanism and uh they also proposed a patch which was effective enough but none of them stated clearly that there was that the attacker could be profitable which gives the vulnerability a whole other severity level. It could be it could as well be just a coincidence that the patch also covered the the severe case. It only appeared after a few prompts to recheck and uh be certain that there is no um real uh danger in that in that sense. Yeah. So another interesting u thing we saw is that with

better specs we received a better tests and better coverage. For example, uh just the readme, the agent stated the property that the shay should always be positive, which is nice, but it covers only the most extreme case where the shares round down to zero, which it can round down, not completely to zero, but still occur some loss. Yeah, the bed requirements improve the tests, but not the economic interpretation. Still I didn't observe the agents say explicitly that this is a severe uh vulnerability where the attacker could be profitable.

So did formal verification in this case uh um cover and uncover more bugs? No. And uh in fact even we had we observed some weaknesses where the human intervention was necessary like we had some impossible states that were wrongly interpreted. We had some uh uh mistakes made during u trying to make the proofs pass because if you use heavy mathematics like uh multiplication and division, often the proofs can uh can time out and you need to resolve to some techniques like to simplify the proofs, divide them or to um simplify the the models.

Although uh and the really power of formal verification is that once the check returns green, you're sure that under those assumptions the the cases are covered and the code is safe. So a bit more about the first um issue that we had is that uh proof can return a counter example because really the property is violated. But it can also be violated simply because the state it set up was not even not possible. For example, here we had the the wrapper contain more assets than it had minted

shares. And of course then the ratio will run down to zero but it is not a possible state. Uh during the the agent when he tried to make the proof pass also we observed he did some simplifications that removed the cases where the bud could be located. Yeah. For example, in the previous case, it put assumption that the assets in the wrapper are equal the supply which made the the bug hidden.

Now, more importantly, where did formalification prove itself worth it is that it forced the agent to find a fix that really solved completely the bug. because the in other cases the solution by the agent was to bring up the decimal offsets which is an economic uh solution to the bug. It makes the attack very expensive but in fact not completely solved. The prover still would complain. While the one that the agent did that had to use for modification, it found a fix that made them mathematically impossible this type of uh error by internally tracking the assets deposited

which is a solution of a better quality. So what can we take out from here? How do we adapt today our development processes? So the old school way to in development was to do first specs, write down your properties, do the implementation, do some testing, then do more some cycles, fuzzing, integration tests, audits and optional formal verification if you have the budget and the resources because it was really difficult. But today the implementation cycle is really quick.

So you should do more iterations and in my opinion spend a lot more time on the specs and now formal verification in my opinion should be part of the testing pipeline because as you saw it's quite doable. Now the key takeaways from today is you should do a lot more specs. You should spend more time brainstorming the invariance, thinking about your designs, the economic guarantees. Then you should maintain your spec, go through them again and again and edit if needed. And um it should be the cornerstone of your of your system. It should be the hardest thing to bend. AI often can adapt tests

so they fit the implementation and your specs should be completely out of the equation. And um the tools for modification is a really powerful tool. But the main thing is to maintain your properties and invariance. And uh that way even you can find interesting bugs using using uh standard uh and already very known techniques like fuzzing and unit tests. Although formal verification really does provide some really important properties when uh verifying your code.

Thank you. Thank you. Next up we have Gustavo. The talk is about we gave AI the keys to our CI then we tried to hack it. Hello everyone. I am Gustavo and

this is the talk that I'm going to do. Let's see if this is changing. All right. Nope. Yeah, this is the one I'm pressing. Okay, thank you. >> Yeah, so I'm going to talk about uh how we built uh our current agentic systems at the security engineering team at Polygon to keep up with the engineering and how we attacked them to uncover some vulnerabilities.

Uh yep, so I am Gustavo, a senior security engineer at Polygon Labs. I have a heavy engineering background like offensive security engineer and today I build and break a lot of agents and this is basically my all my work. So how we begin all the agentic work that we are doing today there uh our first problem was traing bug bounties. So we built this this guy called it Yonos and we were getting like 200 something reports every month since the beginning of the year because of AI. Everyone is using AI reporting a lot of things.

This are weird. Yeah. So we have today three models that judges every report that come and the findings go to their own team to handle accept and do the fix if needed and a human makes the final call whether the vulnerability gets accepted or not. [clears throat] So we needed to keep up with the engineering team and not only with the bug bounty reports and the engineering was scaling pretty well and pretty quick. they move it from just having cloud or codeex or anything on their CLI to cloud uh agents.

Uh their work today is mostly done from Slack. They have 200 plus uh pull requests done every week which is almost impossible to keep up and audit manually and they are review all the p requests but we still have some humans that does the final call on them. So about this we have a blog post on the polygon engineering blog uh from Don Faler which is the responsible for scaling with the engineering.

So the security team also needed to scale and our one agent that we had on the beginning of the year became a fleet of agents. We have Janos for bug bounty reports. Triaging we have Spectre there is our internal red team uh agent that hunts for vulnerabilities every day every time and validates these bugs and propose a fix if they are found. We have app auditor which is a self-s server uh audit uh app that can trigger security audits from Slack uh build threat models every day and also uh audit some some

some repositories that are critical every single day. And from that we went to the 17 security agents that we have today running every day at Polyon Labs. Uh doing uh threat models uh alerting from uh triaging alerts for us doing machine checks like we have we own every machine at Polygon and we check for patches and everything and also doing security audits not only from app auditor but a lot of those agents are doing security audits on other repositories.

And we to make this secure we build for a compromised agent. Uh inputs they are data. We never input commands on the agents. Uh we only have right access where is strictly needed. Uh sandbox everything of course and dangerous actions also need to be triggered on the final for by humans. And we don't let the or at least we try to not let the agents socially engineer the employees of Polygon Labs. So we don't tag people or car links from the output of the agents.

Uh so yeah [clears throat] we assume that every agent is compromised. We threat model them and then we attack them ourselves. And how do we attack it? uh the agents before uh firing the first payload to any agent. We map every read and write that we have with threat model them with our own tailor skills uh that we have in house. uh we fire the payloads that we uh tailor for each agent and for this we use promptful uh some AI uh libraries and things that we gather every day from our own agents.

So what the models did well when we attacked them they check it the cited s sources they spotted a lot of injections they asked before uh writes and some agents detected and cited attacks that were made and logged by other agents. There was one special attack that we did and got through. We uh in did an injection of this footer on a message that was sent to a agent and so it got this text and it it bypassed uh some checks and went through the other agents and this could be used it

to poison not to attack this agent specifically but also to poison the other agents that we have in fleet and scale for more critical attack. Uh, and how we fix this, we fix this not on the model because the models usually detect well the prompting injection injections and things that we have today. Oppus, GLM, the other models, they are like pretty good on that. But we need to fix this on the the infrastructure and on the pipeline. So we tag data uh and the agents now know that this output is coming from another agent and not from a human or trusted source and I brought finally a case

study of a attack that we did on internal agent from the engineering team. This is Jio. It was kind of the first uh cloud uh solution that we did where you input uh uh a prompt in plain English and the output is a pull request. Uh it had its own sandbox and a web app and you could trigger them from from Jio on Slack. Every session is open to the whole org because we wanted everything full transparent. So every engineer could see what everyone is prompting and it was the first version of what he used today that is referenced on that

blog post from the feler. Today it's on Slack as well but we don't use this bot anymore but it was fun when we were using it. And to attack Jio we needed to ask a different question. Every session was holding its own g credential and the question was can I become an engineer and push code without anyone noticing because everything was transparent. So of course I can write code but can I write code impersonating another engineer and not being detected and yes we could because every session also has a shell on that on that system. So we open it uh on the web browser or on the

on the slack and every session new newly created session made a shell on a machine to do the pull request and this is what we attacked. So the five steps that we did to get the shell from other people were list every running session which was plainly easy because everything was transparent. get auto added as a member which also happened uh instantaneously and subscribed over the websocket that was exposed and we when we subscribed to the websocket we received a terminal token that was uh decrypted and we could open

the shell that was accessed uh to access that machine directly and not through the the solution that they And so this is the chain that we did uh on HTTP requests. We subscribed it. We opened the the open socket session and from that we were able to just SSH on the machine and write anything and everything that was written there were was uh opening up a request on the name of the engineer that was using the solution.

Cool. Video play. There is a video. >> Can you play the video that is embedded on the Yeah, >> no worries if you can.

>> Okay, we can play the demo video, but it's the same thing but showing exactly the steps and getting the shell and doing some nasty stuff there. So with this attack and this anal the analysis of the scenario in Jio and everything that we learned today uh was the model refusals are not a security boundary. So uh most of the models today uh refuses a lot of prompt injections uh in general but there is a lot of other security boundaries like that SSH token or other things that we can do to like access the agent work for from other channels and the agent output is

never to be trusted and the worst bug on that was the plane access control not something on the agent itself and the attack uh against the the agents are done every day after any change. So as I said we have 17 agents only on the security teams not counting all the other agents that the engineering are using and every time we see a change on the code that handles that agent we fire the same attacks to check again uh if they are vulnerable to this kind of attack not only prompt injections but also attacks on other channels as well.

And that's it. Thank you. If you have any questions, you can contact me at Gutra on Telegram. And that's it. >> Yes. That's all for the day. Thank you for being great audience. Have a great evening. Meet you all tomorrow.