Security Tools Panel

DeFi Security Summit 2023 · 15 Jul 2023 · 1:02:48

Fraser Brown of Cubist moderates a panel of tool builders from Trail of Bits, Fuzzing Labs, Electric Capital, Certora, Web3 Foundation and Dedaub on the state of smart contract security tooling. Panelists compare web3 with web2, noting that open source code and large sums at stake have driven strong static analysis, fuzzing and formal verification, while a smaller user base leaves fewer tutorials. They also discuss the order in which tools should be applied, from static analysis through fuzzing and symbolic execution to formal verification.

Speakers

Topics

From DeFi Security Summit 2023, hosted by DeFi Security Summit.

Transcript

um welcome to the tools panel we love tools thank you thank you so um let's start things off with a quick round of intros point [Music] hello okay let's start things off with a quick round of intros so who are you uh what do you do and also what kinds of security tools do you either build or use on a daily basis hey everyone I'm Nat I'm a security engineer at trailer bits and on a

day-to-day basis we're generally using tools like static analysis and fuzzing on a day-to-day thank you so I'm Patrick the CEO of fuzzing labs and as the name suggests we are doing a lot of fuzzing so we are basically building security tools and dedicated further for either a client side or smart contracts uh hey everyone I'm Gary I'm a software engineer at Electric Capital and I work on security tools that kind of focus on like post deployment so work on like a code search tool um and surfacing information that comes out after contracts are live and deployed

hi I am Ori I work at sartora as a developer and in developer relations we're developing several security tools one of them is the software approver which is a formal verification tool for smart contracts and the other is Gambit which is an open source solidity mutation testing tool hi I'm Vargo I'm part of the research and specifications team at the web3 foundation I like to call myself a full stack verification engineer so I'm interested in the whole Spectrum right from like analyzing consensus protocols all the way to uh verification at uh

at the code level and mostly right now I'm focusing on verification tools for the polka dot ecosystem hi I'm Janice I'm co-founder of ddub we have a public blockchain Explorer that's geared towards security so we have probably the best decompiler for evm byte code out there so we offer free tooling for all sorts of security investigations but our proprietary tooling has to do with static analysis as well as Dynamic analysis of transactions so we do both Bots for monitoring and we have a language for specifying those and we write a lot of static analysis for code awesome

um and I'm Fraser your moderator okay so can someone or a few of you give your sort of pithy couple sentence analysis of the state of Tooling in web3 generally it's good so I mean we can concentrate on the negatives but uh if I were to give a two sentence description uh considering that this is a young domain we have very very good tooling security tooling compared to much more mature software engineering domains we have probably the most advanced versions of tooling from the

formal verification side the search or approver Etc from the static analysis side I mean I've been in the static analysis Community for over 15 years but the best tools we have ever put out are in this domain and it's all because there's so much money at stake so we can complain there are definitely problems but it's good to see where we are in the whole universe and we have some pretty awesome tooling that's an uh actually kind of answers my second question so I'm just going to throw that out there too and you can answer both um so how would you say the tooling landscape is different in web3 compared with web2

yeah so there is one clear difference between web3 and web 2 right that you can't use uh security through obscurity in in web3 because like most of the code is open source like attackers can spend months analyzing it before they they launch the attack so one of the the key differences I would say is that since everything is open source uh the the analysis has to be much stronger and uh obscurity cannot be cannot be used for security I think one of the main differences

between web 2 and web free tooling from the point of view of the user is that the user base of tools in web3 is much smaller so if you need to look online for answers for your questions or look for video tutorials about how to do something with a certain tool you're probably not going to be able to find it or at least you're not nearly the same ease or quality yeah I think to expand on bargov's point um one of the main differences I see is like because it's open source all the code is out there you know you can there's a millions of dollars of value behind it you get this really quick flywheel where you know there's Auditors and security researchers and they can go

audit the code use all these tools give a bunch of feedback and so you get this really nice virtuous cycle and so I think it kind of leads to the tooling being really good and also evolving at a really quick rate um answers on the panel the only thing I would add is that I think web 2 Tools in some ways are also more advanced than web 3 in terms of the usage in different code bases and usage across applications and so I think there's also um in addition to that there's also kind of the adoption and kind of more having developers actually integrate with like

existing static analysis tools and fuzzing is definitely something that like should be applied to all code bases and I think is definitely like something that is much more apparent and needed in the book um so I I disagree a bit actually compared to what you were saying um if you are speaking about web 3 in general I think there is a huge gap between the different blockchain I think if we are speaking about ethereum the majority of the toolings are really good and we have a bit of everything and so on but if you compare two other chain in general um there is definitely a lack of static

analyzer for the no formal verification on some machine especially if you also take a look at all the new l2zk stuff there is a lot of news um other smart contract language circuit ZK circuit and so on and in this area basically everything needs to be built so if we are only taking a look at atarama and evm yeah we are pretty much sure if we take a look at the rest it's nothing compared to to what we have yeah I mean definitely would agree with that one big difference that I'd like to point out is that this is a perfect playground for security tooling uh it's

it's the only opportunity one ever gets to have all the code open all the test cases pretty much all the past executions permanently recorded you can do pretty amazing security Tooling in this space in the web 3 space and the other thing that helps tremendously is that its small size of code bases like a little over five years ago I was doing similar things I was doing static analysis at Facebook the Facebook Android app which is like the little app that you install on your phone that's a hundred thousand Java classes that's the deployed byte code Java byte code that goes in your phone like a hundred

thousand Java classes imagine what tooling can analyze that versus the tooling that can analyze you know uh 50 Smart contracts that are typically what constitutes the the average D5 protocol that manages so much money so we have a perfect playground and we have gotten a lot a lot of advanced tooling which is great but certainly it's through it's only limited to evm and and especially even in evm mostly ethereum great um so that's somewhat related to this next question which is about how you hope to see the state of tooling change moving forward I

guess we got some of that at the end we would like to see some more One-Stop shops currently you get different tools to do different functions so you get deployment or you get compiling or you get analysis and fuzzing so some tools have already started to move in this direction to great success I think we're going to see more of that and obviously that relates also to the issue of multi-chain which is in general a bit of a lacking area of vulnerabilities for many of the tools yeah

to give you an example in in all cases we are building security tool open source Finance by grants from foundation and typically in my opinion that's the way it should be I definitely enjoyed the different tools that most of the the guy are building and I'm playing with with them at all with all of them but the fact is for me when you have a blockchain and it's creating his own smart contract language his own consensus and so on that should be the one that is financing and developing security tool to basically give that to the to the developer it should be at least them that is doing the first step and then defense security

companies and teams that basically built on top of that and provide Audits and and everything but it for me it shouldn't be the the other ways are a lot of existing tools like um like for example for static analysis with slither for example that do provide like a lot of results that developers and like security researchers have the opt the opportunity to triage um I do think there's probably room for improvement in terms of reducing false positives just to make sure that it it gives you like developers and users just

a better idea of what is more likely to be wrong and kind of in ease of an ease of experience in terms of understanding like what code might be affected and on the flip side I think um of false negatives from the fuzzing side as well to make sure that fuzzing tools can be extended easily and nicely just to make sure that bugs that should have been caught through fuzzing are actually cut and so I think there's a lot of room for improvement in kind of the existing tool space currently yeah maybe I can give some insights from

like the polka dot ecosystem so the whole ecosystem tick stack is based in Rust and it would be great to see some tooling for rust which even before like security or verification the first thing is like program comprehension so it would be great to see tooling which improves like program comprehension because it's only when the developer really understands what is doing that he can come up with invariants and so on so that's like the the first layer that I would love to see being being developed and of course like after that comes uh static analyzers and surprisingly there

isn't that much options which are robust enough to be used on like production grade code I think my feeling has been that at least for like Rush tools most of these tools are like academic in nature and in Academia you tend to prioritize novelty over robustness and so that I feel that's a huge potential here where there are great ideas but these ideas have to translate to like robust tools that can be uh applied on production code yeah so I I would definitely agree but there's uh there's a standard added here

which is there's no money in tooling so and especially in comprehension tooling like they're they're well-known studies like even Google has put something out that says uh nobody cares about offering tools uh to help the programmer understand that's that's considered low value so you need to go directly to something that has value which is like security analysis so I agree that there's a lot of need there but it's not going to be filled by the market so well foundations may need to step in to give better tools at that level because the market will not step in there and imagine this Market with at best a few tens of thousands of developers at best uh compared to the overall the web 2 Market with millions and millions of

developers I mean there we start now to see some security tooling that's uh and comprehension tooling that that has General applicability but it's an order of magnitude larger their Market but certainly I will agree with everyone that there isn't there is a lot of room for improvement there are things we can focus on both on follow the false positive false negative side but there's also a big potential for disruptive innovation here uh and where do I want to see disruptive innovation well first of all we just saw llms we saw AI come in and we've seen completely trivial uses like you just you find like a text generator that hallucinates and you

treat you feed it your program and see what we'll say about it that's not very interesting what I'd like to do is move the frontier of what is considered automation have a neural net come up with specifications for the certor approver for instance have something like that have deep automation something that will really push what can be automated versus what's now delegated to humans and that can get us to the next level with much much greater automation some good security insights encoded in our tools but at the same time the automation will come from llms or something similar so there is there's definitely a very a wide open

Horizon for things that are going to happen in the next two three five years lots of potential for innovation thank you um taking this from a little more of a Visionary perspective back down to really really minute we touched a lot on false positives just now I'm curious if anyone else has any opinions feelings thoughts about false positives they don't matter oh interesting no I'm I'm being a little provocative but they obviously matter but they they start to matter a lot at above the 90 rate that's the surprising

thing you know give me a true vulnerability uh one out of ten times I'm still happy if it's a true vulnerability that's a that's tremendously high value in this domain so I don't care if you give me a few false positives it's not like I'm trying to get the attention of a board programmer programming iOS applications and now I need to give them like extremely low false positive rates I mean that's not the game here the game here is give me high value vulnerabilities even if nine out of ten times they turn out to be false now if it's 99 over 100 yeah that's way too much but you we can suffer a lot higher in terms of the false positive rate so

that's why I don't consider this to be a huge problem that's my controversial opinion I I had warned beforehand and do you think that Tools in this space all seem to share that opinion or do you think different tools and different segments of this space have different reactions to false positives and this is kind of for everyone including you I have to qualify first of all sorry and that's the last thing I'll say it depends on the severity of the vulnerability if the tool is ambitious enough to go for severe vulnerabilities uh and end to end that's when the false positive rate does not matter so I think most people will agree to that but so false positives can actually help in

program comprehension our tool for example is iterative in nature so you will eventually be able to eliminate most of the false positives but uh in that process you are focusing on the parts of your program that are the riskiest at least in the eyes of the tool and that in itself can help make your audits more focused your testing more focused and reduce errors in an indirect way I do think um in terms of something like results from like a static analysis tool going into like if you're just kind of running it on code and seeing results it's

possible that like a lot of those are false positives and maybe one of them is a true positive but still even then triaging those results and going through them and actually really understanding in depth what the system is supposed to do and how it's supposed to work is a practice that kind of needs to be done because um that tool can essentially help you determine those vulnerabilities and those risks beforehand I think there was a recent study that was just a release that was a few runs based on previous code bases where Slither was run it could have saved like 150 million in funds I think

that goes to show that developers really need to take results from static analysis tools carefully and really understand what are the true impacts of even if it doesn't affect your code base right now how will it affect your code base in the future once you do a code upgrade once you do a migration and actually understanding like end to end what that impact has on your system because there's a lot of things that can fall through the gaps and so it takes a lot of time and effort to really go through those and triage them I think on like the ergonomics and FX

side of things false positives can be bad um just because you know if you keep running tools and they give you these false positives that are low severity you kind of get desensitized to it and almost like annoyed sometimes you know like if you ever run npm install you'll see it tells you there's like five warnings and things you should fix but like how many of you guys have actually looked into that and so you know that's possible that for some of these tools that can also happen where you might just be like I don't want to run this anymore it's like too much noise so I think that's definitely one concern that we should have when it comes to false positive oh sorry so one of the other uh

ways of like getting rid of false positives is to use maybe some kind of symbolic execution so that after the tool gives you there's uh possible issue here you would want to have a concrete input or like a concrete test you know which exposes that vulnerability so maybe there are ways where you can combine static analysis with some symbolic execution to improve the the false positive rate so so I totally uh agree on that um the fact is most a certain point most advanced security analysis will actually directly include symbolic execution Android inside

because if you want to be able to find some complex vulnerability you will be able to maybe suppose or at least get a range of a possible value at a certain point in time so what I think is definitely valuable is symbolic execution to actually get a closer look of what is really happening and I think something really important to have and it's typically the first time I saw that was in slitter is the confidence of the vulnerability and I think it's basically what potentially matter the most if if you have a critical and confidence on that is really high it's not the same then are critical with a low confidence so

maybe a first step for the developer to do is actually to take a look at all the vulnerability with a high confidence score and then go to the to the rest yeah I definitely agree that static analysis should be used in combination with other tools I would also say like if you do actually find a true positive with slither or any other tooling that should be a sign that you should be fixing that vulnerability that you should be fixing that patch and probably writing like a unit test or some kind of fuzzing test even just to make sure that that's no longer exploitable so that in the future when you're updating your code you you've checked to make sure that that like it doesn't repeat itself

and just making sure that you're like you're always running those tools like as you change your code and not necessarily just like write all your code first and then do the Slither and like run static analysis or formal verification or fuzzing just because once you get to that very end most likely those static analysis results are going to be never-ending fuzzing is going to be very difficult to get up because it's such a large code base that you may not have considered like what are your invariants beforehand and so ideally if you are running these tools like as you're creating your code by the end you shouldn't really have like a long list per se of like findings

that you should be like keeping in mind within your code base it should be relatively succinct because it's something that you've thought about as you're building your code and do you find that's how developers tend to use these tools or what workflows are you actually seeing in real life we definitely like them to make sure that they're doing this throughout this security work process um I think it's it very much depends on the project and especially if a project is set up with thinking about their invariants beforehand thinking about like what their code is supposed to do it's noticeably much easier to get

fuzzing set up and it's much easier to triage results because there are not that many results um so it's you can vary you can there's a very noticeable difference between those projects and um from that it becomes from the Project's perspective much easier for them to analyze potential vulnerabilities or like Risk with like external protocols um and so from their side they have kind of a more they have a safer posture which can help them essentially future proof their code but also just make sure that their current versions are safe yeah a lot of developers have that misconception that you should use tools

as the last thing in the development life cycle right before even right after Audits and actually the biggest value you can get from tools is from using them from very early in the process it just gives you more economic value because the mistakes that you have especially in your design are going to be a lot more expensive if you find them later in the process rather than early if you're going to do it anyway please do it earlier I would also add that um especially for um growing like after you've written your code going into like audits or bug bounties or any kind of um other eyes of

on your code at any third-party opinions having run Slither and having the fuzzing set up means that other people looking at your code can then focus on very complex bugs that integrate with protocols or different contracts and so the quality of those bugs are likely much higher those of like results from static analysis because these two these tools will help you find kind of the low hanging fruit and maybe complex interactions but it means if you've already run those tools when you get to kind of having that third party look at your code that it's much easier to

actually understand what's going on but also identify potential books okay I'll go back and push back a little on the idea that a static analysis tool especially can give you good estimates of its own confidence I mean confidence is a great thing but we need to be really careful when inspecting results at a certain level of confidence and I'll explain what we are noticing and kind of why this is happening there's this old anecdote in business settings you have professor and the professor is teaching her students everything about stock picking and hear all the criteria for seeing whether a

company is doing well and you have your PE ratio and you have what the executive team has sold recently and you you have whatever criteria you want so the entire class is learning about all of those and professors like okay so give me an algorithm for finding the best stocks and the students come up with something and they State their criteria and they run the algorithm it's like there are no stocks like that and of course there are going to be no stocks like that in everything that has money behind it if you only focus at what you can be certain about if you only focus at the highest confidence you're not going to find anything and it's the same with with analysis warnings if you only look at high confidence basically that's clueless

code most of the time so it's not going to hold any money if you do a high confidence and holds a lot of money that's an extremely rare occurrence to find anything so oftentimes one needs to inspect a lot more than the high confidence warnings why because the analysis itself the automated analysis it knows of one thread and it knows of a guarding pattern against that threat and it thinks it sees that guarding pattern but it's not really there and you have a real vulnerability and a human needs to come in and find that even though I see a low confidence warning this is really something that looks a little suspicious

so yes definitely we want analysis to tell us how confident they are yes we want to focus on the high confidence but only if we have limited time for inspection if if this is really a project that we care about you need to inspect nearly everything that the analysis tells you about because this is a lot of money and the analysis is just doing its best and it's just a machine yeah I want to refer to a few things that uh Janis have said before about confidence in terms of formal verification so we said before that maybe in the future AI will produce specifications

so um there is a running joke that formal verification makes sure that your code in your specification have the same bugs and that's a true risk that you can have with generated specs it might not be what you mean them to be and that ties into the confidence problem that we faced and we try to solve it using a different way with mutation testing the basic idea is that you take your code to Lady code and include a random fault in it and we call that a mutant and the idea is that it resembles a code with a bug in it so it should fail somewhere along your testing suit maybe

static analysis will find this mistake or fuzzing or your unit tests even and that gives you some estimate of confidence seeing how many mutants were caught we say well killed and how many were not and it's pluggable with um all kinds of different tools is there a chance that maybe you generated specs at least will be more different than specs written by the people who wrote the code like it it seems like it could be an interesting moment of diff although maybe the generated specs are like so kind of average in what they generate

that they also incorporate sort of the most likely kind of bug but I don't know any more thoughts on like generating specs so um yeah I guess that will depend on the exact AI technology that will be used to produce these specs I think that there are two main problems one they're going to see only specs that humans wrote and uh well most of the specs are are not catching bugs right and the other is that we see that the more uh tailored the spec is to your program logic um the more kind of unique bugs you can find if it's a generic bug there are other technologies that are very good at

catching bugs like static analysis and you're going to to miss out of some of the edge of the technology if you cannot really um find something that's very different from the other programs that have been used to train the AI okay great um thanks for coming with me on the small AI tangent um okay so I'm curious if there have been any developer responses to results from either your tools or tools you've seen that have been really surprising to you or taught you something about your tool or the state of tooling more generally

yeah there is always some funny responses from developer to be honest like you find the bug they fix it and they say it's not the bug but why did you fix it if it's not a bag but whatever so this kind of stuff happened all the time what what happened as well is that the tool is too specific or not specific enough and again that's the main issue with again if you want to have eye confidence on I don't know around from C we're gonna really be specific on which type of front Francie have a high confidence because based on the CFG the evm bytecode and so on we can affirm that

there is a run from debug but if it's like another variant of runs on C if you if you have been there for like five or six years there was only one kind of run from C back then um and not multiple of them so definitely the tool at the time was only able to find the let's say the Dao roundtransi but was not able to find the new read-only run from C or whatever that we have right now so there is definitely um updates to do on the tours and um and the fact are the developer some of them think the tool is Magic and that we will do the all the job for you and that's my conversion and my

controversial opinion about formal verification because everyone wants to have formal verification but for sure if I'm formally verified that one equal one it doesn't mean I'm formally verified so um for me that there is also a notion of let's say a timeline applied to tools static analysis tools should be kind of one of the beginner finding all the longing fruits then you are doing fuzzing and then you are maybe doing symbolic execution and then you are doing a formal verification but it shouldn't be the other way you want it shouldn't be like a mixed up in different order it's really a process

and basically that's what is I think missing in most developer mind I think one common question that we get around when we do like fuzzing workshops and sharing essentially how to fuzz is that if the fuzzer passes um then it means there are no bugs which it's it only means that there are no bugs within that iteration and that those attempts that it in those tries that it attempted um I think the other thing is that um the the invariance in general any tooling that you use to test your

invariants they're only as good as your invariants are and if your invariants are wrong then your tooling isn't necessarily actually going to tell you much about your code which is why it's so important to actually start with like what your code is supposed to do and figure out what those invariants are I mean ideally before you even start building it but um that gives you a better idea of what you're aiming for and what your what your code is supposed to do and only then Contours actually be useful and helpful in determining whether those actually hold um sometimes users on code saw will use it to search for dependencies which

wasn't really something we like anticipated but uh it lets people dig into like the supply chain of the dependencies which you know we don't at least in ethereum there's no like widely adopted package manager and so kind of highlights like the need for some of this basic infrastructure for developers that you know it's very common in web 2 programming languages so we're kind of missing a lot of that key infrastructure because I think a lot of the focus is on you know the logic and the contracts themselves when it comes to tooling at least which is you know of course very important as well um but yeah it shows us there's still some more work to be done on the infrastructure side

so one of the reactions usually when uh yeah I try to show like a formal verification tool as uh that okay this is great so I need to write a lot fewer tests uh but that's kind of not the the best way to go forward because in some sense tests are specifications right because if you have a code with a lot of corner cases well crafted tests really tell you what what the spec is so uh yeah even with all these verification tools and static analyzers tests are still like the the first thing that you would need to to write

so it's like these tools are not like Panacea so they don't get rid of the need for writing or tests I I don't have exactly good stories of user feedback but mostly comments on things that were said earlier and and also controversial statements uh so first of all I'd like to point out that the tools are continuing right uh I mean there is uh perhaps formal verification against specs on one end but everything else is is very much a Continuum it's not just the static analysis static analysis and symbolic execution and

fuzzing could all be part of the same tool like in our case they typically are deep symbolic understanding of the program could very much go inside the static analysis tool it could be trying to derive specifications we're trying to do that one thing that I think might be a controversial opinion is that the the protocols that I want to use formal verification on are some of the worst written because I cannot understand the code fully in full confidence as a human and there I definitely want some formal verification tool where I can just write in terms that I understand the specification and have the tool tell me

yeah it's true after a deposit of zero the shares remain the same oh great because I couldn't tell that myself as a human that indicates really badly written code so that's kind of a controversial or negative opinion but we have to see that what we're doing in this space is was pushing the limits of tooling and their contribution to programming we are having very very Advanced tools and this is very good to see we are seeing formal verification fully used in practice for protocols that manage lots of funds now where what are the limits there we're discovering them in this community we don't exactly know it's not like other communities have done this other software

development domains have done this we are at the Forefront there we will see what can be the impact of all sorts of tooling on automating security of software since we've had a few controversial opinions already I'm just going to open the floor for more of them so bring your bring your best and most controversial opinions now I have a controversial opinion for developers probably not to my peers but if you've tried a tool and didn't like it or couldn't manage to use it well and it was actively developed for over a

year you should give her another chance most tools have had some amazing development in the last year or so and they could bear very little resemblance to the experience you've had before it's very easy to write things off oh I've tried it like a year and a half ago it was too complex couldn't run on my code you should try to do that again you're missing out um yeah completely and they actually should put that in the CI CD because the fact that the tool will evolve a lot will also potentially feinbergs in the future I'm thinking typically of your the studio

you mentioned that about the fact that slitter actually find bugs like on on some contract and if developer was using slitter they will they will have find the bug the bugs sorry the question I will ask is do the bugs that was detected in this Duty was actually bug that was already on the tool at the time the contract was available or is it like new detectors on slitter that actually find the bugs sure they did a close analysis of different The Depths between those contracts um so it's against the if I'm not

mistaken the current version I'm still there okay any more controversy we should have competitive teams I I can yeah I mean we are all against formal verification so that's uh that's a no not too bad what no I'm so my controversial opinion is yeah formal verification is there is way too much noise about that for not that much uh privilege in my opinion so it's a really really controversial opinion but for me yeah I mean it's something that is proven to be efficient and so on I also disagree of what

um you were saying previously regarding like we are completely new in this area like we are like on top of the game and so on I mean I think most of you in the room have take a plane to come here and I think typically the Aerospace plane security is kind of a top of what exists in terms of assurance make sure that if you're playing get any problem you will get multiple backup and so on who are not even close to that in in my opinion on Smart contract so there is definitely some room to Improvement and I definitely think we have still a lot of tools and stuff to to do and yeah when I'm not on top of the game

on that clearly not in my opinion I do agree that there's a lot of tools that exist for developers to use to make sure that their code is safe but then that puts the onus on developers to actually integrate them use them use them properly and use them in the way that they're intended and I think that's one area that um it's it's a very it's it can be difficult to do because people just want to keep writing code and keep building new features or keep building new things but just taking some time aside into thinking about security and thinking about how to write safe code while you're developing code goes a long way

yeah so if if I can defend a little the earlier statement and then we can we can get back clearly there are domains that have had formal verification in the past I mean uh in processors in Hardware uh subroutines have been verified routinely since the uh Intel bugs like the AMD square root routine has been verified uh control systems in trains and airplanes have been verified general purpose software development completely open that can do any calculations whatsoever it's not a closed control system has not been verified as aggressively as software in this domain so we are in in

to a great extent we are at the Forefront and I do believe in formal verification but I do think that the extent of its applicability and its overall impact in the industry is still to be determined we don't know whether how much it will capture of the security the Assurance of the overall space I mean I think everyone will agree to that but it's uh this the this community is making great strides towards popularizing uh formal verification with various uh companies uh here well represented but uh yeah I think the truth is somewhere in the middle uh there but when I said before we should have competing teams I meant perhaps the

people who will be convinced of the value of the tool will should not be the people who are developing the code in the first place just like we have coders and Auditors uh to some extent it should be for some kinds of tools not for all of them it should be coders and quality assurance Engineers something and I know that's kind of an old idea it's tired we kind of don't like the sound of it but you do need some sort of competitiveness there you don't want to always be trying to convince the person who developed the code alone you want to convince an adversary so to speak that's what I meant earlier yeah so another reaction to the formal

verification hype and maybe tying into the question about surprising customer reactions uh we've found out that for different people it could be a lot easier or a lot harder to come up with invariance or specifications and it seems to be somewhat of an independent skill uh towards a good code writing so people can be really good at writing uh complex or efficient smart contracts and struggle with writing specifications and vice versa and yeah I don't know if there is a good predictor for that trait okay I just want to leave like two more

seconds in case any last minute controversial thoughts came to the surface but it seems like not so much um Okay so we've talked a lot about smart contract security that's just been ambiently around but there are also many other layers to like the D5 stack right we have the protocols we have maybe some bridges we have wallets we have all sorts of stuff so what parts of the stack do you think could be better served by existing tools and how would you like to see that you know change moving forward I I think this the rest of the stack is

definitely under threat but it is very much a web 2 security issue not so much a web 3 security or device security issue so in a sense we all recognize that there is a need there but I don't consider myself at the Forefront of how this can be addressed what can be the next huge step in the web 2 security space in in anything that's outside the smart contract space anything that's outside the core crypto space let's say um so I can mainly speak um but basically for the in clients and auditing clients which is what we are

doing basically on a day-to-day basis so typically there is clearly like a tool on that both at the language level like um rest go and so on there is some toolings but nothing like no extra stuff for blockchain uh there is definitely a lack of tools for blockchain framework I'm thinking of substrate Cosmos and so on um so there is a lot of documentation and so on but in my opinion there is definitely a lack of tool of okay I'm building a substrate blockchain can you find out if I'm not like preventing any API publicly that shouldn't can you

verify a bunch of stuff and so on so clearly something is missing in the ecosystem and even in time of fuzzing I've been doing fizzing on layer one and chain for quite some time and different shell facing as well and typically this kind of stuff is something that is only financed by the foundation and the fact the foundation need to do the work and um and and put money on the table because of course a differential feather like the one I built with Sigma Prime become first is only applicable either if you are doing bug Bunty and want to

find works or either if you are the foundation and you want to find bugs on on your channel otherwise it doesn't make sense to to to build the tool as a product because it will be only usable from one specific scope so typically in such cases those tools need to be built by some people Finance by foundation in in the same way that Foundation Finance for example multiple clients to get diversity of clients so in the semis I need to finance these tools but it could it's not possible to make it a product on itself so it's more like pure research and development and and

securing the the chain itself and it should be the same for all of them I think they're generally many areas of growth that like automated tooling can extend into like for example for Bridges um yeah you can definitely test like the smart contract on both sides using like the existing tools but I think there's also a lot more room for additional automated tooling and like the Locking of funds on one chain the minting or minting on the other or vice versa and so that kind of ties a little bit into differential fuzzing in terms of like if there's a reintegration of like

different functions on both chains but generally just more kind of end-to-end tests and kind of being able to test more there there's a lot more potential that it's going to be very protocol specific and very dependent on what you're trying to build what invariance you want to actually hold and what you're trying to test is that it's not necessarily like a one size fit all just because of how unique and how different all of the existing contracts and Protocols are outside of just the realm of smart contracts yeah I think one area that uh could use some more attention is

it's kind of like fuzzy area of like behavioral security so this kind of extends to like wallets um you know having standardized ux's so you're not just like signing a bunch of gibberish like zeros and ones and letters um even to like standardizing you know Audits and package managers so that um users and devs and security researchers have confidence about what they're looking at and they can actually point to like what what things are being imported and what versions of code are being used um and so all of these kind of contribute Downstream to security and so you know like web 2 they have like this like audit uh standard called like sock 2 and so you know maybe at some point like D5 or crypto has its own version of sock 2

where it's like oh this thing is like had Slither run against it or Torah or whatever and so on and it gives a lot of users more confidence and actually helps us like push the industry to a better adoption because each user that has a very poor like experience getting rugged or you know just making some mistake like they're probably not going to come back so we kind of need to like dedicate some more attention to the ux of crypto and the security implications there I would like to extend Gary's answer that so I think it's very important to also look at uh security from the user's point of view as well so I think web3 in

general has brought in a lot more ideas and Notions about like access control with Notions of proxy accounts account abstractions and so on and it would be interesting to have tools which exhaustively uh check if there are any uh ways of accessing your account without having the the credentials you know so these kind of basically tooling which helps you to uh yeah to verify that the access control system works as intended great so it looks like we have about

five minutes left so I'm going to ask one more question um if I'm a D5 developer I'm starting a new project first of all how should I evaluate you know there's so many tools how should I evaluate what to use and how can I think about setting up sort of a long-term tooling pipeline I would say start with specifications start with identifying what your code is really supposed to do before you even start writing code that way you have an idea of where your target is where you're aiming towards and like what you're even trying to build

and then really just integrate security tools like Slither and Echidna into your CI pipeline just to make sure that every time you're updating code you're adding you've decided oh my code is going to support a new feature run Slither on it write a small fuzz test on it making sure that you're essentially up updating and making sure that that those that the static analysis results are triaged and the fuzzing is up to date according to what you're trying to build and kind of keeping your specs up to date I think that's the perfect way to start because if you start with that then you you're essentially growing a list of your specs

and like your unit tests and and your fuzzing test can essentially help with identifying what your invariants are and it becomes much easier to actually create like a mental model of your code base and identify like what and where things could potentially go wrong either in the future when you update it and like add a new feature or just like make changes to your code it gives you a much better idea of how you set up how you have set up your code and where like potential problems are are likely to be I would say first of all there's lots of tools to get started with a new project

right now or for developers that are just getting into the space or they're they're launching a new project so obviously they'll start from the free ones they'll they will run Slither but first of all you need to write lots of test cases and then you need to write parametric unit test cases like good things that do environment invariant based fuzzing and we have Foundry has an amazing facility for that best that you can get in almost any software development domain so you start from those you start by writing your invariants and having a fuzzer that knows about invariance generate tests you go and you run a static analysis tool and then you you are there and you've done the basics and you're thinking do I need to write

specifications do I want to write specifications am I skilled to do that we're already we've already eliminated 98 of the developers right there because at least in most projects there's not even sufficient test coverage let alone all the advanced things that we're talking about but if we're going to something more sophisticated uh yes you you then think of of all the a little more advanced maybe proprietary tools uh maybe writing specifications maybe using the Satora approver in a pay-as-you-go way or commissioning if it is going to be a project that has the budget for that but that's kind of the gradation but at the at the beginning level

there's amazing tooling already I mean I like I was saying before I've been uh very pleasantly surprised even by the I don't remember the exact terminology in the docs but the parametric unit testing in in Foundry just write in variance and I'll generate good tests for you within those yeah so uh I would say like the first thing is to start with the clear threat model and then also clarify the basic trust assumptions that you have when you're building uh the system or the protocol and there's actually a in in the tooling landscape there's a

inherent trade-off between uh Automation and expressivity of the kind of bugs that a tool can detect and it's you can't have usually both of them right so you either go for the particular use case that you have you either go towards like automation where you you get uh security guarantees but only for a particular class of bugs or if you want to verify like the consensus mechanism of the protocol itself then uh you would have to invest a lot more time and effort and it it's always yeah worthwhile to think if it justifies the

the time and effort that you invest in it yeah I agree with my peers you should definitely start early if possible try to use uh yeah the the more generic less specific tools first and one important thing that I want to add is that you need to evaluate your testing as you go if you find lots of vagina specific error fever code obviously you'll want to focus more there and maybe controversially if you don't find any bugs that's even worse for you because then you don't know you have more more unknowns for you like I would be even more paranoid if I can't find many bugs in my code but definitely

do some revaluations as your code matures and now remember to do this once in a while instead of saying hey I have no new bugs that's it I'm good to go not at all and I think also something to um for the for the beginner developer it's also reuse existing Library I mean we don't have anyone from open ziplin but I think they are a good example of basically some kind of best best practices that you should do there is multiple templates of contracts so there is a use huge chance that you can basically start from that and using what is already provided to you as a basis

and then just ramp up on top of that so I think it's also really important to actually take a look at what exists and is already secure by by default I would also just add uh not like in addition to not Reinventing the wheel just start small in terms of like what you're actually trying to build and don't just create one piece of code base that has like 15 different features and then um treat that as your proof of concept just because it's going to be really hard to understand how how is that code supposed to work and what are the potential impacts of a code base of that size so if you start small instead and start with like a

minimal viable product of what your code base is intended to do in the future and then by some version you'll have essentially what your code is end to end and you do that piecemeal it's much easier to actually understand what the impacts of adding new features and new code is great okay I think that's all we have time for so thanks to all the panelists thank you all for coming and listening we really appreciate it foreign