AI Composer - Safe Vibe Coding

Transcript

Good afternoon everybody. I'm excited to tell you about a new tool that Certora built, which is called Round About. So, many of you know about Certora as providing formal verification, which is a very advanced technique Today, I'm going to talk about a much simpler technique that we have implemented in an open-source tool which you can download and play. So, please listen and we'd love to get feedback. So, this is a a joint work. This is a team work in Certora.

I want to point at Julian Dolby, who is a scientist from IBM Research, who joined us recently. I want to point out uh Yaroslav Bendik, who run our R&D. Nurit Dor has been with us almost from the beginning. Shelly Grossman, who is my co-founder. Chandra Nandi, who is leading the R&D in the US. Leo Oppenheim, who is a security researcher. We have a large security team in Certora. And John Toman, who is a senior technical developer. So, all of this is a is a is a is a team work.

And the problem, I think, in the area of the crypto is very clear, but it's actually not specific to crypto. The idea was that as a human and in finance, we think about math. But in fact, in reality, computers, especially in the age of cryptography, they think about bits. So, there's a gap between the two of them. And this gap has nothing to do with blockchain or even decentralized finance. And this gap leads to errors. And these errors are very, very tricky in in in cryptocurrency.

And the question is, what do you need to do? Do you need to round up? Do we need to round down? Sometimes the answer really depends on the application, and there is no solution. So, I'm sure you heard, there have been quite a few hacks relating to rounding errors. And you can take a look of on wrecked. Again, these are not blockchain specific. I took the ones here from wrecked, and you see several one of them. You see the big one by balance there, Kyber Swap, and other. These are all rounding errors. So, they are effects of rounding errors, which are actually exploited by hackers. And the purpose of this talk is to try to prevent them. Of course, you can use methods like fuzzing or formal

verification, but this is supposed to be an easier-to-use technique that we want to deploy. So, what do we want to do? We want to build a tool that automatically help you, and the tool is intended for developers, although of course, it can be used by security research and other. But the idea is that as you write the code, we want to alert you about the the consequences of rounding errors. And we want to warn you what's going on. So, you as a developer, you will have the decision what is right and not is what is true.

And this is something that allow you to basically make your code more secure while you develop the code. Okay, of course, you could still integrate it, but it's not a bug-finding tool. You should think about it more as a tool for the developer, like a compiler or other methods that help you get your code right. So, the key idea is actually pretty old. Uh many of you probably I want to see how many of heard of the idea of abstract interpretation. Raise your hands.

So, it sounds like there are a few, but very few. So, this is actually a very, very simple, old idea that actually developed by Patrick Cousot. So, uh basically, I I don't have a pointer. But the idea is that instead of working, you think of of running your program, but instead of running your program on on the real number, you write them on some kind of a representation of these math numbers. Okay? So, here you see that we have a program that manipulate integers. And this program has loops, actually. And we don't know how many iterations are there. But even though we don't know how many iterations are there, we can still figure out some properties of these.

Okay? So, for example, in this example here, you see that the value of X and Y can range on arbitrary value. But in fact, you see that we can infer properties of them without running the program. In this case, we can infer that in at the point at the at the loop, we see that X is odd and Y is even. And why is this the case? Because we see that X is started odd and Y started even, and we see that when we add an even and odd, we get an we get an odd, and we get an even and even, we get an odd. We get an even. So, basically, this is very simple arithmetic.

And this is there, like I can't point out, but you see here, this is called lattice. So, the idea is there is this lattice, there is this question mark, which is means that I don't know nothing, and there is a value of even, and there is a value which is odd. Okay. So, Okay, so, the how is this related to rounding? So, apparently, it seems like actually rounding is very, very much related to this kind of things, because rounding errors actually also accumulate.

Okay? So, this is really a code that we took from a client, and we run this on very on very things on the client. And you see here, there is this function. And you see that in fact, how do I know which kind of rounding is here? You can think about it. You see, for example, there is this convert ratio, and it's called receive token price div what down. How do we know it's div div what up or down? Do we need to trust the user? So, we don't actually trust the user. We don't know. We don't This our tool doesn't understand natural language. It understand what's in line the code.

And so, basically, the fact that you are suggesting rounding up is not necessarily say that you are rounding up. Similarly, you don't know that you round down. And more interestingly, when we actually execute the operation, the the the the the imprecision can cascade. So, you can have imprecision with one level which will go to another level. So, in the solution, we build this tool, and we integrate it into Wala, the IBM tool, and actually now available. And the Wala actually allow you to do things. You can do many things besides rounding errors.

And we can basically find this rounding up and rounding down analysis. Okay. So, let's see this example. How do we know about the return value? How do we know the return value? How does the tool say? And as I said, the tool doesn't understand natural language. It only understand the code. So, we add this lattice. Okay? Our lattice is fairly complicated, but if you think about it, it's actually natural. So, the bottom value, the the value which is the most precise is exact. Which means that the real number and the integer integer number coincide. And then, there is the possibility of up, that the integer number is above the the the the the real

number, and there is a possibility of down, that the the the integer number is below. And if you join them, if if I have two possibilities, then it's either. So, I really don't know. And the worst that can happen, in fact, is intermediate. I'll show you later, when actually I don't know nothing about it. So, you can think about it as some kind of approximating the behavior of the program. That's what we are doing. We are approximating of the behavior of the program, and we cascade the value. So, you see, we start by the value being precise. This is where the function start. And you see that we accumulate it. We go precise, precise. I'll show you later.

And the idea is, you see now, we see it's round it it is round uh it's it start precise. You see, then it's round up, and later on, it can round down. So, we we figure out how the values propagate when the program executes. Okay. So, let's see this program here. There is this divide what up. What do we do? How do we know the value? So, what we really do, we actually perform what people call interprocedural analysis. The idea is that we analyze all the behavior of the program. So, in this case, we have the function the function divide up up, and it's calling actually the function my div up. So, we look at its behavior.

This function is actually implemented in assembly. So, what? So, we understand the value of the way assembly is executed. And we propagate the value of assembly, and we understand what are the mathematical rule for the assembly to behave as well. So, you see, the divide runs up, and adding runs Sorry, divides run down, and adding adds up. So, we accumulate all the values, and we compute them. So, this is done. So, now, what happened the the the the return value? So, you see, the return value, it takes the value which is computed by the previous function, and it's and it's it's it's it's

returns this value. So, what do we do here? Again, we look into the implementation of this function. In turn, this function is calling another function. So, you see, this function And this function is also implemented in assembly. So, we understand how the assembly is executed. We understand how the assembly is executed and we divide rounded by up you it yields down. So, this is how we do this abstract interpretation and we infer these properties of the program as we do this static analysis. So, this is of course something we do before the program is executed and warn you about the behavior.

Finally, what do we do about the return value? So, we propagate from the result to the return value and this case you see that we infer that this function return down and this is information that we can tell the user and the user see if this correspond with her intuition about what this program is supposed to do. And we we have actually implemented several patterns. So, for example, this is taking from the Morpho score but we have run it on many existing code. You see that here it's actually inferred the thing that if you take a function and you add a number and you divide it by a number which is smaller than this, then in fact the result is a rounding up. So, it's inferred in some kind of

good properties of arithmetic. What happened when you have when you have when you have a a if when you have conditional statement? Of course, any interesting program have conditional statement and conditional statement are fine. So, let's look what happened here. You have some kind of condition. Our analysis doesn't need to understand what this condition. So, it's conservative assumes that both of them are executed. So, you have the first case that the value is up, the other case the value is down. So, this is by itself not so bad. It's could be happen.

For example, you have a deposit where we draw have something economically which is different. But what happened in this program? On top of it, the program also does division after that. So, our analysis get very very confused and what we do in this case, we alert the user. We say we sorry, we don't know it's indeterminate and we don't know. We alert the user about this behavior. So, that's what we do and we we say round off this flag is what we call indeterminate. It means that we don't know what the analysis. It's not necessarily a bug, but it's something that we want to alert the user about.

Uh now we're getting to more complex program and we run it on quite complex program. This is a real example and you see actually how the analysis work on something pretty real and pretty sophisticated and you see actually it's makes something about quotient and it's actually give you something tricky about what happened with numeric and it's tell you that in fact there is some kind of tricky division. This has to be reviewed by the developer to see what's the intent. Uh here is another example. It's really a real bug actually that you see it's running by this analysis and in fact the tool can tell you the analysis because in this case it tells you that in fact it's indeterminate. So, it in fact it it gives you this and this is

something that could have be done to prevent this hack. Okay, and how will you do it? So, you see we start by interpreting that it's down. So, this is automatically inferred by the analysis. Later on, it find out that it's either okay, which is which is also inferred by the analysis. And finally, you see here it's find that it's either and here we see that the user will automatically see that there is a bug because you see the user call it down because the developer thought that it's rounding down. So, this is a mistake of a very experienced Solidity developer that this tool could have automatically prevented. And this tool this bug unfortunately was exploited.

So, this is what we want to do. We want to prevent this kind exploit before you run formal verification or fuzzing or any other method. So, this is what we do and we want to do this thing. Uh I'm wrapping. Uh this is a basic idea. We have implemented quickly because we we were really worried about all these uh bugs. Uh we did some shortcut like you every time when you do when you do something right and and basically we kept some patterns in particular we only handle unsigned.

We plan to add more but we this is what happened most of our clients. So, we think this is the most important thing. The analysis is sound. It means we can mathematically prove it's correct, but we have to be careful because we have done some shortcut that the analysis is definitely incomplete in the sense that there are a lot of program which are good and this analysis will fail to handle. And this is this is of course we have it's come to from a fundamental program problems in computer science. We cannot solve them, but I think we can make the analysis way more complete and we need your help to do it.

Uh you can extend the analysis to do many things. Uh there are of course a lot of related work in particular our tool which is very sophisticated there. So, to approve on the EVM bytecode and also I want to point the D dub tool. These are more advanced tool, but we wanted to do something much faster and this why we did this analysis. Uh the takeaway, this is a roundabout. It's a tool that you can use anytime and we have it and there is a QR code that I can show you. You we we plan to to integrate with as many other tools that we are building in terms of the Soter approver and uh and in in Q2.

It's a security tooling. You can use it with AI or with formal with any other tool and it's simple as extendable code. Uh I want to give you some questions. So, uh time for questions. So, basically this is the the QR of the tool. I I'm happy to take questions. There is time. I I I made it the talk uh quick enough. I see the question. Please take question. Please. Yes. Thank you for your presentation. Um I'm thinking would it be possible to compute bounds on the errors?

How easy would it be? Yes, so we have been working I've I've been working on it also academically with a with a colleague at Princeton and and Madison. We have methods for computer bounds. They're expensive. They're much more expensive than this. This is a very very simple analysis and it's even not done. So, so I the the good answers that we have analysis that we have done and it's actually very interesting, but it's expensive and I can tell you we the for example, this tool for good and for bad, it doesn't use the SMT. It's it's very very simple.

So, and if you want to do that, we can do that, but we we we it's it's much more complex. This is a the way I think about this tool is like you probably know I mean Soter is doing a lot of things including services and the service company we want to find bug and we don't want to miss bugs. That's uh and and this is something that is very very low hanging fruit for not missing bugs. But you are want something more advanced which we are working on sort of computing bounds and and and in fact the we we have been working on it both academically and practically and and we'd love to talk about it.

Thank you. Thank you so much. There's more more more question. Have you tried running this on the other hacks of the wrecked leader board? >> Um yes. Yeah, yeah, yeah. Yeah, it's we have we need more and we you love to this tool is a very should be available now. I don't think we run it to all of them. Hopefully people will not abuse it. We don't know, but but yeah, we it is detecting things and of course there are some cases that it detect errors even in program which are completely right, which is unavoidable and because it's the it's conservative. It's just basically compute something more of it. But yes, it is it is a tool that you can use and we

I I've one of the example you actually two of the example are from real life. Thank you. There's more question. Thanks so much for the for the presentation. Um sometimes the the developers they have this trick to round up a division of X by Y, they do X + Y - 1. That's what I showed. >> It's the example and in this case would you would the algorithm return up or would it return down?

>> It's exactly it knows the value. It knows So, in fact you can these are simple cases that we can analyze. Basically the analysis abstract interpretation even though it's so simple, it's surprisingly powerful. We have seen things like McCarthy function whatever that sometimes things are very hard for human and very easy for machines. This is something which is pretty easy for machine. The the machine only needs to understand that the the division by a number which is greater this number. So, it's actually very simple and that's the thing that actually I should say Patrick Cousot is from France. That's the thing that Cousot observed many many years ago before I even started my my academic career. Yeah, so the answers it's surprisingly uh how this simple method can actually infer these kind of properties like

division by X + 1. Uh but but some things are hard like of course exponential functions. There's some things which are which are much hard for for these kind of things to do. But but the the the normal thing that we see in DeFi should be handled and we we need to see that of course a practical issue question. But we see that in fact it handle division, handle addition, handle assembly code which is pretty common, handle conditional statement, loops. Thank you.

More question. >> Thanks a lot and I invite you to continue the discussion just after the the session. Thank you. >> [applause]