New Ethereum talks, every Monday. The week's conference uploads by event, in your inbox.

Demystifying Smart Contract Security: Facts & Fallacies

Devcon 7 SEASat, Nov 16, 2024, 11:05 AM · 56:26

Smart contract security is of critical importance as the Ethereum ecosystem rapidly expands across different infrastructures & applications. However, there exist serious gaps and misconceptions about security as it relates to smart contract design, development, validation, tooling, offchain components, audits, bug bounties, monitoring & incident response. This panel brings together six recognized researchers within the Ethereum security ecosystem to help demystify facts from fallacies.

Transcript

All right, GM, last day, last session, good to see you all. So this is, hopefully this will be worth your time. We will kick off with, you know, a quick round of introductions. I'll start. So I'm Rajiv, I'm the founder of Securium.

Securium started about three years ago with the mission to scale Ethereum security. And we have been doing it in a couple of ways with the bootcamp, the online bootcamp, with which we have onboarded hopefully hundreds of security researchers into the space in a variety of ways. And also, we are the Trustex event, which is a dedicated event to Ethereum security, all layers of the stack. So that's Securium. And I'm also a security researcher.

Been doing security research all my life. Web 3.0 Ethereum security for the last six to eight years. And most recently recently as a lead security researcher with Spearbit Cantina. So that's me and we'll pass it on to Hari.

Hi, I just want to add Rajiv is very humble here he said hundreds of researchers, it's probably thousands. So my name is Hari, I'm one of the founders and the CEO of Spearbit and Cantina. We are an end-to-end security platform. We work with companies like Uniswap, Coinbase, Optimism, you name it. I used to build a sort of decompiler at the Ethereum Foundation before, and our founding team has a lot of experience building software that where there is like zero tolerance to mistakes.

Hey, I'm Joslin. I'm the engineering director of the blockchain team at Trade of Bits. We are a company where we specialize in high-end security technology from blockchain to application security or cryptography. We spend also a lot of time building tools. You might know Slitter, Medusa, or Echina, which are all smart contracts, or bug finders.

Hello, yeah, I'm Matthias. I'm a managing partner and co-founder at Chain Security. So we focus on complex audits of DeFi projects and many, many others around that. I'm very happy also to be here. This is with the fellow ones because the Ethereum ecosystem of all the time has been great on, like, joining people and working together.

On our end, we have been doing this also for quite some time together with Ethereum Foundation. With some bug reports, you might find us there on the Ethereum leaderboard. Hey, everyone. My name is Mehdi, co-founder and director of Sigma Prime. We are a blockchain security and research firm, have been operating in the space since 2016, turned eight years old last week.

We provide security assessment services to Web3 projects exclusively, do a lot of smart contract security reviews, but we're also very comfortable diving deeper into the stack, doing a lot of L1 and L2 security assessments. That's kind of half of what we do. We also do a bunch of research, and one project that I'm sure speaks to at least some of you here is Lighthouse. Lighthouse is an Ethereum consensus client. It's currently responsible for about a third of the Ethereum mainnet.

Very thrilled to be here amongst these esteemed professionals and can't wait to get into the weeds of it. Thank you. I'm Uli Sagiv. I'm academic in computer science in the area of static program analysis. I contribute with algorithms which are now integrated into Microsoft device driver verification.

I am also co-founder of DeFi Security Summit and CELTOA. CERTOA will be six years old on Monday. We have developed this during this time three things. We have this language called CVL which is extension of solidity for formally specifying code. We have used it to actually write formal specification for many of the DeFi manually important and also we have developed sophisticated static analysis that convert the program into mathematical formula all of this will be open source actually soon I'm really really excited to be here among the distinguished colleague actually I have was not when I started this domain at zero knowledge in security and X and and smart contract and thank you all for teaching me I've learned a lot and I'm looking forward to learn more.

Amazing. So welcome, everyone. So the title of the panel, as you see, is really broad, right? It's Demystifying Smart Contract Security, Facts and Fallacies. So we thought we'll keep it...

I mean, a lot of the panel discussions get sort of repetitive in the format, so we thought we'll keep this a bit interesting, maybe a different style. So what we're going to do is I'm going to pose one statement, very sort of a short statement with maybe a brief context to each of the panelists and they're going to react to it by saying, okay, do they believe it's a fact or a fallacy? And they're going to justify it with their opinions. And then we'll have any of the other panelists either rebut that with their opinions or agree to that, right? So we want to keep things interesting.

I mean, smart contract security, there are a lot of these things, as you see, which are not black or white, right? So they're sort of in the gray area. So we hope to touch upon those topics. But we would also like to leave a good 10 minutes at the end of the panel for the audience. It won't be more of a Q&A, but we would request the audience, I think, to scan that QR code, maybe now or at the very end, and pose similar statements, right, which you believe as a fact or fallacy and you would like the panelists to, you know, react to it, right?

So we want that to happen. So let's sort of level set and see if anyone on this panel or otherwise thinks this. Smart contract security is a solved problem. So there are really no gaps or misconceptions, and this panel is really irrelevant. We shouldn't even be here.

Does anybody think this is a fact? Hopefully none of us here. Anyone in the audience? Okay. If there was, you know, if you think so, please reach out to me and we'll, if you can convince us, we'll have you on the next panel.

All right. So let's get into it, right? So this one is to Hari. Smart contract security is considered equivalent to audits today for most developers and for any users who care about it. I think there is some truth to it.

Well, the term audits in a traditional sense often mean like a tax audit. And maybe the term is not the correct way to look into things. The issue is that a tax audit is completely defined, well-defined, whereas a smart contract secure review is often open-ended. You don't truly know what are the bugs when you are coming into a code base. And it's very frequent that when we audit a codebase or like you know review a codebase you find bugs that have never been discovered before so in that sense like audit the term can be a bit misleading but at the same time it's okay to use it like colloquially I don't agree I think it's it's a it is part, but it's a lot of things start way before the audit.

Simplicity of the code, documentation, thinking about it, of course, and using tools. Of course, audit is a significant part of it, but smart contract security is many things. Like we have seen recently even code, like, for example, decentralization aspect. Everything you have to worry about when you have a code which carries a lot of value. You need a lot of things to make it secure, and audit is a core part of it.

But you want a lot of it, not just audit. Sometimes you see a customer, he is going to an auditor and he said, you understand what this code does. It's not what you want. You want to have, and we have, for example, a team that have internal security and that's great. It's not instead of audit, but it's a very good component.

So you want everything. Do you believe that the protocols that you work with understand this, or do they think that audit is everything? I think it varies. It's not like one thing. It varies.

There are definitely a lot of protocols that understand. I think it depends. Some protocols do see their security as something they delegate to security provider they see like security oh okay we are going to do another security review you know one week before deployment they are going to find everything and you know we are done we want security I think there is a some team that see security that way so it's kind of a part of a fact that they see it that way. But it's not obviously what security is about. It's not binary.

It's not like you pass, you don't pass. It's everything Moody mentioned, like security is like a, it's a journey, it's something that is going to help you to get better overall. I can add to that. At this workshop here on what did we learn from hacks. And what I spent a lot of time at DEF CON was interviewing projects which did not get hacked to have the opposite side of what to learn from the not hacks.

And there's a wide variety. It is true. I would agree it is a fact what you said. For most projects. They equal having done an audit is what makes them secure.

But there are those projects which honestly even we struggle to find more bucks in. And crowd auditors have a very hard time then to find anything, right? They don't get paid anything even. These projects, they have really excellent security practices through the whole development cycle. And they know that audit is a piece of the puzzle.

So, yeah, there's much to learn, I think, also from the people who have not been hacked. So, yeah, I'm looking forward to another workshop, actually, on the not-hacked people ones. Absolutely. So, good. Can I add something?

Please, yeah. I may have misunderstood the question, so I completely agree that, you know, an external secure review is not enough. The best teams that we work with, they're very, very security aware and they're very security conscious from day one. They try to build protocols so that even if there is a small mistake in one component, there is a lot of defensive-like building where one bug in a certain component wouldn't be the end of the world. So the greatest teams out there they are aware of security from day one of building and they don't just rely on an external secure review to secure their you know small contractual protocols.

Great point so we may be sort of answering there may be some repetition as it goes along but we are sort of just getting warmed up. By the way, none of these statements that I'm making are my opinions, these are sort of, and they've obviously not been vetted by any, you know, any of the panelists. This is the first time they're actually hearing these things, but it's, a lot of these things are sort of common perceptions or misunderstandings in the space. So that is what it is. So the next one is for Jocelyn, and you may have touched upon this already.

Smart contract audits are neither necessary nor sufficient. I think you talked about the sufficiency part, but can you talk about the necessary part? Does every protocol need an audit? Okay, I hope that we get to a point where it's not necessary. Like that should be our end goal, as a security community, our end goal should be to put us in a place where we are not needed.

To get to that is going to be, you know, about training, about education, about tooling, and things like that. Chance at this end state is never going to happen. We are not going to be out of business by that. But that should be our end goal. So it's a fallacy, but it would be nice to be a fact.

Anyone else want to add to that? I mean, I agree to this and I can maybe like give some anecdotal examples. Over time, the quality of engineering has gone up significantly. If you go to a record report, the number of hacks from 2024 is like, you know, very little as compared to like other years. In 2020 and 2021, every other week, there's a hack that will get into the top 10 of the report.

And I think there's only one from 2024 in top 10 today. And even if you speak with some of the greatest bug bounty hunters out there, they share the same feeling. They feel like the bugs are in code deployed in 2020 and 2021, not in the code that's deployed today. And I talk with a lot of successful bounty hunters, and they just go one by one on projects that are deployed three years ago. And they believe that the current projects are much more mature.

Just to answer your question, I think it depends on whether the actual contract handles user funds. Not every single smart contract has to have tokens that have value and hold ETH or things like that. But I'd like to think that as of today, if you are deploying code, production code that's handling user funds, you should probably seek an external security assessment. I certainly agree with Jocelyn. I think ideally in the near future, we have tooling that's a lot better for developers, but there's so many foot guns in the EVM, maybe Solidity itself as well, that it's extremely easy to introduce bugs.

So static analyzers are there, fuzzers are there, but seeking advice from people who have been doing this for quite some time is certainly something I'd recommend. I agree. I think also that we are actually seeing a lot of progress in the last year. We are seeing, at least with working with our client, first of all the tool get better, but also humans, internal people get better. And we are seeing actually internal security researchers in companies that we work with, they actually do pretty decent job.

So basically they have something called internal auditing. I don't know if it's a good term, maybe it's a misleading, but actually it's useful. We have seen these teams are working in addition before, after the auditor, after deployment. We have actually recently worked with one protocol and actually we together, and it was actually audited, but we together with the team found a compiler bug just before deployment. So the teams are getting more technical.

The teams, I think, not all the teams, but some teams are getting more technical, and there's more education thanks to Secure Home and others. The more this space will be educated, we see also on Web2, some people get audited sometimes. But I think the more there is, the need for audit still will decrease in my experience. I know. And this is an external audit, right?

Yes. I think it's definitely wrong to think that an audit or a review isn't needed. You will always need other people to challenge your code, internally or externally. Sometimes externally is the most efficient because they have been doing this more than internally or internally they they might be too tunnel visioned on this right but you will need this and the more review you put in the better your whole project gets actually so we might get away from external reviews over time or reduce the reliance on them, but only because we got internal reviews on a state which is really good. Makes sense.

So, by the way, just to clarify, when I say audit, I mean time boxed external security reviews of smart contracts, right? To come back to something that you said, which is if you are handling user phones, because there is also a point in time where if you are deploying something which is not going to be integrated in anything, which does not have any impact, which does not have any user phone, your need for like external validation is lower than for something which can have an impact um so right now like everyone is deploying the fire application you know mostly and so there is always like kind of like a composability or user phone or you know something like that but we could see a point in time where people are deploying things that have less impact that are not connected to other protocol uh for which like the security guarantee might be lower than what we need today can I add that thing if you have funds in your contracts in some way or if you are a company that manages like funds chances are there are like bad actors that are looking to exploit those funds already so people are out there who are trying to steal these funds and you need to work with the mentality that if you don't put in the work others are going to come in and steal the money. That's a reality. Makes sense, alright. So turning turning up the heat just a little bit, here's a fun one for Matthias.

Audits are opaque, underwhelming and overpriced. This is a loaded one, so, and just a bit of the context, right? Opaque, right? And not from the context of your own companies, but in general, right? The perception is what we are going towards.

Protocol gets an audit from some team. It could be a solo auditor, it could be, you know, you have all the variants, right? It could be a contest, it could be any of those. The protocol gets deployed. And we don't know if the contracts deployed were the same ones that were audited, were there changes made, were they upgraded?

So that's the opacity I'm talking about. And then there's a report that's either published or not, it's private, we don't know what the scope was, we don't know how much effort went into it, we don't know who performed the audit, right? There are just so many levels of transparency that may be missing, right? Critical, critically missing, so that's opacity, opacity and then underwhelming in the sense that, I don't know what the latest direct leaderboard statistic is, but several of the protocols that were hacked, right, for millions, hundreds of millions, had audits, right? So it's, so that is, that is that part.

And then pricing then pricing right so when I use I was talking to protocols as well and when when we talk to them they like great we will love it can we you know do it for a lower price so that's yeah bit of a loaded one feel free yes thanks for that so the price keep it today yes so starting with the um opaque right fact um the um like overpriced one jumping to the end I definitely agree with the feeling if I am a founder of a defy project and you have to shell out this amount of money which equals approximately for a small project your development budget you are shocked. Is it overpriced because of that? No. It's because the security is so paramount and this is not something you are used to. So that's a fallacy.

The reason for why it can be underwhelming, there I'd say like it's also a fallacy. The reason is that you get a lot of value from that added security. And overall, the stats we have seen, which there was a great talk by Peter at DSS, for example, on this, having reduced the exposure of the ecosystem to smart contract tech significantly shows that value. And this has been heavily carried by initiatives like secure am to train and by a lot more audits being available today to also have the throughput right and then doubling down on the initial part this is kind of dear to my heart this opaqueness we struggle with that ourselves when being an auditor after another auditor. And you go in and you read reports from others, right?

And you want to know, okay, what did they focus on? What should we focus on? Did they miss something? Did they have some misconceptions? What are their assumptions?

You will not find it in an audit report. Our audit reports today focus heavily on issues, right? That's kind of the bread and butter. How many criticals did you find? We do very extensive system overviews and clients love it, right?

It's really important, but that is something which is still rare. It's this documentation thing, right? Which all developers and auditors also aren't into that much yet. You hunt for bugs. You don't hunt for the best documentation.

The way I do it is, for example, if we follow an audit after Trail of Boots did it, then I call. Then I reach out and say, hey, let's jump on a call and how did you do it? And then we get to understand better. But this is probably rare. And the public audit reports bring little value except for you can extract, hey, that was an issue.

You can learn from that issue. Yeah. Hearing you ask the question reminded me of a conversation we had just before DevCon on the opaqueness and opacity of the space. I think there's definitely room for more transparency and perhaps for even a platform that could link those commits that were actually assessed by some of these firms here and what's been actually deployed on chain and I think that is a massive gap that and the unpublished security assessments just want to say if if a Sigma Prime report is not public it means that our client did not want to publish it all our work we take great part in our work all our work by default is to be published. Unfortunately, in practice, I estimate about 40% of our work being kept private.

And there's plenty of reasons for that. You can imagine the biggest ones, I guess. But I think it's probably something that we should aim at fixing. And I think there's room for a platform that could, you know, kind of name and shame all these protocols that decided not to release those public reports, those audit reports. Sorry.

I actually disagree. This is going good for me. This is going good. I mean, this is going to be good. Yeah.

So you want to start? You guys. Okay. So I don't think we should have all the report public. Like all report are not meant for public conception.

They are meant for engineer. Like they are meant for the people building the protocol. Making them public is nice. Like it's nice for transparency. It's nice, like it's nice for transparency, it's nice for like visibility, but I don't think it's a necessary step for the security of the protocol themselves.

And... It's not for the users. It's for users to have confidence in the potential safety of the protocol they're interacting with. The reality is that users don't read the public report. We can have a protocol, we can say...

That's a policy. They read. Some, some users. We could have a protocol. We say in the executive summary, this protocol should never be deployed.

It's trash. It's not going to prevent users to use it. This is where a platform like the one I'm suggesting, sorry, could come in, right? Where you don't have to actually dive into the technicalities. Perhaps we could come up with a way that we surface the important information that should be consumed by users.

This is my point. So I think that's probably, I'm definitely on the minority here probably in this sector I even so we are our most commitment is to our client not to the community sorry about that if you want to deal with it's fine so if we tell something to the client and the client we we we need to be transparent but we our most commitment is to the client we are not a bug bounty platform we are a company that's serving a protocol they pay us we provide services we do also tools of course but then people use the tool so we provide that. We, of course, we like to talk to this team here, I will run with you, but our most commitment is to the client. When we disclose a report, for example, we find many criticals, the client does not want to publish it, we negotiate with them. For example, we tell them to fix the code, we will not publish it because we are not a shaming company, we are not a social media company, I'm sorry about it.

So this is what we are not at, and maybe you need another company for that. Now, as for partners, we have advantage because we are using tools. So every commit that we have, we are getting the rules. You can use FASA, we use our approval, it doesn't matter. So our client, we've seen even other publishers, that they change the code and even before us, it actually finds a bug because it has these rules that we wrote.

And also when we work with other auditors, we look what they find and we write rules for that. For example, you saw recently the Uniswap updated their code after the contest and then they run the rules and it fails we see the thing so we our biggest value as a tool provider is to integrate in the CI so basically every time you change your code you want to check that so that sort of where tools can be more valuable than humans you are not a minority okay thanks so can i after the the original question on like the opaqueness the the transparency and the pricing so we are the youngest company here we started in like late 2021 and one of the reason of starting now speed and later continues because we saw this like we saw that the audits were very opaque, there was no transparency, they were extremely pricey, and we wanted to do something different. We are extremely transparent as a company. We are very transparent about what the security searches make, how much we make, and we pay our security searches a lot of money. Because of that, we have some of the best talent in the world like they're not necessarily like security talent that just the best talent in the world at what they do and it's a privilege for us as a company to to get them to work on you know security and you can see over time that you know the smart contract hacks have gone down significantly and part of the reason is because we are able to attract a lot of talented individuals they would be excellent whatever they do it doesn't matter security or something else these are extremely talented people and the money you pay them is 100% worth it and we also build Cantina later on to make it more like affordable and flexible for people so today like if you come to us or like many other providers like I think there is something for everyone like if you are a small project that has something that you want to review there is some something that we can offer you that will fit your budget and to like answer maybe like some of the points over there I do not believe we can grow the industry if you like shame companies so we should like avoid like shaming companies.

That's my two cents. What we always say to our clients is that if you want a report to be public it's your responsibility to educate your user on how to read a report and you know like even if critical bugs are found in a report, what have you learned through this process? You know, how have you improved whatever you needed to improve to get better? So there is like part of it which is from the moment you want to have something public, you need to think about how it's going to be read by the user. And that's not our responsibility to do that.

I think it is to a degree, to a large degree actually, because we know like we are in a different industry than the others which usually keep reports private. It is going to be read by the public, it is something which is important that many understand, like of course you can have technical details but the audience is not only the project. This is also why we call it audits, to be honest. Audits are traditionally not reviews, right? And what I would never want to have is that there is a false impression of security because of an audit done by anyone, right?

So, I agree with the client doesn't have to publish it and that's up to them. I would never go in and say oh now send us a new code, we review from like as if that was original code, we give you a report which says zero findings and now you think it was perfect, right? If you publish a report it will have everything in there and in that sense I agree with like if you know there is a report upcoming and it's not being published there might be very good reasons for it right but it is a sign of look out right be a little bit careful what's going on. There are many, many more, and our timer has already changed colors to red. As you can see, we can go on and on.

This, I think, achieved the desired effect, right, in terms of turning up the heat and bringing the disagreements. I think we all, at a certain point, agree. It's just about the terminology, the factors, the incentives, and, you know, the industry or the space as it is now versus as it should be. And obviously, we'll have different opinions on that. So the next one, switching gears a little, this one is for Mehdi.

Smart contract security, on-chain security, is overrated compared to Web2 off-chain security. Yeah, interesting. I kind of want to say... You don't need any context. I want to say fact.

For 2024, that is, I think. One of your earlier questions was whether we've sold smart contract security. I don't think we did, but we've gotten a lot better. And the numbers actually show this. The past year and the past 18 months, we've lost more money to threat malicious actors in traditional Web2 security problems.

Unfortunately, what we still see to a great extent these days is protocols solely thinking that smart contract security is the only thing that matters. And if I get a gazillion number of security assessments, if I have a bug contest, if I have a bug bounty program targeting my smart contracts, my on-chain operations, then I'm good. Then my users will be good, and there's absolutely no other vectors for me to get popped. That is a huge fallacy. That has actually cost a lot of money this year alone.

Peter, that you mentioned, had these great numbers up in his presentation at DSS, but it's something that I think we're actively trying to fix just by educating this protocol, saying, hey, if you have a multi-sig and you're dealing with user funds, then there's probably other ways that these threat actors could get and unfortunately cause you to lose your users' deposits. It feels like we are at the same stage of, like the same place we were in solidity security maybe three years ago, four years ago. So I'm quite hopeful that things will change. But at the moment, what we're seeing today is a lot of money, so much money lost to North Korea, not to name them, through things that really, really shouldn't occur anymore. Web2 security, I wouldn't say it's a solved problem, but we've learned a lot of things over the years, right?

So security hygiene, raising the bar is everyone's responsibility within an organization. And I think, you know, through education and also, you know, some of these OPSEC audits that some people have been hearing about, we can help these protocols raise the bar. Maybe a good time to mention the security framework from the secretarians. Yes, yes, great, great. Thank you, thank you.

So if you go to frameworks.securityalliance.org, you will land on a page that has been put together by the security alliance. Kudos to Mata, who's done an incredible job on this initiative. And essentially, it's a collection of best security practices across the entire stack of a Web3 organization.

Forget smart contract security, right? There's a gazillion number of resources and experts out there. When I talk to protocols, they don't really know how to secure their CI CD pipeline. They don't really know how to harden their EC2 instances. They don't know how to prevent SIM swapping and harden their Discord servers.

All of that information is out there somewhere. What we did was consolidate it and put it in one central repository that everyone is actually welcome to contribute to. And we want contributors, we want people to go and close the gaps that we have because we do have gaps. It's not a perfect release. In fact, it is not a release.

So please take a look, frameworks.securityalliance.org and this should hopefully, hopefully help raise the bar. Thanks, Jocelyn. So can I add to, like, maybe, like, I agree, like, a lot of money is getting lost today by traditional attack vectors, so much so that if you run a company that is, like, building in crypto, or if you're, like, an engineer, you're going to get constantly phished or, like, social engineer right now like if you you're not getting getting fish your teammates are getting phished and it's even more important to build like a very resilient protocols like we see examples were protocols that were very secure on the smart contract level lost money because somebody's private key was compromised because of a social engineering attack like oftentimes this would look look like, hey, I have a job offer for you.

Do you want to interview with us? And then they would ask them to download a malicious NPM package and accidentally compromise their machine, which will eventually have some privilege-like roles as private keys somewhere. So it's so important today. I think here the fallacy is to think prevent phishing and you will be fine on this level like smart contract security we have seen hacks right and we may not drop the ball on this but the hackers are often like very talented individuals but but they aren't usually the leatherers groups these we have seen on the other side so the threat is here an actor a state actor right which has different resources they will not get you through fishing they will get you through zero days right the level of sophistication you need to put in there is a different one. There are great guidelines of how you can improve your security out there, but as a project which has like eight, nine figures, which someone can take by compromising a few keys, the game changes.

The game changes completely, right? And it becomes something unique, right? Where general guidelines don't help. It becomes similar to smart contracts. Every smart contract, it's hacked differently, right?

So that's why we have these custom audits here. But only for these very large projects, I think the real new threat is a state actor compromising them, right? Ethereum being out there the first time, kind of against a state, right? So this will be interesting. To illustrate what you're saying, I like this quote from Maurelian from Optimism who says, we should build our processes so that even if we were to hire 49% of our task force and DPKR agents, we would still be fine.

And I think if people who are building the next protocols of tomorrow can keep this in mind, then we would be a lot more resilient to these problems. But none is, right? None is today. There's perhaps a handful, a couple of protocols out there that are trying at least, but yes, you're right. Not enough.

Great, great point. So moving on to Muli. So this is something, I think there's a topic that you're intimately familiar with in Sartora. Formal verification should be used by all projects. I think the stress is on all.

The answer is yes, definitely. And even more, the earlier the better, and even more, and that's contrary to some of what our competitors say, you do not need a PhD. You essentially can use, start with fuzzing, start with unit testing. You don't need to necessarily prove. Of course, sometimes it requires some skills, and don't wait until you have all the TVL, and don't wait until the tool is, the code is complex or the code is complete.

And don't write a lot of assembly code. I have a different opinion on that. Probably of a movie who is my soon-to-be neighbor, I don't believe that. I think fallen verification does not scale at all to the level of complexity of today's code base. I respect the Torah for really pushing the limits, but it's fundamentally something that's unscalable by design.

So let's see examples. For example, let's take the recent Uniswap V4. It was formally verified by Jochen, who's somewhere there, and then the container tried to find a bug, and no bug. Let's take Euler. Also, Uniswap, the container didn't find a bug.

So, of course, the real answer, it depends on the time that you spend, but it depends. If you have three or four weeks, so far at least from using the experience of the great security researcher, at least I understand why you are protecting your territory. But and it's good actually. I like it. But the issues that we are seeing actually, I think Kurt here from the Maker team who is now in your team actually has written a beautiful rule and found like a huge mistake.

So we are seeing people writing rules on code which is complex and simple. Yes, it is true. The tool is costly sometimes and people are building open source software like the Holmos and others, and we are trying to get our tool better, but I think the technology is getting better. And actually, the thing which is hard about formal verification, actually, for that matter, phasing too, is writing the specs. I think the issue with why our tool is not used more is, of course, there are technological limitations, but writing specs.

And in DeFi, I work in formal verification now for 40 years. And I can tell you DeFi is a beautiful domain because the domain is mathematical. So specs are very natural. Think of something like a constant pool. It has a beautiful environment.

The multiplication is constant. And we work after the top auditor, and the team wrote this constant pool, and in fact it prevents losing all the money in the contract. So I think formal verification is a formal specification. Use phasing. The issue is that writing invariant is a very interesting concept.

Actually, I think you should use it even if you are doing manual auditing. If you don't want to use CVL, you want to write it in English, it's fine. But I think writing spec early is a very, very crucial thing, and you should write it. Whether in a white paper, you should write the spec. You look at the compound V2, compound V3.

So writing the spec is a look at the compound v2, compound v3, you look at it. So writing the spec is a very very important concept whether you want to use CVL or other languages but writing the spec I understand and you they can still pay you, no way. So good, so as you can see, as you can see we're we're all really passionate about our uh you know about what what we've been working on for for a really long time so this is this is good I mean this is uh what we've been working on for a really long time. So this is good. I mean, this is what we wanted to talk about.

So now... Can I rest for, like... In, like, five seconds. So I think the problem is that the complexity of DeFi is increasing, like, linearly, but then the complexity of formally verifying increases, like, exponentially. And we got onto a point where you use V1 or V2 and maybe V4, you can verify it, but I don't think the next generation of DeFi, we can scale to that point.

So the only way to scale system, not just formal verification, is modularity. And the issue is that with modularity, you can scale formal verification better than phasing and other. Phasing is good for many things, but with formal verification, the beauty of it, if you look at Euler V2, unlike Euler V1, it's very, very modular. If you write code modular, whether you use formal verification or not, it's a good thing. So you have to design your code well, and then it can complex.

And actually, you can make the blockchain modular. The more things are modular, it will be more scale. You write your spaghetti code, and yes, maybe they can pay you, but it's not going to help. And I'm here with Muli, like formal verification, to me, made blue screens go away. For someone who is that old, that they grew up with constant blue screens, then this is something which Microsoft used to make device drivers, like, proper, like, I mean, Muli did, actually.

And we'll get there. The Wide Wide West is not suitable for that. Manual audits are more efficient. Things change too much. We'll get steady.

We'll get in more modular ways, and then we can build, and then the time of formal verification will come to its full power. That's what I believe. Can I quickly interrupt? We are going to get into Q&A the last 10 minutes so while that is coming up I know we can you know rebut quite a bit and agree so there are I mean we're just warming up right so let's also give maybe some of the questions And then, okay, we see it here as well. All right.

So the top-voted one, in five years, more than 80% of new code will be AI-generated. I think that's a fact. Like, there's a likelihood that a lot of developers are going to use for part of their code AI. Oh, sorry. No, no, sorry, because you're all nodding.

Sorry, everyone was nodding. I feel like I'm the only one who doesn't think that's the case. I think, I guess the question is like, what does security mean when code is going to get AI generated? And like, you know, it's a bit of a cantina. Like, we are building towards this vision that there's going to be a billion developers in the future, and we want to solve security for those people.

We know how to secure like in a code basis where there is like no room for mistakes, but I think the real challenge in the next decade is going to be like, what does it mean to secure when a billion developers are now writing code? Okay. Any rebuttals? Any... Yeah, I don't think so.

I don't think... Let's see, deployed code, smart contract code that will handle billions, hundreds of millions of dollars of value, like properly coded by AI agents and deployed on-chain without any human intervention within five years, I don't think so. Without human intervention, probably not, but... Human scrutiny, sorry. Yeah, yeah.

I have seen code which was deployed for, like, real protocol where I am somehow confident that it was solely generated by, you know, charge of pity or whatever. Right. Did you audit that code? NDAs. Bugger easy to find when it's...

Good. Right. Did you edit that code? NDAs! Burger easy to find when it's...

Good. So let's go on. I mean, some of these questions may be repetitive in nature, so we'll skip the OPSEC one, but the one on top, L2 fragmentation makes smart contract security more difficult. I think to some extent, because there are changes in the EVM across like L2s and if that is something you have to watch out for, for example, ZK Singh does have some deviation like the Creo 2, KIA's pricings are different, so it makes it a little bit more difficult but not really. It would make it because you change small thing, We have seen it like the LLVM bug of the ZK.

So the issue is that small changes and now we know account abstraction is being built. So I think for us we ended up because we have to model everything in the thing. So things are tricky. Most changes are small, but there are some changes and people should be aware, even things like Celo. So I think maybe that's actually an opportunity for the SEAL team.

You guys should at least document it. Yeah, we see that. I agree with Harry. I think there's like push zero, for example, not being available across all the EVM chains, but it's not really making it that much more difficult. We got to be aware of those differences, but it doesn't really change the game, I'd say.

Fantastic. All right, next one. Okay, this is... I had a different version of this. Okay, these keep getting switched.

And thanks for marking those answers. Smart contracts are insecure because saluity is a flawed language and somebody on this panel may want to answer that or not. So I want to say that there is an opportunity to make Solidity 100 times better. I believe in that and we need to make it 100 times better. But at the same time, I would argue a lot of the bugs are really like at the logic level.

For example, there are rounding bugs that are, you know, that exist in smart contracts that has been there like, you know, 10 years ago. Like there are local launches that failed because of rounding bugs and now DeFi protocols are getting hacked because of the same rounding bugs. So fundamentally like it's like logic issues, not necessarily like language issues. For example, you don't really see like memory management being a problem in Seridity, whereas you know in traditional compilers that is a big problem. Like you don't allocate memory in C correctly, like you can get exploited.

So I think two things. There is an opportunity to make Seridity a hundred times better and we should do it, but the bugs that are out there, I mean it's across every language. I totally agree and the issue is that the thing, and actually I don't want to talk, but there are so many other languages which are proposed that say we go to this new language, it's type safe and we solve the problem. It's not the case. I don't want to go to these other languages that are proposing.

Solidity has problems, but most of the bugs, they're logical mistakes, they're access control, they are things that if you move to another language and you have beautiful language design, maybe these new languages, it's still not going to solve. So I believe Solidity has fundamental flow that leads to issue with respect to security. For example, there is no inbuilt testing in Solidity. That's for me a huge problem in security because now you have to rely on third party tricks and hacks and like cheat code and whatever. No debugger too.

Yeah, like there is a lot of fundamental flow. Like the optimization of the compiler are not great. This led a lot of people to use assembly to do like basic operation. That's a fundamental flaw of the language, which leads to a lot of security issues. So I do believe a lot of security issues stem from some of the design of Solidity.

I agree with all this point. There are opportunities to improve, but on the optimization, I would say that if you know what you're doing, you can always beat compilers. Any compiler, if you know what you're doing, you can beat it. Compilers can never match creative humans. I don't know if it's true.

I always heard JavaScript was the inspiration for Solidity. And what Solidity did absolutely right was make a language you can easily understand. Like only Python, perhaps, is easier to understand from the get-go. But JavaScript is very close to that. and it is a very auditable language.

It is not a language which makes it hard to make mistakes, but as was said already, the mistakes are in not understanding what the code is doing, not because of language features usually. So this is what Solidity got really right, to make code we can easily understand. We were moderating a panel with Harry at DSS and I think there's this misconception that Solidity is flawed and I totally agree with what you're saying, but I think the biggest problem comes from the EVM, as we were saying. Right? So, Solidity compiles down to EVM bytecode, and there's been some, just say, questionable design decisions that have been made at the EVM level years and years ago that we're kind of stuck with, but there are actually, the good news is there are ongoing efforts to remediate those in the hopefully near future.

I think that's an excuse because, for example, again, no inbuilt testing has nothing to do with EVM. That's a design choice. I agree with what you said. I agree with what you said. All right.

So I think some of the interesting questions are popping up that we couldn't get to. So the top one, right? Skin in the game, as some people tend to call it. The first thing that happens when a protocol gets hacked is, at least on crypto Twitter, is who was the auditor, right? And there is a school of thought that believes that reputation is not enough, that they should have skin in the game, and they should, you know, be paying more than with reputation.

What do you guys think? I mean, I think it's a practical question. Like, at the end of the day, like, we are security experts. That's what we're good at. If you want to do insurance, that's an entirely different ballgame.

It's something that's like fully mathematically more, you know, you can model it with mathematics. That's not our expertise. And I think it should be a second party that should come in to like insure it. And that party is not there today like most insurance companies they like you know sell off the insurance off this to some third party and we don't have that today so I mean we would love to make that happen but we are security experts no like insurance experts if there are people who want to pair with us like we're happy to do it I have to say it already happens, and it happens in a different way. While the small money you might reclaw from an audit, that's usually not compared to if you really got hacked on a large project, right?

It's just peanuts in comparison. The real value brought, if you have an auditor who is with you, right, is that they'll be there for you if there is an exploit, if there is a bug report, if anything was missed, and they'll put all they can in to help you for free, right? They missed it, it is a reality, and now they are there to reduce the damage at kind of no cost. And then that is something very important, I think. This is something you should ask for.

So that you know, like, if shit hits the fan, someone has you as much as it's possible now. And that's a real value out there. Cool. We have 30 seconds. So I want to take this opportunity to give each of you sort of a closing statement which you believe is the top thing that is considered as a fact but is actually a fallacy or the other way around?

Starting with Hari. I would just double down and say formal verification doesn't scale. Thank you. All right. We don't have time for discussions or rebuttals.

We'll take that off stage. Joss, Jossian? Invariant-driven development should be the future. Auditing small changes is easy. It's a fallacy.

Tight OPSEC security can save you. So mine is that basically now he put me in a difficult situation. I think we need to understand that actually smart contact security is not everything. There are a lot of actually other things there and we should be aware that actually a lot of the problem and if we see in DSS and we see it also from our client is not actually in the smart contract security. All right, do you have one, Rajiv?

Sorry? Do you have one? I would, you know, agree with all the statements here. I have quite a few myself. I think a lot of it was reflected in some of the comments earlier.

Yes. Maybe one. Do we still have four minutes? Or is that over time? We're ready.

Oh, okay. Do we have a talk after this? We can keep going. Please, please. I do have just one closing statement.

I think we need more time for this.

Automatic transcript — names and jargon may be misspelled.