Securing AI-Assisted DeFi Development with Formal Verification

Transcript

[Music] Good afternoon and thank you for coming. I'm sorry like the previous speaker I've changed the talk uh but I think I made it more interesting uh for you to judge. So I'm not going to talk about how you use a formal verification to secure AI. I'm going to talk about the opposite. I'm going to talk about how to make use AI to make formal verification easier. And actually this talk applied not just for formal verification, it applies for fuzzing and others. So please listen, I'll be uh I'll save some time for questions.

So about me, I'm a co-founder of Satara. Feel free to ping me. This talk is actually not by done by me. It's done by three amazing people on our team. uh Naftali uh Yoslav and Yannes and they're not here but are available to answer questions. It's a small project that we have done we are incorporating into our open source tool. Uh we can give you the source already or if you want you get it as part of the open source repository of the set approver. So there are many many tools in this space and we think that this work applies to many of them. Here we listed some of them. So Slater is the sort of a

very mature static analysis tool. Fairly easy to use. The problem doesn't provide a lot of security. It's very very general. Also it's hard to use it for bugs and you can integrate into CI. Uh Foundry is a fing tool. There's also Enkidna. These are good tools. they give more coverage than static analysis but a bit harder to use. Then there's Kalin interactive term provers. Uh uh there's also audit agent which is a recent and many others. I'm sorry I didn't have to list them all but these are tools based on AI to find bugs and uh they actually I listed the one by nethermind but there

are others. I apologize and our own tool prover which is open source. This is actually a tool that we think it's very very usable for developers. It checks the code at the moment. We made it available for EVM, SVM and web assembly and it's basically give you high security and it's still easier to use. But the the purpose of this talk it make it even more easier. So maybe just sort of talk about manual what are the things that people are use for security. So uh obviously people are using manual auditing this is the standard and we know that auditors can find a lot of issues but the problem is

auditing it's a human process so it's errorprone and it could be expensive and time consuming testing fuzzing is great you can automate it but you miss some of the bugs and it's very hard it's also can can be expensive formal verification has been used in other industry for example safety critical system it's provide a guarantee but it's really really expensive in terms of human effort and computational effort and AI checks it's it's something which of course exist before but now with the AI it's getting more and more popular so what we want to do we want to integrate it into formal verification this is the definition of formal

verification come from Wikipedia it's this method to give you a guarantee about your code but we take from this the actually definition that was done given to us by Ernesto uh from BGD it's the mechanism that actually increase your security or your confidence in your code so somehow it's something that allow you to go to the unknown part of your code it give you more security of your code uh so it's increase your trust and this is of course a nice quote by Vital Talic this came sort of showed that if you use form verification open source you increase the trust in the software

and also uh to uh looking actually after using our approver essentially saying that this can do can be also useful for the Solana uh okay so for the purpose of this talk I'm going to do something which basically I'm saying formal verification is good for proofs but it's also good for bug finding and I'm going to show you that actually formal verification in addition to the fact that it used for proof it it's actually useful for bug finding okay so why actually do we want to use AI for formal verification and why is formal verification not heavily used if it's so useful so there are many answers

but I think one particular answer that formal verification is considered hard and a lot of people I've studied computer formal verification for a long time. They say this is sort of the hardest problem in computer science and it's hard from a computational perspective but it's also hard in terms of learning. Okay. So these are many things that sort of go to you that you are starting from verification. Probably the most difficult part is the mindset. You have to change your mindset. when you are hacker or when you are programmer you have some kind of adversarial thinking which is very very useful you think how do I break it when you're doing formal verification you need this adversarial

thinking but you also need to think about what properties is and actually some people say that the bad hackers are the ones which think about both but it's sometimes hard to find so you need to think in terms of what is the code is expected to do and then you can use it with with tools or with with humans to break this thing. So you need to think and and another thing that you need to do you need to think declaratively you need to think of what is this code as opposed to imperatively and we know it's not it's incomparable you know we think imperatively I go someplace I need to do something it's sometimes more natural but somehow and for example when we work with client sometimes we come with a

property we say we wish we knew it before we wrote the code because you have to come with this kind of properties and it's hard for people to do As a result, sometimes people use abuse formal verification. Our tools are that and there are many way you can abuse formal verification. For example, you can prove things which is tutology. You prove that seven is greater than five. That's great. But it's not saying anything about your code. And also diagnosing formal verification is hard because basically formal verification can do something very very useful to you. But then it gives you an example and it's hard for you to understand what it means. So that's why formal verification and we see some kind

of a learning care. Somebody learns formalification and it takes him or her some time. So what do we want to do in the purpose of this talk and we have only done baby step. We have actually added this AI based formal verification. The idea is a formal verification but not the human is writing the properties. The system is writing the properties. So the system is trying to infer the properties that a smart human is writing. Okay. So how does it work?

So we start with the with the general defi knowledge. We basically have a data base of information. We take the design of the code. We take the code itself and we also take any documentation that you have in mind. And this is actually where the smart part start. You infer a property. We have a very simple language that we which is you can think of something like swel or something like this. It's a it's a language that allow you things to write things that you cannot exactly code but it's similar to code. It describe the requirement on the code.

I'll give you an example soon. Then we use a normal compiler. We essentially this is not very smart but still you have to do it. You have to compile into the CV into our own domain specific language for writing the properties. And then we run the ser approver. This is an automatic tool. You can write it on the cloud. If it verifies the property you know it verifies. So if you trust it you increase your confidence in the code. The interesting thing what happened? What happened with this violated there?

We use the AI again. Why do we use the AI again? Because we want the AI to help us diagnose what is the problem because we want to AI to to explain actually and AI are very good but they are very local and they can make terrible mistakes but it's not so bad. We run it and we will check it. Okay. So basically this give you this potential exploit scenario that a human needs to invest to to check and then if this error is real then you in fact apply the manual fix and then you write the set approver.

So I give you a few examples as I said we are doing really really step at this point. So please bear in mind that we need to run it on way more examples but we have been running it on few examples based on things for the public domain and based on many audits and formal verification project that we have done. So this is a of course example everybody knows is the open zeppelin transfer. It's a baby example but it's good to show you what we do. So we take the code, we take the transfer function, we basically oops okay we take the the code we take the transfer function and what we do

we take the code itself and we hide it we don't show the AI the implementation itself because we want it actually to find something which is the intended behavior not the executed behavior but we show it all the other part of the code and then we also show of course the documentation and We ask the AI to infer what is the intended behavior of this code. So this is what we do. You see this thing. Okay. And let's see what it's inferred.

Oops. Some reason it doesn't move. No. Okay. So it infers very simple property. Uh it infers that the total supply is unchanged. It's still a simple property you see that and it also infers potential exploit scenario. Okay, it's it's infers that a buggy transfer might might increase the total supply with allowing it. So it infer both of these. It infers the spec and you see this spec is not actually written exactly in solidity.

Bear in mind we have actually some extension of solidity to express some things that to to to allow you to write the properties but it's not the full power of CVL something much weaker and you see this is what it infers it's a very interesting case but it's very very simple we also apply to something a bit more real okay oh sorry this is the code which is generated by our compiler you see this is satura verification language if you don't No satar verification language ignore it there's some boilerplate code it's essentially writing on the bite code it is details it's details think about it some it's some details but the nice thing about it you don't need to know that it's automatically generated

from the high level spec and I imagine you can do it for fer like founder and and kidna we have not done it but I'm sure you can do something similar okay so let's to look into more interesting example uh We work with client before they deploy the code. This is a beautiful client. We have been working I think for four years. Balance. I'm sure everybody knows them and we work with them together with other auditors. And we are proud of finding the most interesting bugs preventing the most interesting bugs. And here is a very interesting bug which we prevented at this point without AI with our humans of course and it's a critical bug. uh I won't be able to explain but the idea it's written in our

blog and actually acknowledged by the by the by the balancer team. It's essentially allow you to use the token in a way that you actually steal all the money. It's a very very tricky situation. I I wouldn't be able to find such a bug. Okay, how did we find it? So we ended up writing a property. You see we wrote a property. It says this is the property and essentially the property says that if you have shares you have asset to cover for the shares. So it's a very natural property and then you see we write it in our CVL it's an invariant. It's an invariant you can write it. So it's basically you see in CVL you write in variants which are

independent of the function. So you see that here we say that if you have uh total shares then you have assets. It's a very very uh sort of natural property and this natural property is violated in a very rare situation and the prover automatically find this violation but the human had to write this property okay so somebody in our team has to write this property or okay so let's see what the AI inferred so so the AI inferred something actually simpler the AI inferred that basically the the the amount of asset doesn't change. It's

infer simpler property and let wait a second and it's also infer exploit. It's interesting. It also infers an exploit. You see if the buffer asset could be changed in fact it's interesting it infers and it infers it of course based on history of bugs that happened. So basically this thing knows about many many bugs that happened. So the AI infer the property and infer also the exploit and you see this is the generated CVL code. It's technical. It doesn't matter.

It's basically generated automatically by the compiler. So it's interesting. This is a case that a bug that somebody could have found without using us at all. Okay. I can tell you with you could save money. Okay. So that's the idea. uh I want to give some time for question. So further work we want to use it internally. We are doing good job but I can tell you our audit takes us long time. I know thanks our audit takes us long time. So we want to shorten our audit and the idea is we're going to use this tool initially and after that add things by human and hopefully it will speed our our internal work. We also

want to open source it. uh we only use entropic there are many other llm we want to support foundry and enkidna and there are some things that you cannot write in this language for example and this for example properties of internal functions and things like that so I'm almost done I just want to before I go to the question I want to don't get this talk wrong so this talk doesn't prevent we still need auditing we still need fuzzing we need everything Okay, I'm not going to I don't want to confu confuse it. This talk is actually giving you an extra security layer. You can use our tool to get to use this AI

based together with our tool or fuzzy others. It just get another layer. I'm not proposing it instead of everything you have. And finally, I think it's interesting that basically AI allow us to do more automation of security. So, I'm ready to take questions. Please, please ask me some questions. Yes. [Applause] Yes. Hello. Thank you, professor, for this interesting talk. I just wanted to ask about the false positives. So, how often does it say that there's an exploit when there actually uh when a human studies it there is no exploit?

So, so, so, so notice that in this case and that's something interesting. Uh, somebody could think of formal verification and and and AI as complimentary AI is very very local but it it makes mistake. Formal verification doesn't make mistake. Okay. When we prove the property up to a bug in our tool, it is proved. Okay. And we have when we have a violation of it up to a bug in the rule it is a violation otherwise you will complain a bug in our tool. So we the formal verification has a scaling issue but the formal verification always give you the exact answer. LLM give you a lot of noise but but this noise you can you

can you can check. Of course it could be confusing if it give you a bug which is not understandable. But the the false positive are are are being uh sort of handled by the by the formal verification tool. Um very interesting talk. Thank you. Um one of the slides said your AI model already had uh knowledge of DeFi. Can you talk a little bit about whether you found an existing model that had DeFi knowledge or did you train one yourself? And if you did train it, how what what is the data set you use to train? Thank you. Yes, that's a an an excellent question. So the question is how do we get AI models? So it's very clear that

in many domain including us there's very small data companies like open AI they do ma a magic job by basically putting a lot of smart engineers to to collect this data. We are at the moment using very very simple data. It's based on all open source and it's based on the repository that we have and of course we have a little bias to use our thing because we understand it more but of course we we we we want to use more and we want to leverage community and at some point if we have enough budget we'll probably put engineers to to collect data and to to gather data ourselves.

Thank you. It was a very nice talk. Um, I'm just wondering, I think it's a bit related to the exploit question, but separately. How many of the specifications that were generated by AI were actually correct? Did they actually capture what you were intending from whichever function you were analyzing at time? So, does it does it generate a lot of uh completely garbage even things that are might not be syntactically correct even? So, so for us the one thing that we did for good and for bad we we picked a very very simple language for writing the property. So if you if you generate CVL you're definitely right. CVL is very expressive. It's allowed to write. We decided to to go about the long hanging

foot. So by definition the the properties that we infer are small. But I want to be fair with you. We have not done enough experiment to say I imagine you're probably right at some point. It depends also which audit we go and depends on which thing we go. I'm sure there will be some noise. I totally agree and we have to see. Okay. Thank you. Thanks everybody. Thank you for the talk. We will have this work very soon available. Thank you very much.