Bug-Free Solidity Coding Agents

Transcript

uh I'm here to distur you be disturb you and entertain you before lunch uh so I'm sure I'm been in this space for a long time and many of you are probably security researcher I just want to say some few words that I am actually uh representing and this is very different than the talk I gave for the terum foundation here I'm representing sata And so is a service company. We are actually providing a lot of services in this space and working with many of the client in this space. We're providing audi formal verification, obser design review. We are providing many many things. Uh I'm sorry doing a little advertisement. It's the last one. But

the idea in this product that we are launching now is that it will actually uh be something that way more affordable and it doesn't cover all our services but it's something that it's beginning and this is a product that we want to release and actually we'll release uh this week and it's open source and it's actually will include a lot of things. It doesn't replace audit or formal verification or something but it's the beginning of it. So please listen I will encourage question either before after the talk. Everything that we produce here is open source. We have been producing the sat prover which I think George mentioned sat prover people use it for solidity which is amazing. But I

want to point out that sat prover handles many things be beyond solidity. It handles particularly different virtual machine. The Ethereum virtual machine which is the first, Solana byte code is the second one, web assembly which is the third one. It handle many programming language including Viper, Vas and we want to actually build more. We are building more and we have uh we are extending this the set program. Okay. So actually this is probably something interesting uh that we need to think of and I'm not sure what is the solution. We are seeing everybody that the LLM the agent are getting better in writing code and definitely faster. They

can produce I don't know if you've seen the Ben example the people talk a code a huge code in a in a variant of C and they rewrite it in into rust in few days. It's amazing. I work in industry and we ended up writing like 1 million lines of code. It took us one year and we got many award of it. So people are really really writing code very fast with agent but now the bottleneck and I think we saw it in George uh question but the bottleneck is code review is testing. What do we do about it? How do we review that and maybe what do we do about it and what how do we how do we get into this domain that code are being changed all the time and new code is

generated and new code from old code or new code from scratch. So the solution that I'm proposing and in fact it's not any new it's uh when I started computer science which is long time ago this solution was proposed okay so it's called specbas based development it's one of the oldest idea in computer science you start with the prompts or something you ask the agent not just to write code to write spec and to write spec and code and the idea is now we have the agent is nondeterministic. The agent is doing all this smart thing. But we have a mechanism. We can check that the code and the spec adher. So

basically we we check that the code adhers to the requirement which are defined by the spec. Okay. And and the spec question is it written by human is it written by agent? How is it reviewed? But this is this idea of specdriven development has been around for a while. It's been around for a while. But there's a huge challenge in it and I actually love it when I give talks about formification when you ask people to write specs initial specs are terrible that writing by human and they ended up writing spec which is exactly simulating the code. Okay. So you do an assignment say X get five and you ask the the the

human what's the spec they say X is equal five. Okay. And you see now when people tweet that they formally verify, you look what they formulate verify. They formally verify exactly what the code is doing. This does not increase the security by any mean. But it's good for marketing. I agree. So this is what we want to avoid. We want them to write something which doesn't mirror this the spec. And the challenge is also that the goods back informal or formal it need to capture some interactions between different part of the system. This is what's sort of hard and it's hard for

human and at the moment is also very very hard for aging. Okay. And the the challenge is that LLM and we have seen it in the last few weeks and I'm sure we'll see more LLM generate code and generate spec and it will generate basically code which meet the spec but this code is not good at all because the spec is not good at all. In some is just making sure that the code and the spec have the same bugs. Okay. So what are we doing? We are doing baby step here and I'm sure many can do more but we are doing different things.

We are using offtheshelf coding agent like codex and others but we add these skills we call them FV plugin. They're based on our experience in the last eight years proving smart contract but we are going to more things and they're trying to leverage the things that we learn when we are doing formal verification. So what are we doing? The first thing that we do is property property inference in English. We at the moment use the agent but as a human we review that and we hope in the future they'll get better. We are using different agent. This is definitely the weakest part. But we are trying to help and I

give you a simple example later. But this is the weakest part. It's sort of getting to the good informal spec. The other thing we are doing and actually this is actually where LLM is getting better and we are getting better and it's surprisingly we have a tool that we build and we invested a lot of time and a lot of engineering to get it working but in it seems like and we are really surprised the agent is sometimes better than us the agent like we have a a solution of the formal verification the formal verification fail the agent can help us and it's amazing the ideas and I show you some but you can see more this is the FV troubleshooter so it's something

that help you to diagnose failure of the formal verification the other thing that we are doing which I think very important from security is to understand the quality of the spec because that is our biggest scary thing when work with client and we miss bugs in client we miss it only because of one reason it has nothing to do it's not a technological failure it has to do with are a human or or the developer themsel did not write the right tech so this is where we are trying to help we are doing some string we are also doing academic

work I think this is interesting the last thing that we do which we haven't done enough but we do more we are not actually betting only on formal verification we are also betting on testing we think that getting good test is as hard as getting good spec. If you ask to LLM to give you a test, it give you immediately many many test they are useless. It's basically they are simulating behavior of the code which is which is essentially very very simple and very very connected to the code. So it's unlikely to find the tricky part where many many things go together. So we are trying to generate test and we are actually pretty positive. What we did is that we took

repository for a client and we took the test that the human wrote, we throw them away and we are now generating automatically and since we have good spec we can actually generate tests which are as good as the test that produced by human. We believe this is a good saving for protocol now and will be huge for proto saving for protocol in the future because testing is expensive and getting good test is very expensive especially if this code is generated by LLM well have to be speed up okay so how does it go there's this property uh there's there's the the the agent it it

infers the property It gets the code and the spec. Then it use the prover. It uses our prover but in fact we can plug in other prover or fazer. We are actually integrating in lean and others. And then you see either it finds a bug. It's basically the like we seen in George talk. It finds a bug in the in the code which the agent generated or there's a proof or there's a timeout. there's a failure of the solver and then we use the the the the every troubleshoot. The last part is a spec evaluator. It checks the spec. If the spec is not good enough or if there is a bug, we ask the agent to generate more code. So you may have to spend more tokens. The agent generate code and then

you we check if it's correct and then we call the agent again and so on. So this is a loop around the agent that you keep improving the call depending on your budget and you keep improving the security of the code. Okay. So I wanted to give you an example. I have 9 minutes I'll make it. I want to give you an example. I use the simplest code and we have actually been using it with real code. For example, we took the other V4. We give it uh I think something like uh very expensive I should say. We give it like 48 hours. I think it simulate about half half of the properties that we wrote manually. Okay, we have to see. So it's interesting. We are actually investing in trying to

understand in retro perspective on project that we did things how can the LLM do it. Okay. So this is a a very very simple uh vault. You see the ERC here you see the the informat. You see there is a vault. You see the property this is what is given to the agent and you see as the result you see these are the properties that the agent get informally you see there is a property of the vote no one can withdraw when you when you have add 10% you see it gives you a property for each of the API calls it give you an informal property and you get all these informal property you see for an owner ro you get these all

informal properties from there You generate the code essentially like a coding agent that you're using now. You generate the code. You see it uh it it generate the code. It's the solidity code. It's it's standard. There's nothing any use here. You take the prompt and you get your favorite coding agent to generate the code. Here it's interesting. You see we take the informal properties and we generate CVL. I think this is what George did in his talk. It's easy actually. It's very interesting. The the the agent is pretty good in understanding CVL. At the beginning, he does badly, but you tell him about the the manual and it's

getting better and better all the time. It's amazing. It's something which for us was hard to teach our team, but LM is getting better and also understanding diagnostic everything. So you see the agent is generating a rule. Don't don't worry about it. It's look like solidity, but it's different than solidity. You see there is this assertion is essentially checking a property that you have here. You are checking that no one can withdraw more than the the legitimate value. This is interesting. You ask the agent to to generate correct code. The agent ask ask you what's correct. You mean correct is winning by the set approver.

So the agent you see it does it. It tells it's very interesting. It even explains very nice. It basically generate a code. Then it's called the set approver. It finds a bug. It explains a bug. Actually, of course, the set approver give you a counter example, but it's technical, but it's explained it informally. It's explained it in formally. You see there's this bug with higher motor mark and it's also give you the fix all the give you the fix. It give you the fix. uh and and it give you actually it's telling you that there is uh you see here there is and it's and it's and it's it's it gives you everything. It's nice.

Okay. And you see here that I I I'm unable to do it. My co-founder did it yesterday. You see the commit it uses the opposite. It's it's it's actually does everything for you. Okay. and and uh and you see the it fixed the account share and I I should show you the code but you see here that what happened after every operation it's there is this raise of high water mark watermark it's the solidity code is updated correctly so you see the agent using the set approver is able to generate this correct code this is great but here is what we need

to help you and this is what we help you with a prover. The first thing we do this FV troubleshooter once you fix the code the the prover is unable to get it because there are some limits. So the prover is unable to get it uh and and you see that the rule time out. So what happened is the agent is calling another prover which is called lean and proving a very interesting pro theorem about code. Actually it's very interesting. So it's proving something informally about the code and then using it to solve the timer. So in fact it's helping you in the formal verification process.

Okay. And the last this is probably the most important part of the thing. We need to understand how good the verification is because our fear is that people will do formal verification and after that they will have they will find they will have bugs. The purpose of formalification as far as we see is to prevent bugs. Okay. So here is what we do. We have three ways that we measure the quality of formal verification. I'll elaborate on on on all of them. One is called property uh property coverage.

The other one is the spec themselves. And the last is understanding how good the agent himself itself is doing. I think all of them are interesting. We evaluate all of them and we show you the result and you of course as a developer you need to decide what you do about it because you are owning the security. Okay. So what's the first one? The first one is probably I think the most important and most interesting one to understand what I told you before. How good is your specification? In particular maybe you can think about it in terms of coverage. How many behaviors are you covering with your

specification? So one way to use is mutation testing. We have other ways to do these are methods that you can use with or without LL and understand how many of the situation you are covering. So you see in this case we are covering 75% of of the situation. You can argue if it's good or bad. I argue it's bad. I argue and actually statistics shows that when you're not covering something close to 100% the value of form verification is not high. So you need as a human when you see this you need to do more and this is also our experience with project that we work with that project that use formal verification and proof and only

one rule didn't do anything interesting. So this is the first thing. It's basically showing how good your your your specification and one way to do it is for example change the code insert an interesting bug and see if it's that's what I tell people when they do audit with us try to insert bug see if it's caught or not. So you see here it's we are covering some bugs but not all of them and we have to invest in more informal properties in order to cover more.

The other thing which is also interesting is understand and here again the LLM is useful. We can also use formal verification understand for each rule how accurate how does it capture the correctness of the code. We call it here CVL faithfulness. Here you see also this spec that we generate for this talk is not great. It's not as good as the spec that we wrote for AR. It's clear but we spent nine months on AR. I want to be clear here. Okay. So, and you ask the agent. Actually, the agent is coming up with pretty interesting explanation why this pack is not good. I I leave it to you. But the idea is that cuz I'm running out of time, but the idea is that you are actually not capturing the

right properties of this code because the way it's doing and other things. And it's interesting the agent is actually helping you here in writing a better spec. And of course you as a human need to decide if this is if this is this is a a good or bad. But I still think it's good for you because in this process you get better spec and hopefully you get better code. The last part it's obvious but still you have to do it. It's you have to check how well the agent is doing. And of course this is issue of budget. In this case, for this dog, I didn't want to burn a lot of tokens, so I didn't run it a lot. So, you see the agent is

cheating. The agent is cheating all the way if it can. So, you see the agent actually it one one property is violated. And in fact, it's okay because it didn't want to run it again. And also, you see that uh it didn't verify there are time two timeouts. And of course, if you are not happy, you can run it again. You can run it again but it requires more token and you'll get better to you will get a better code. Okay. So I think I'm almost at the end. I have time. So uh uh I want to actually explain to you what you want to take from this call from this uh lecture. We have I've been of course working on formalification long time but I think

this is a very very exciting time for forification. I'm sure you have heard from other. So I think the the the most interesting thing from that and this is what we learn from people also in manual audit that the more complete spec you have you have a better code and the more understanding of this code the better and if you have a complete spec actually you can change the code as long as you maintain the spec and reviewing the spec is in many ways more important than reviewing the code. It can also allow you to generate test and many other thing. So that's the first thing and because of this as a human as AI we want to spend a lot of time in generating the

right spec because once we have the right informal spec we can generate code. So in fact we used to say that code is low maybe we should change the say spec is low because once you have the good spec we can generate the code. So we we as humans we the only way to review is code is by reading it. uh an AI generate code which is correct by construction using our approver or other approver also AI generate test cases once you have good specification AI can do many things for you that's the idea we are releasing this auto approver skill it has either SAS interface that you can do or it has a skill as an open

source and you can use it in fact it can give you even audit report it has integration with bug finding and AI audit and others. But the interesting thing here, it get this formal spec also get fast test. So it's get the ability that you can actually use and and ideally you can use it when you develop the code but you can also use it before audit but you can use it when you develop your code. Okay, I'm running out of time so I want to say we have this auto approver. Uh if you want you can just scan this QR code. This is a tool which will be we are releasing now we will support it we are we will actually it's it's for solidity but it will be

available also for solana for stellar for other domain it will also be available outside smart contract this is a tool that you can use to secure your code and also it help you in the formal verification process so this is the idea it's called auto approver I'm ready to take questions either here or later. Of course. >> Thank you very much. Uh so it seems the programmer's job is now writing and reviewing the specification. Right. >> Say it one more time.

>> That now the programmer's job is writing and reviewing specification. >> Exactly. Exactly. reading and writing informal specification and later of course sometimes reviewing formal specification because we cannot trust the LLM to to to to really even though in general it does a good job but we don't know and I I I must say sometimes also of course reading the call yeah >> so let's take some questions from the audience uh thanks for submitting I'll read the first question uh and it's here it's are you saying that generating specs from an implement mentation is not ideal raider you should generate specs from product requirements and then check

the implementation against it. Definitely definitely and what we have seen actually when we work with LLM they they they actually cheat sometimes when we when we show them both they cheat so he definitely I think the the looking into the the data I think I remember once that there was auditor I think it now I I'm I'm I'm bulling in his name but he's from consensus that saying that when he gets an audit he doesn't want to look into the code he first want to look into the spec yeah Nice. Okay. So, uh the next question uh will be this one.

How do we ensure that the LLM infer and test edge cases that may not be too obvious from a single requirement? Each sandbox arise from changing multiple operations together. So that's the beauty of formal verification. Formal verification rely on modularity. So ideally you have a spec of the procedure boundaries and then what we want we want the formalification to check the interaction between the different functions and so so we want to actually to to come up with specification for each module that's by the way an advantage of formal verification or in fact formal specification as opposed to agent we think on a model base. Okay.

Now, uh we have here a question uh from uh students. Can you give me a short uh advice to all students out here who are here to learn something uh and build future in cyber security web three. So question. >> So I think the lot of things about web three. I think web 3 is the most open domain. A lot of excellent material seware rare skilled a lot of most of the project is open everything is open I think if you look into recent forification uh project there some are good or some are bad but they're all open it's great you can you can look at it I think this domain is excellent for

student it's moving fast but I would advise you to pick one topic and follow it yeah >> very nice so uh let's uh mark answered and uh next question is about hallucinations. So uh what about hallucinations and novel approaches if any updates from like new compiles version ATC memory and orchestrations of agents I guess we a little bit answer that but you can >> so so so hallucination from what I understand these are the cases that the LLM itself because it's actually produced some errors form verification of course if you have the right spe uh

can can check it I I think there's a we have a a interesting competitor logical intelligence they actually trying to combine intelligence with formal with formal verification I think it's a big issue hallucination definitely but for from our perspective working with LLM especially working formal verification which is a very deterministic procedure the fact that the LM is nondeterministic is sometimes also an advantage so I would uh but at the end when you are working With such a tool, you have to have some kind of level of paranoia.

When it finds a bug and you understand the bug, it's great. When it proved a property, you as a human still need to understand what's going on. Okay. And now we have a question about models because we didn't discuss which models we should use. So there's a question uh do you think that decision models like Jeff uh can change the workflow? >> Yes. Yes. Yes. We have not invest enough about in this but it's definitely thinking Jeff uh of course think like thinking we at the moment in set because we are very very small and don't understand we are essentially integrating all model in fact you can plug in your own models but definitely

it's very interesting what people do in models for and forification or other models is very interesting very useful also in terms of reducing the cost our our tool At the moment I didn't tell you if you're using a very expensive model it will be expensive. >> Okay. Thank you very much. We are out of time so please huge applause for Molly. >> Thank you very much. Thank you very much. I'm here around and also our team around please uh send us message try this tool. We are interest we are eager to learn how good it does. uh we want to see actually and take a code that you are familiar with and try to run this tool and give us feedback. Thanks a lot.

>> We are also out of time for this morning security block. So thanks you. Thank you for being here. Uh it was a very pleasant experience and uh we both look forward seeing you on the next uh event. Thank you.