Harnessing LLMs to generate secure code

Transcript

Intro: can AI make smart contracts more secure?

Thank you everybody. So good afternoon everybody. Uh maybe it's a new community for me. So I want to ask you a quick question. How many of you have written a smart contract or know about smart How many of you have written smart contract? Amazing. Amazing. Okay. So this talk is relevant for you. But even if you uh uh uh so uh smart contacts are interesting and we're going to show you hopefully something very interesting related to smart contact in AI that John has been working in the last three months.

Okay. What's going on there? Not yet. >> There we go. We got it. We got it. >> Okay. No, it's >> We got it. Look. >> Okay. No. No. But I see it here. Just put it slideshow. >> We are doing it on slideshow. Really? Uh it's not slideshow yet. >> Slideshow >> then give me this. Okay. So uh what we going to show? We want to show you something actually pretty interesting that I think it's really surprising. So everybody thinks that you know we are in the age of AI and you hear that many people say that AI makes code less secure. But in fact we're going to show

you that it's not necessarily the case. So what is the oops it's going too fast for me. So what is the situation in the this area of smart contract? I'm sure you have already had. So basically what happened in the area of smart contract there are these hero developers. There are developers that are very very smart and they are developing these smart contract and usually they are it's a very very lucrative job if you know how to write smart contract and there's huge money spent using security f including our own that actually makes the code secure. The interesting thing is that even if you do all these security

Why smart contract security remains hard

including auditing, fuzzing, formal verification and many techniques, people are finding bugs and when you look into the internet people say LLM will just make things worse because it's going to generate more code. It's going to generate more buggy code. It will make the task of the hackers really really easy. So is that the case? So in fact in this talk we're going to show you that it's not the case. We're going to show you that in fact it could be the opposite. It could be that LLM despite what everybody thinks and vibe coding which is probably the worst thing that somebody say is not so bad because VIP coding could be combined with what method called formal verification. And

for those of you who are not familiar formal verification is the art of making the code secure and making formal verification and the idea is formal verification and LLM they go along together in some sense they are complimentary the LLM is good in sort of anticipating some things and formal verification really know what the truth is so in this talk we're going to show you how you combine it together and John has built a system to do that So what is the main idea? The main idea is actually pretty old. It goes the way how we usually develop cycles in software. We have a a a circle of developing software. We start from the

Spec-driven development and catching bugs earlier

design. We go to the implementation. There is testing. There is refinement. There's all of it. But the issue that there are bugs which are fine there. And these bugs are actually making it and these bugs are identified usually too late. So what we going to do we're going to add some spec into the domain. We're going to expect the the ability of the user or somebody to write what is the expected properties and this will allow us to find the bugs earlier and also to make a guarantee that the code does what it's supposed to do.

It's not moving. John, why is it not moving? Okay. So why are why is it interesting now? So what's going on now? There are two things. Of course, if you look into this idea of spec driven development, it goes back to the early ways of computer science. People were saying write starting by writing the spec. But there are two things that change. Formal verification tools are becoming readily available. For example, we put Sertora which is a tool that almost every developer can use and Amazon put a a wonderful tool which called LIN 4. So there are these tools that can allow you to use form verification by engineers and on the other hand the LLM is getting

Combining LLMs with formal verification

all the time better. So that's why we can do this uh in a we can combine them now. Okay. So how is it going to go? So what we're going to do, we're going to allow you to do this provably correct vibe coding. So the user start with the specification. The specification includes some formal. It includes some interface. It includes some document. We give all of it to the LLM. We give all of it to the LLM. And the LLM is smart.

It doesn't get the whole code, but it gets the beginning. So it get this of course you give it a prompt and you say and the prompt is something that we engineer internally in Sora. Now we have worked and we engineer internally the prompt and it says generate this implementation that satisfy things and it for example you give some kind of spec based on what you expect. You get a code in solidity. This code is not perfect but it's the start and then what we happen we run this code along the spec and this is the prover. This is technology that you can have and he can check the bite code. If you are lucky and you get the proof that's great you get the proof the LM got it right from the first but this is usually not the case. Usually the LM never get it right

all the way. So this is why we run so it comes from bugs and the idea is tools like Stor they give an explanation they say you this is violated under this condition and then we feed it back. there is a feedback loop. We feed it back to the LLM and we say look give us now a code which does not have this behavior that was there and the LLM keeps going and then again we run it and after several iteration the LLM get it right keep going. So this tool is a used to be called a very safe but for the purpose of this call we call it composer. It's a technology that we are actually working on. It will be released

Composer: feedback loops between LLMs and provers

and you can use it to generate at the moment it's for for solidity and EVM but we can make it for work for other things. Okay. So the rest of this talk I'm going to uh transfer to my colleague John Tommen who actually built all this technology and he's going to show you how to build it and we actually prepared an example for you. It's not a real example but it's a contrived example that allow you to appreciate this thing. So take it John. >> Thank you. Can you all hear me? Is my mic on?

>> Yeah. Can you all hear me? Perfect. >> Can you put John on the >> Can I get my mic? Maybe. >> No. No. I can't take that. Wait. I think. Okay, perfect. We got me. Perfect. Uh, okay. So, as Muy said, this isn't working. Yeah, there we go. So, our contrived uh uh AMM is what we're calling the collective compensation constant product pool. Uh for those of you familiar with DeFi, this is just a simple constant product pool with a twist. That is larger withdrawals will incur progressively higher and higher fees. So, we're effectively redistributing large gains to the remaining uh liquidity providers uh socializing uh big gains. Uh now note that this is a novel idea, not necessarily a good one. In fact, we've cho perfect perfectly, we specifically

Demo setup: a novel AMM with progressive withdrawal fees

chose something that no one has done before uh because we want to show that it's able the LLM is able to generate novel implementations. This is pretty laggy. So perfect. So as Mully said, uh part of the input is a natural language specification. So this is a design document that we cooked up for the CCCP pool um written in natural language just specifying the behavior that is expected for uh these kinds of uh this this pool. But we also include this formal uh specification that formally says what the pool must do. Um this is written in a language uh called CDL which is a verification language and this is sort of one of the core rules.

It basically says that uh bigger withdrawals, so LP token 2 being larger than LP token 1's should give you a larger penalty and that's so penalty 2 has to be bigger than or equal to penalty 1. This is just one of many rules, but it is representative of the kinds of rules you would write for a D5 protocol like this. So how do we turn this into a synthes uh a synthesized implementation? Well, if you remember the doc uh the system uh diagram that we showed earlier for composer, this is our instantiation of these three inputs. And I am now going to play with fire. And here we go. This is an interface that we built for uh the uh debugging this tool and for seeing how it worked. And we actually see there is a fourth input

Extracting requirements from docs and formal specs

here which are a bunch of natural language requirements. Now the user did not actually write these. These were all extracted from the uh system document. And uh so before we ever actually start running the LLM to generate code, we first just feed it in the rules and the documentation and say uh analyze the specification and identify any requirements from the system document that aren't necessarily covered by the spec, right? because it's hard to write formal rules that cover every possible behavior. But you still want to make sure that the implementation hues as closely to the system document as possible and out of this comes things like the implementation must ensure that the first liquidity provider etc etc etc and these this list of requirements is fed

in as well to the LLM. Okay, so one thing we all know about AI is that it can hallucinate, right? And even outside of hallucinations, it can very easily make wrong assumptions or get stuck into some local maxima. And so we need to have some correction mechanism. We don't want this running in 200 loops thinking that misunderstanding how liquidity is supposed to be managed within a pool. And so what we've done is we've added a human in the loop feature where the LLM is allowed to ask the user questions. So uh should the implementation do this or that? And then the user can provide free form natural language guidance back to it. And so we can see an example of this here. Um, nope.

Human-in-the-loop corrections and spec refinement

Uh, which one was it? So yes, uh, this is an example of the question. Uh, no, it's not. Well, whatever. Fine. Never mind. We don't have time for this. So, uh, this is again very commonly called human in the loop. Okay. So remember one of the inputs is this specification and writing specs is very similar to writing code. It is not a foolproof process. Like all code artifacts, specs can have bugs. And so do we need to have perfect specs from the start. Does this require you does this basically change the problem from uh writing perfect code to writing perfect specs? Because then we've really only made kind of a lateral move there.

And the answer here is no actually. uh when the LLM gets a counter example and an explanation of the bug that comes out of the uh prover theory and say well hang on the spec is saying that I shouldn't do X but the spec document seems to say that I should I think the spec might be wrong and so then the LM is allowed to ask the user I want to change the spec and then it provides a diff that describes the change in the specification and crucially the user has to approve this the spec is the guiding light for your implementation And the LM is not allowed to arbitrarily change it. You have to approve it. And you can of course also reject it and say no the spec is right.

You are wrong. Fix your implementation and it will try to adjust to that uh specification. Or you can give it some guidance to say please uh refine instead and do this make this small tweak instead or you can accept the spec change at which point uh or excuse me this is uh basically LLM powered spec refinement. And this is by itself quite useful. we found for taking an initial spec and just seeing putting it through its paces. Does this actually describe the implementation uh that we're working with right here and so uh after this uh refinement we take the new rules the new specification that was generated by this uh proposal feed into the prover and then the process continues.

Handling incomplete specs and missed design constraints

So, uh, I just asked, do we need to have perfect specs from the start? And I argued that no, the LLM will help you go through any, uh, spec mistakes that you might have, but are we actually requiring that you have complete specifications from the start? Do you need to have your spec 100% upfront? Right? So, let's work through an example actually, as I described to you, has a problem. We implemented it. We got some generation. We got some code that came out of it that implements the specification and the requirements document and big withdrawals definitely incur progressively higher fees, but nothing stops someone from just doing several small withdrawals in a loop, right? Oopsie, we forgot something.

There was a a bug in our design, right? And so the solution here is to refine the specification. We can add this new rule to our uh the specification file that effectively says uh in the same environment which defines the current block. If you try to withdraw twice in this same environment, then the second attempt to withdraw reverts. Okay, great. We are able to update the spec, but we've already gotten our implementation. Maybe people have started to review it. Maybe people have started to build components that interact with it. So, do we have to start over? Do we have to take the old spec, add this new version, and then just start the whole process over again?

Meta-iteration: updating existing implementations safely

Do we have to answer all of the same questions and learn this new implementation, rebuild everything that used to interact with it? And luckily here the answer is also no. This is something that we call meta iteration. So we can take these refined rules and uh basically feed in the previous implementation which actually usually consists of a lot of files. This is the implementation that came out of a prior successful run. We also include some memories that were generated by the LLM in the previous generation step. It understands it remembers the answers to the questions that you or the qu the answers that you gave it when it asked a question. It understands uh the spec better because it has asked questions to uh refine its understanding. And then we feed this into the LLM as well. And we also of course adjust the prompt

slightly to say please update this implementation with explicit instructions to try to make these changes as minimal as possible. We don't want the LM saying I see I should rewrite everything. Because again we want to try to keep these changes minimal to make it possible to keep working with this as part of a larger software development pipeline. And then yes once we've sent in this prompt and the uh this in uh this uh old implementation the process continues like usual. So in summary composer is a mostly automated code synthesis tool. Again the mostly here because there is interaction with users for help or for potential edits and whatnot. The code is verified against the final spec. The final spec because that is what you've

Summary: verified code synthesis with user guidance

refined with the help from the LLM. And we also have this feature for meta iteration when you realize that your AMM has some crucial design bug or maybe you just want to add new features or whatnot. >> Okay. And this I will hand it back to uh Mully. >> Thank you very much. It's not working. It's not working. >> No, just I'll I'll advance the slides. >> Okay. So you continue. >> So thank you very much John. So let me just summarize and then we will be love to get some uh questions. So I think the take away from this uh uh we doing baby step here and the I think we presented it to several developers and don't be scared if you are a developer you still and you're a good developer you're going

to get a lot of work this is not going to eliminate developers but I think it's it actually makes an interesting case that somehow the AI when it's instructive instructed properly it can actually generate code which is almost right and is the LLM it can get all the way right. It's also interesting thing for formal verification. We have been in the last seven years Sura is actually celebrating seven years tomorrow and we have been in the last seven years trying to verify some of the most complex code in the smart contract which is still uh simple software. But the idea is that often we find out that formal verification comes in the too late in

Why formal verification should move earlier in development

the development process because we we are getting a code which is very complex. It's all spaghetti. It's not modular and it's not amenable to formal verification and what we think is with this kind of approach we can always maybe have the best of both worlds. So the ingenuity of the programmer is still in the play but I think what happened is that we know that in all code there are corner cases and corner cases is hard and this is actually where formal verification is very good maybe it's a rounding error maybe it's so some kind of corner cases so basically the idea that you have this invariant or this specification they serve as kind of a

guardrail for the development and the LLM M is learning things more and more locally. The interesting thing is that LM here is playing several roles. It help you in writing the code. It help you in writing the specification and it's not actually contradicting. So we at this point we are uh willing to take question. Thank you very much for listening. Thank you very much. And the credits uh beside us I want to give credit to Leo Openenheim who is here as a security researcher and Joseeppi uh GM Mari he's in our team and he he helped John in building this tool. They helped John in building this tool. Thank you

Q&A: does the LLM/prover loop converge?

very much. >> Amazing. Thank you for this amazing talk. >> Um >> we can start a Q&A session. So if you have a question please raise your hand and our volunteer is going to give you the microphone. we have in the middle row. >> Hola, how are you? So, um you presented this sort of loop between LLM and coder and um if failing then get back to the LLM generate etc. Is there any formal guarantee that this converges?

Uh, no. You could, you know, in principle continue to adversarily give the LM different guidance. You could say to do one thing and then decide afterwards to do a different thing and keep doing this again and again. The key here is that the LM is explicitly prompted to ask the user for help if it thinks it's stuck. Now, again, that's still relying on the LM to follow this prompt, and you know, we all know how that goes. But um there is also the possibility to interrupt the flow and try to correct it if you see it's basically getting stuck in some local maximum and it's not asking for help. It's just something we didn't have time to discuss in the slides.

>> But we we can actually show you at least one case we had in Sattor for example we had a lot of specification for ERC and the tool told us that these specification are wrong in the sense that there's no way to satisfy them. So in fact it found a bug in our own manual spec because the idea is that right the LM >> so so you are obviously right because in fact there's a loop that the LLM the formal modification and the human okay so and and and we can all get osillate but it's interesting that we are all helping each other if we are operating correctly right >> thank you and are you aware of any sort of theoretical framework to understand

Theory behind synthesis and counterexample-guided refinement

this better Yes. Yes. Yes. There are a lot of uh so you the question is are we aware of theoretical framework to to understand it better. So the answer is yes. There's a lot of work in in automata theory and others about synthesis. There have been a lot of theoretical think about synthesis going back to logic quantify elimination but the issue with LLM I honestly I don't understand maybe John but they're working very well. So uh there are things that we don't understand but practically work very well and also we are using SMT solver which also a bit unpredictable. So yes there's a lot of theory the theoretical result explaining when can you synthesize or not but yeah

you want to >> yeah yeah this is actually a instantiation of a general technique from synthesis called uh counter example guided uh refinement where essentially you have something that generates code and then you check to see whether or not it sat does what it's supposed to do and if it doesn't that goes in a loop in this case the thing that proposes the code is happens to be an LLM but this is an instantiation of a very particular technique that's been discussed in the code synthesis literature for I don't know decades at this point >> right yeah so there are work in counter example synthesis and automata theory a lot of people on synthesis but we think it's unique because of the the the practical usage with the prover and the practical usage of LLM but if you look into the programming language literature

Closing thoughts

there's a lot of thing even Amazon now announced that they are working on a tool similar like this I think actually Okay, we're out of time. Uh, let's give a big applause. >> [applause]