You Don't Trust AI. So Why Are You Shipping Its Code?

0:09Izar Tarandach If my thoughts about privacy are secret, do they still count as private?

0:14Chris Romeo And folks, welcome to the AI Security Table, and that's your thought of the day. So please ponder that throughout the day. If your thoughts about privacy are private. Are they still private privacy thoughts about privacy? Try to put that together all at once.

0:34Izar Tarandach If a private tree falls in the middle of the forest and there's nobody around to sell it to a data broker, does it count as confidential?

0:43Chris Romeo Yes and no.

0:46Matt Coles What happens if a hiker comes and finds it later?

0:50Izar Tarandach What's the sound of half privacy?

0:53Chris Romeo Half privacy.

0:55Matt Coles Half privacy. Is that a half open connection?

0:58Izar Tarandach I'm doing privacy cons here.

1:01Chris Romeo Privacy. You're trying to con people out of privacy?

1:03Izar Tarandach No, that's a data broker.

1:05Chris Romeo I couldn't resist. I'm sorry. It's early

1:07Izar Tarandach in the morning.

1:08Matt Coles That's a data broker. The analogies are, and the metaphors are—

1:11Chris Romeo We are all semi-caffeinated here at the AI security table.

1:16Matt Coles Wait, we are? Oh yeah. One of us is caffeinated, therefore semi.

1:19Chris Romeo Semi.

1:20Matt Coles One of us. One of us. One of us.

1:22Chris Romeo We'll let you you know, just try to decide which one is overcaffeinated, which two are undercaffeinated.

1:32Izar Tarandach There's no such thing as overcaffeinated.

1:35Chris Romeo That's true. All right, let's, so let's deal with this one that you did, this issue that you just threw freshly into, onto the table here about Sam Altman from OpenAI making some statements about We're not worthy.

1:52Izar Tarandach We're not worthy.

1:54Chris Romeo Nah, we are. Don't, don't even go there. Let's, let's not put these, these folks on a pedestal like everybody else in our industry does. They're not.

2:02Izar Tarandach What? But I thought that that was the rule.

2:05Chris Romeo No.

2:06Izar Tarandach No?

2:07Chris Romeo You know, on this podcast, we break all the rules. We're the bad boys of application security. I couldn't even say it. I couldn't even say it with a confident

2:20Izar Tarandach measure. Where's my buzzer? Okay. So what is it that the guy said? I no longer think we're going to be able to just patch all the bugs, he told the audience, in part due to the ongoing advancement of AI models and in part because the targets of cyberattacks have acted too slowly to get ahead of it.

2:40Chris Romeo Ouch. Gut punch.

2:41Izar Tarandach It's like you're standing in San Francisco in the middle of the street and you're seeing the tram coming down. And you can clearly see on top of the tram written security debt. And all of a sudden the thing just goes and hits you. All of a sudden, like nobody saw it coming.

3:00Matt Coles I actually agree with his statement a little bit.

3:03Chris Romeo What? Come on. All right. Explain.

3:07Matt Coles How many issues do you think you have in any given piece of software?

3:11Chris Romeo How large of a piece of software are we talking about? 10 lines or 10 million?

3:17Matt Coles No, let's say a common desktop application. So probably 100,000 lines of code.

3:23Izar Tarandach Sure.

3:23Chris Romeo How many security? So how many flaws?

3:27Matt Coles How many flaws? Now here's the interesting question. Not necessarily a vulnerability, but a thing that can be exploited later.

3:34Chris Romeo Okay. I just got into a big argument on LinkedIn about this one, so I can't wait.

3:39Izar Tarandach Where later is a movie target.

3:41Matt Coles Right. And, and this is, this is part of the problem, right? Is you're always gonna be chasing your tails. We're always chasing our tails anyway in software security, right? Cuz we developers introduce bugs and then they get, there's a risk process where those bugs get shipped.

3:57Chris Romeo Yes. Right.

3:58Matt Coles We don't ship, we don't fix all of them.

3:59Chris Romeo You're describing the, the, the distant past, not the current future that we exist in here where I can, I can spin up 200 subagents and say, Tear this repo up, try find as many flaws as you possibly can and fix them.

4:18Izar Tarandach And how many do you still have left?

4:21Chris Romeo It'll be less than what I started with. I hope.

4:24Matt Coles Are you sure?

4:25Izar Tarandach Are you sure?

4:26Chris Romeo Well, it, it, it come, but it come. If, if you do this from a single model, single agent perspective. Then yes, you will likely not get any type of positive result. If you use a multi-model, multi-provider approach to looking at your 100,000 lines of code, you can reduce, maybe not to zero, right? But you can reduce, but we'll get into formal methods and formal verification later.

4:58Matt Coles Yeah, we got to talk about that next.

4:59Chris Romeo 'Cause that could get us to zero, maybe. But yeah, my point is like, you can eliminate some percentage, I think some large percentage of them by having the right strategy of models and reasoning and capability of the models.

5:16Matt Coles Sure. And how many, how many software vendors are going to do that on day one, release one of their thing?

5:24Chris Romeo Well, a bunch of people that used PHP in the last week or two have been scrambling to try to update that sucker.

5:32Izar Tarandach Yeah, that's the point. Very quickly. You do all that nice exercise with your codebase, and then Carl goes and changes a little library written somewhere else by somebody completely different, and pop goes the weasel.

5:47Matt Coles Right. So, we're in the same boat, right? That we've been in for decades is software gets shipped. And I won't— well, let's not restrict us to software, by the way. It's systems get shipped, right? They get built, release one, they have a bunch of They have stuff in them. They're not perfect and we're okay with that, right? We know bugs exist, bugs happen.

6:04Chris Romeo We're not okay with it, but we just have to accept it.

6:06Matt Coles We have to accept it. Right. And whether it's human-generated code or if it's AI-generated code, and certainly you can do things with, with, you know, verifications and QA and whatnot to try and reduce the level of defects, but we almost certainly are going to ship with defects and we're certainly going to ship with things that will later become defects. As we all know, right? Zero days exist.

6:29Chris Romeo So for now, I would agree with your statement today. I don't know. I don't agree with your statement one year and five years in the future.

6:37Matt Coles But if we start right, but if we start fresh, then what you're saying makes sense. And that's, I think, where Sam Altman is going with this, right? Is now that we have the power to build it correctly, shouldn't we go back to release one?

6:52Izar Tarandach But do we?

6:55Chris Romeo So you think he's taking the disposable software argument?

6:59Matt Coles I think he is.

6:59Izar Tarandach No, he, he's saying, he's saying this.

7:00Chris Romeo I didn't get that from it, which I've heard people describe the disposable software argument for the future, which is we'll reach a point where it won't even make sense to patch something. You just have the agent rewrite it from scratch. That's right.

7:15Matt Coles I, I don't think that's, I don't think that's in the far, far distant future.

7:19Izar Tarandach Look, he's just being the hero that we didn't know we needed, right?

7:24Chris Romeo You cannot attribute him to Batman. No, he is not Batman. No, I refuse. I refuse to accept that.

7:31Izar Tarandach Wait,

7:32Chris Romeo where's my button to bleep? Do I have a bleep button so I can just bleep these out from now on?

7:36Izar Tarandach His next quote.

7:37Matt Coles Don't we have time delay?

7:39Chris Romeo We are time delayed because we're on broadcast television.

7:43Izar Tarandach This cybersecurity dot dot dot. I don't even know a dramatic enough word to use, but the problem coming towards us, I think, is still something that we have not, as organizational leaders or countries or individuals, taken seriously.

7:58Chris Romeo I agree with the dog.

7:59Izar Tarandach And the dog appears to agree with him, which is basically what we've been saying for the past, I don't know how many, 30 years.

8:05Chris Romeo Well, yes. I mean, it's tough to, it's tough to argue with that statement that leadership across small and large companies haven't taken cybersecurity seriously.

8:15Izar Tarandach Agreed. But then, then he throws in the, the, the, the Facebook lingo, whatever. People definitely patched some bugs, but it was another one of those cases where people didn't really intuit the exponential.

8:29Chris Romeo What? What does that mean? Did a model write this? No. Is that actually him?

8:33Izar Tarandach They, they, they, they didn't see the curve going up fast enough, you know? Even though we were standing at the bottom of the curve saying, look at that mother going up.

8:43Chris Romeo Yeah.

8:43Izar Tarandach Apparently nobody else.

8:45Chris Romeo It was, it's all, it's all perception. Because we were seeing it, we were watching it.

8:50Izar Tarandach We were surfing that shit, that thing.

8:54Matt Coles There goes our PG rating again.

8:55Izar Tarandach Indeed.

8:56Chris Romeo So much about E for Everyone. I thought that was always my, our goal. Yeah. So I, I, I think it is, I think this is, this is something we have to focus on right now. The ability to use AI to remove as many latent flaws as we possibly can from a codebase.

9:16Izar Tarandach Yeah, but look, the conversation will always be, until we get to the formal methods, did you do a good enough job, right? When you have on one side a tool that apparently is able to intuit the exponential and figure out every single hairy issue that we can, could never with our measly scanners. Right? Or even reading the code. Sure, it's going to figure out a bunch of low-hanging fruit, medium-hanging fruit, even some high-hanging fruit.

9:52Chris Romeo Some critical.

9:53Izar Tarandach But then what you're left with is the hidden critical, which could, maybe not, have the biggest impact.

10:04Chris Romeo Well, you just have to find ways. For the model to find these hidden criticals.

10:12Matt Coles Part of the problem is costs. And I don't mean, well, it translates to dollar cost, right? But in order to find more higher complexity of problems, right? So the low-hanging fruit of the flaw in the code that's obvious, right? Like it's a CWE written right there, right? I don't check memory, or I have some other flaw that's obviously a single weakness, right? That's a grep. I mean, it's not a grep, but it's a grep, right? It's, you're looking for a construct in code. As you get more and more complex, and as you start to chain these things together, the token cost goes up, right?

10:52Chris Romeo Well, who cares about the cost?

10:54Izar Tarandach We're

10:54Chris Romeo fighting for security. We're fighting for security.

10:57Matt Coles Somebody cares about the cost and we're back to the iron triangle problem.

11:00Chris Romeo It depends on. It depends on the organization. So I'm aware, I was talking to somebody who's at a, I would say a very high-end, and not even a startup anymore. It's a company that's now established, but a tech player, not in the AI space. And they were given a blank check by their CEO. The security team was given a blank check for token spend. CEO said, I don't care, just reduce my overall risk profile.

11:29Matt Coles Right. Of the, of the million or so software vendors in the world today. Yeah. How many of them are gonna do that?

11:36Izar Tarandach Less than a hand. But here's the problem. We, we are—

11:39Chris Romeo doesn't wanna succeed.

11:40Izar Tarandach Wait, we, we are falling into the same pattern.

11:42Matt Coles Maybe it's pay to play. Is that what you're saying? It always has been, by the way. I mean, you've hired the, the good engineers or the biggest tools.

11:49Chris Romeo Yeah. Look at the Frontier Labs now.

11:51Izar Tarandach Guys, wait, wait, wait, wait.

11:51Chris Romeo You get hired there, you're like, oh, look, I'm making $5 million a year. Sweet.

11:55Izar Tarandach Wait, you, you, you fall into the same patterns that we've, that we've fallen in the past, right?

12:01Chris Romeo Guilty.

12:01Izar Tarandach We are going, we are now saying tokens, tokens is everything. Once upon a time we said regular expressions was everything. Once upon a time we said AST trees was everything.

12:10Chris Romeo Anyone who's ever created a regular expression that's more than 5 lines did not say this was everything. They said this is terrible.

12:16Izar Tarandach But everybody was like, oh, we're going to write the scanner and figure out all the bugs. Just go back 10 years and look at the marketing that we got from, from companies.

12:24Matt Coles Oh, sure.

12:25Izar Tarandach And now we are saying tools are everything. But they're not. Sorry, not tools. They are everything. But they're not. They're limited. We know they're limited. Sometimes it can even be proven that they're limited for some cases, right? So let's not step into the same mine that we keep telling people that they step on. Let's not just call the next Messiah and say this one is going to take us out of of the sense. And then they're good.

12:54Chris Romeo So what else can we do then? What should we do? Just, just wait.

12:59Izar Tarandach Let's bring everything together. No, let's bring the tools together. Let's get a bit of this one, a bit of that one, a bit of that one, the best of all of them. Make them work together and then see what we get out of it.

13:09Chris Romeo If you don't go all in, let me, let me throw the other side of the table here. If you don't go all in on models, LLMs, AI, assisting your security program. We're, we're watching the other side go all in with AI, meaning the attacker collectives of the world.

13:32Izar Tarandach Yeah, but some of the—

13:33Matt Coles So the defenders have, defenders now have an advantage in this area because the tools that were deterministic in the past were always generating a lot of good information. I'm sorry, they're always generating a lot of information. The problem was good information. And what the AI is, I think, really going to help us with, or should help us with, is in the past you used to have humans, you'd have a team of engineers go look at 100,000 findings from your static code analyzer and go, "Ah, that's a lot of stuff. Ship it," right? Because it was noise, but it wasn't really noise. It was actually a lot of good data points.

14:13Chris Romeo Well, it was a lot of false positives too, though.

14:15Matt Coles Yeah, but it was a lot of false positives under certain condi— under a certain condition, which the engineer was biased towards. Now, I think what we might see is that these findings are valid, or they're valid under certain conditions that the models can now extend to multiple path to tech discovery.

14:34Chris Romeo The model's working with the output of a deterministic scanner. Should be able to get you better detection of false positives, reachability, all these types of things.

14:47Matt Coles So I'm going to liken this to when we went from, you know, point-and-shoot security testing to, to aggressive fuzzing.

14:58Izar Tarandach He's reviving DAST. He's reviving DAST. I can see it.

15:01Chris Romeo I'm not reviving DAST. He loves DAST.

15:04Izar Tarandach I am not.

15:04Chris Romeo This is time he's been wearing a t-shirt under his jacket that says DAST is the science.

15:09Izar Tarandach He's doing CPR on DAST.

15:12Chris Romeo And it's, he, he was afraid to speak because we were so mean to the DAST community.

15:17Izar Tarandach Actually, Matt, I think that what you're describing is a journey into what's called the knowledge pyramid or information hierarchy, right?

15:26Chris Romeo What is this, a CISSP review class?

15:29Izar Tarandach No, no, no, no. It starts with Data in the bottom, it goes up one level to information, another level to knowledge, another level to wisdom. So we had a lot of data in the form of code. This is our data. This is what we swim in. We applied the scanners. We got a lot of information. Then we had to figure out of all this information, what the heck is good? What is bad?

15:54Matt Coles Right.

15:54Izar Tarandach That was transforming that information into knowledge. Now we know what's bad. We know what needs to be fixed. Then from knowledge, we would go to, okay, what are the mistakes that I can't repeat again? And here's my guidance and here's my templates and all that good stuff. And that became wisdom. And that journey took a lot of time because you had a lot of data, you still had a lot of information. It was hard to come up with the knowledge and only sometimes you could get to wisdom and then you had to go back to the people who created the data and apply all that., right? And that loop was hard as

16:29Matt Coles hell,

16:29Izar Tarandach right? Especially the one going from knowledge to wisdom,

16:32Matt Coles right? Because you had a lot of, again, you had, you had people, which isn't necessarily a problem, but there's bias, there's schedules, there's cost, there's, there's people.

16:43Chris Romeo I'm just, I'm just pissed. I'm realizing I'm just pissing everybody off today. Sure. I'm just, I'm in one of those—

16:48Matt Coles You're not pissing us off. You're just, you're just arguing about, uh, invalidity.

16:51Chris Romeo I mean, every— I'm trying to, I'm like, I'm like equal opportunity offender this morning of like,

16:57Matt Coles Democracy. So, but AI models are, well, since we've talked, we can talk about superintelligence if we want.

17:04Chris Romeo We talked about that last week. That was last week. We already, we already, we already handled superintelligence.

17:10Izar Tarandach Kill me, kill me in the morning. Kill me in the morning. Yeah. Yeah. Why not? It's not like I have a full day of work in front of me. Yeah. I mean, yeah.

17:18Chris Romeo Might as well go out early in the morning before you put a whole day's work in.

17:23Izar Tarandach This is a FedRAMP compliant podcast. We don't talk about the US, we talk about superintelligence.

17:29Chris Romeo We're not going to get our federal grant money, which is why we were doing this podcast the whole time for that $995 grant money per year.

17:40Izar Tarandach Superintelligence, la la la la. Yeah.

17:44Chris Romeo No. That was actually a nice move. That was like your superhero pose. I prefer the One where you hit the ground like Captain America. Oh, here comes Hulk. I could see Izar as— Izar would be a funny Hulk. Cause he doesn't really— I don't— you're not a super angry guy.

18:04Izar Tarandach Hulk sort of bashes. Hulk not invested enough to bash.

18:11Chris Romeo That's your— that's definitely your superhero. All right. So let's talk about formal verification. Let's see how that plays in. Let's see if we could, let's see if we can tie that into this conversation. Wait, wait. And boy, what are you getting academic here? What are we doing?

18:28Izar Tarandach I'm getting formal.

18:29Chris Romeo Okay. I thought you might've had a tweed jacket with those little like elbow things, whatever. Actually,

18:35Izar Tarandach you

18:35Matt Coles know,

18:35Chris Romeo if, if,

18:36Matt Coles if you have a, if you have a pipe and, and a foot of rope.

18:39Chris Romeo No, we don't allow pipes to be part of this podcast because you meant like a pro— oh.

18:45Izar Tarandach Not

18:45Matt Coles that

18:45Izar Tarandach pipe.

18:46Chris Romeo Oh, I thought you were talking— I gotcha. Okay.

18:49Izar Tarandach I thought if I put on a tuxedo, people are going to, to think that I'm going 007, not the formal.

18:55Chris Romeo 007. I like how you use that.

18:57Izar Tarandach Yeah.

18:58Chris Romeo It's not double O seven, it's zero zero seven. Secret agent, man.

19:02Izar Tarandach Right. You people call it double seven. Yeah. Sorry.

19:05Chris Romeo Well, Ian Fleming, the guy who

19:07Izar Tarandach wrote the

19:08Chris Romeo book,

19:08Izar Tarandach because it's too boring to say twice the same word, zero zero. It has to be something like Double zero. Yeah, sure.

19:15Chris Romeo Well, he is a super agent. Come on.

19:17Izar Tarandach Americans. Oh wait, I'm American too.

19:19Chris Romeo Yeah.

19:20Izar Tarandach All right.

19:21Chris Romeo So formal verification. So I remember this and we talked about this about 2 years ago on the previous podcast called the Security Table. The formal verification came up and, but now we've got superintelligence and what if we take superintelligence and we point it at a codebase and say, formally verify this thing, is that even, is it more possible? Start there. Is it more possible today than it was 2 years ago?

19:53Izar Tarandach Well, it's good to say formally no, but the thing that I think is gonna come, and this comes from some other stuff that I've been doing with AI, it's going to create something so very convoluted, so very jargon-loaded, so very pseudo-mathematical that most people won't be able to actually look at it and formally say, oh yeah, this is right.

20:20Chris Romeo So its own programming language, is that what you're— or just its own communication?

20:24Izar Tarandach No, no, it's going to come up with like a bunch of gobbledygook saying according to this and that, and if you call this an invariant and this idempotent and that's the other thing, it's, it's, it's, it's it's hard.

20:39Chris Romeo But isn't formal verification have to have some component of simplicity? Isn't that what makes something formally verifiable? At

20:49Matt Coles least in the historical sense, you need to make— the proofs get so complex that you have to start with a small thing first. What do you want to verify? Right? So you want to verify correctness, completeness. You want to verify some property. And so if you don't bound that, that proof is going to get very large. The number of variants, right? The number of variables, the things that can change will basically make the complexity of this formula, of this algorithm explode, right? So can you prove, you can prove certain things. Pretty well if you bound it pretty well, and then it becomes a lot easier to verify.

21:41Chris Romeo Right. Okay. Now we live in a world where we have LLMs that can do hard things on our behalf. So Ezar's, Ezar's objection is that they're gonna make it, they're gonna, they're gonna document it in such a way that we can't even prove or understand that it's

22:02Izar Tarandach correct. What Matt so aptly put that I failed to is that the proof can end up being more complex than the thing that's being proven. And I do not think, my personal, do not think that I trust the output of an LLM enough to look at it and say, well, this looks like it makes sense. Must be right.

22:25Chris Romeo What would you need to see to build that trust?

22:29Izar Tarandach I would not have anything today that would build that trust to 100%. I think that Matt, of course, is right when he says you have to start small and you have to start with little things. But then my, my, my next question is, how practical is this for the everyday system that is built? To apply. So are we talking, are we proving algorithms? Are we proving implementations? Are we proving coverage? Are we proving what?

23:01Chris Romeo Or is it just critical pieces? Well, actually, because there's, we could make a short list of critical pieces of the system, payment processing, authentication, authorization policy.

23:13Matt Coles That's too big, right? You wanna prove, you need to prove correctness. So first off, you're proving correctness, right? Correctness implies there are no flaws. So does it do what you need it to do correctly and not do anything else, right? Security issues are side effects.

23:35Izar Tarandach Yes, but I'm going to throw it out there that the security value that you could get from a formal proof, at least to the extent that I understand it, that could be completely wrong. Is going to be so, not small, but focused on the piece of code that you're trying to prove something about, and leave so much of the scaffolding around that code, that at the end of the day, from a security point of view, it's going to be immaterial. So you can prove that the crypto bits of OpenSSL are perfectly done. But that proof is not going to say anything about the verification of authentication up to the end. The use of nobody, nobody used 4 for a prime for the certificate or something

24:35Chris Romeo like

24:35Matt Coles that. That's a simple proof though. It

24:37Chris Romeo sounds like that happened. It sounds like you're describing something that really happened.

24:41Izar Tarandach But my point is that the, you know, I'm just having a horrible déjà vu here of going back to calculus classes and I had very special calculus experiences and see a proof of a theorem on the board and being unable to, from that proof, think, okay, where does that fit in the world? So that's proven, now what? And it's difficult for me to understand or to, or to imagine what would be the formal proof of no security issues. I can understand the formal proof of this algorithm is valid for something. This algorithm does what it's supposed to do and nothing else. But it's hard for me to imagine how the, the security of something can be formally proven. When the number of variables and the number of external dependencies, and I'm not talking about libraries and that bunch of stuff, talking about logical dependencies, could be so much bigger than the code that's actually in the binary.

25:50Matt Coles Agreed. And that's, and that goes back to formal verification. Proof is for correctness of function. And we should really be, we should be careful making that a statement that if we prove a function is correct, that the system is secure. The formal proof, the formal verification enables us to know if a piece, if a particular piece of code that does a certain thing is free of flaws, which contributes or should contribute to the overall security of the, of the thing in which it lives. So I don't know if you could take a full software application and formally verify it in a reasonable cost or time. Even with LLMs, but you could verify its pieces of its functionality, file reading, file handling, user input, maybe authentication might be not, might be small enough. Right. So certain methods you could probably verify that are, that are flaw-free. Now the integration, we've talked about this before, I think about its building blocks, right? So if I, if I verify Feature A and Feature B, when I now add A and B to a broader system, not all of those verifications are gonna, not all those, those, not all of those results are going to be valid because now I've integrated them together and changed the posture.

27:16Izar Tarandach So in other words, if they create new

27:19Matt Coles paths that have to be verified,

27:21Izar Tarandach if we were able to take all the security notable pieces of a system, Put all of them in a single library and then use some mechanism to prove that that library by itself is correct. And from there, assume that it's secure. I would say that that's a lot of tokens wasted because the moment that you start calling those functions from different parts of the system, that you probably cannot approve the same proof. The way that you apply those proven trustable pieces may be untrusted and probably will be untrusted.

27:57Matt Coles Yeah. So the, the article that we were referring to here actually talks about this, right? So it talks about verifying Cellphore, right? So Cellphore is a microkernel. Let me go find it here. I lost it. Where, so it's a security microkernel, right? And why can I not find it? Just looking at it, hit it when I lose track of things. So they did some formal verification of Solve-4 and— what? Sorry. I was going to quote something, but I can't find it anymore. Probably because I resized my page. Sorry. Talking out loud here. Talking to myself.

28:38Chris Romeo We can—

28:39Izar Tarandach oh, there's more than memory safety.

28:41Matt Coles Yeah, I know there's some tool I could use. Yeah. Search, Ctrl+F worked fine. So they used, they tried to verify Cellphore, right? So it's like microkernel. It took 20 person years to formally verify it. Now, does that mean that—

29:03Izar Tarandach But wait, where is it that they verified? What does verification mean in this case?

29:10Matt Coles What they, what they verified, they actually published their formal verification paper. They did machine-checked formal verification of Cell4, which is a microkernel. They verified its C implementation, IPC communications, and the kernel.

29:33Izar Tarandach Okay. That's what they verified.

29:34Chris Romeo Simplest case.

29:35Izar Tarandach But what was verified?

29:36Chris Romeo But they use, so what they, they verified using fuzz tests.

29:41Matt Coles They verified all possible code paths. They verified all possible code paths.

29:44Chris Romeo Using fuzz tests as the input. They took the existing fuzz tests and turned those into proofs. So it's a very, it's a, it's, it's not a full, I wouldn't say this is full formal verification of that software. It was more focused on file processing.

30:00Matt Coles It wasn't a mathematical verification, I guess. It was a real-world test verification. Right. So verification can mean different things, right? So they used, they use code path analysis. It's, I'm just summarizing and hopefully I get it right. That they use code path analysis to verify that all of the functions did what they were expected to do and nothing else.

30:25Chris Romeo And found a whole boatload of bugs along the way.

30:28Matt Coles Found a whole boatload of bugs. And this is, Sulfur is used, it seems in Well, various places, like, uh, is it in the Airbus? I think they're implying. So it's used in very specific ways that where you need high assurance.

30:47Izar Tarandach Yeah. The, the, there is a line here on the conclusion that's bugging me somehow. The trajectory is clear. Formal verification, blah, blah, blah, blah, blah, blah, will soon be as practical as fuzzing. Is today for almost all production software. When did fuzzing become practical that I missed the memo?

31:09Chris Romeo Well, you don't fuzz all your stuff? I don't either.

31:14Izar Tarandach I barely fuzz my hair in the morning.

31:18Matt Coles So, yeah, I mean, fuzzing is practical, but it's not necessarily economical.

31:25Izar Tarandach So fuzzing as an activity is practical., but we fall always back in the same black hole. You fuzzed. It depends on, it

31:34Chris Romeo depends

31:34Izar Tarandach on where you're building. What if the next byte? No, no. What if the next byte is the one that, that, that would trigger the, the condition?

31:40Chris Romeo Well, that's why you generate tens of thousands of mutations.

31:43Izar Tarandach And what if the next one was the one?

31:46Matt Coles Do you stop?

31:47Chris Romeo Formal verification is you create all of the possible mutations that could occur,

31:52Izar Tarandach which is why

31:52Matt Coles you have to bound the problem,

31:53Chris Romeo which is why you have to bound the problem.

31:54Matt Coles Cause otherwise

31:55Chris Romeo it's, I'm, I'm way out of my league. You have to.

31:58Izar Tarandach Now, the article also offered limitations, which is great, right? They're saying, hey, there's some stuff in here that in practice, formal verification can sometimes prove less about the security of the code than we would like. To me, the words, the key words here, in practice. Formal verification is something that is wonderful, that is great. And we knew that before LLMs. In the blackboard. As soon as you jump from the blackboard to the real world, all kinds of strange limitations start creeping up. And the fact that now we have some logical engine that does the formalization much faster doesn't seem to be adding much to the, uh, you could call this a forward-looking article, but at the end of the day, we are in the same place that we were before. We can generate a lot of stuff, but then we look at it and you say, now what?

32:54Matt Coles Now it is interesting. We are talking about LLMs, which are non-deterministic. And so what they're writing is a set of, basically a set of requirements, right? They're, they're setting a bunch of, uh, defining a bunch of rules that need to be checked.

33:14Izar Tarandach Those would be goals, right?

33:16Matt Coles Those would be goals. The AI writes the proof based on the data that it gets. It says, this is my code, this is my results.

33:25Chris Romeo But it's not doing it in a determined or a, it's not, the model's not doing it from what I'm reading here. They, they turned it over to this RockCube software, which then ran every po— and they did run every possible input. I was only joking before when I said that, that you have to run every possible. That's how they got to run every, that's how they're calling it. They're, but they're calling this formal verification because they're saying we ran every possible thing that could happen for input. And then this is the pile of bugs.

34:00Izar Tarandach Let me guess, this, this RockQ or something, that's basically a formal logic engine. That gets rules, transformation rules saying if this, then that, and that is true. So we are losing the non-determinism in the use of a formal language.

34:19Matt Coles Right. So interestingly, let's, let's, let's, let's take a look at the specifics on this one. Over the span of a few weeks, Claude successfully patched bugs it found and then proved that there are no crashes on any input up to 64 megs in size for 239 entry points across 123 different OS fuzz libraries. The typical proof was 600,000 lines of code providing security guarantees on binaries with a length, median length of 18,000 RISC-V instructions.

34:56Izar Tarandach So it's doing what, just memory checking?

34:59Matt Coles It was memory checking of small functions, right? I mean, 18,000 RISC-V instructions sounds pretty small, right? So they took a defined thing, they took a very constrained thing and proved that all possible inputs are correct.

35:23Izar Tarandach Up to the length of 64 megabytes. So, A, we don't know anything about 64. Plus 1,

35:30Matt Coles right?

35:30Izar Tarandach 6 megabytes plus 1 byte.

35:32Chris Romeo Mm-hmm.

35:34Izar Tarandach And so

35:34Matt Coles they claim it actually, we don't know if 0 is part, we don't know if 0 is included in that, by the way. We, we only know it's, we don't, don't know the full limits of

35:43Izar Tarandach it. But then comes the question. Now what?

35:47Chris Romeo Now they have a whole bunch of bug fixes for the problems that were found.

35:51Izar Tarandach For those small functions, for, for those small text functions.

35:54Matt Coles Right. So now you know that those functions have no flaws.

35:57Izar Tarandach And when 9 AM clicks and I turn this, I turn to my work desk, uh, laptop, how's my life better?

36:11Matt Coles Well, if you're using RISC-V, you're marginally better because the functions you're using are now proven to be correct.

36:18Izar Tarandach But yeah, so those three guys would be very, very happy.

36:23Chris Romeo But they, this is only in regards to like file processing, which is, I guess, what the libraries are doing.

36:32Matt Coles Yeah.

36:32Izar Tarandach Yeah. Well, but, but, but on the point of view of the memory corruption issues, doesn't say anything about that.

36:39Chris Romeo Which are common things that happen in file processing libraries, right? It's easy to have memory corruption when you do that.

36:47Izar Tarandach Yes, but. Yes, but. Type-safe and memory-safe languages and compilers have been a thing for a while. Not that they don't have bugs themselves, but there are other ways of dealing with this stuff that do not depend on formal logics of blocks of up to 64 megabytes.

37:09Chris Romeo So I'm getting that these are just a formal verification hater.

37:13Izar Tarandach No, I'm not. No, I'm not. I'm thinking that. That's a great way to go, but formal verification of the things that we have today, perhaps before they are heralded as yet another great revolution, they should be practical. And this does not seem to be practical to me. On the other hand, working off of formally provable programming languages might bring better results over the horizon than this.

37:43Matt Coles So honestly, I'm the issue I think I have with all of this, the automation to prove correctness is awesome.

37:51Izar Tarandach Yeah.

37:52Matt Coles But, but where I have a, where I have a, I'm curious about is using an LLM to fix the bugs that are found.

37:59Izar Tarandach Are you introducing more?

38:01Matt Coles Well, that's, that's one. How do you verify that the bugs are actually getting fixed and not introducing new side effects?

38:07Chris Romeo In this case. The model, they're, they're, they're creating these RockQ proof language files,

38:19Matt Coles right?

38:19Chris Romeo Which are then the source of truth. So it's a deterministic,

38:23Matt Coles it, it's test-driven development.

38:25Izar Tarandach Yeah.

38:26Matt Coles But, but it's, how do we know that what Claude is writing is free of defects?

38:34Chris Romeo What it, what is, because when Claude writes something, writing what?

38:36Izar Tarandach All the tests are green. It might be 100%, but it's library

38:40Chris Romeo code. The theorem, the proof language code,

38:44Matt Coles all

38:44Chris Romeo of it,

38:45Matt Coles right? They're writing the code, they're writing the patch, and they're writing the verification of that patch.

38:51Izar Tarandach We talked about earlier.

38:52Chris Romeo Yeah, it is, it is test-driven. It's tests are what are driving your ability to explain.

38:57Matt Coles Should the plot be writing its own proof?

38:59Chris Romeo No, probably not. Back to the first, the thing I said earlier.

39:03Matt Coles Right.

39:04Chris Romeo You need to, we need to live in a multi-frontier model world where if you have one do something, you should have the other one either check it or do the other thing. Like don't have Claude write tests for code that it wrote. Have Codex write tests for the code that Claude wrote and, and code review, have one review the other. And I've found some really interesting things when you have one frontier model review another frontier model's code.

39:39Izar Tarandach So you're telling me that compounded mistrust equals trust?

39:44Chris Romeo Compounded mistrust equals trust.

39:46Matt Coles 3 lefts always make a right, right?

39:48Chris Romeo It's the best that we can do right now.

39:52Izar Tarandach Do you think that video from last week of the two AI is interviewing each other and they couldn't get out of it because they kept saying bye-bye, bye-bye, bye-bye, bye-bye. Do you think that they were using the same model or two different models?

40:07Chris Romeo Probably using the same model. That's why they got caught.

40:10Izar Tarandach I say it doesn't matter. At the end of the day, they got into a loop.

40:14Chris Romeo Loops are certainly possible.

40:17Izar Tarandach So that, that, that's the thing. If we don't trust A, we don't trust B, we don't trust C. Putting A, B, and C in a pipeline and having them mix and match results does not give me more trust.

40:30Chris Romeo The alternative is to just live under a rock and not use advanced technology.

40:36Izar Tarandach Depending where the rock is.

40:39Chris Romeo This is, this, but this is the, I mean, the, the bigger issue that you're describing. I've heard other, I've heard this play out in multiple different ways. But it's the, the, the, it's the anti-AI crowd. So I'm not saying you're, I'm not saying you're a part of that, but that's, but that argument is going in that direction. Like there are some people that are, that are arguing against the use of AI still to this day.

41:05Matt Coles And

41:06Chris Romeo it's like, we just did a, we did an AppSec podcast with Brooke and Brooke brilliantly just described this, like either get on the boat with us or the ship has already sailed. Like if you're not, if you're saying, well, this isn't gonna change the world, this isn't gonna change how we build stuff.

41:25Izar Tarandach Chris, Chris, look, look, I use AI every day, day in, day out. Okay. I'm even over the bump of feeling guilty about using AI to code, but there's a difference between being the guy in the front of the Titanic saying I'm the king of the world, And being the violinist playing until the water gets to your waist, right?

41:50Chris Romeo Mm-hmm.

41:51Izar Tarandach What I'm saying is, sure, let's use it, but let's not think that it's the solution for everything under the sun because it's not. Now let's use it with enough mistrust.

42:01Chris Romeo But you trust it enough to use it every day.

42:04Izar Tarandach No, I'm, I'm saying let's use it with enough mistrust so that it forces us to keep some modicum of cognitive capability to make sure that what we're getting is actually what we want to get out of it.

42:18Chris Romeo Let me ask, let me just make this really spicy. How many lines of code did AI generate for you last week, roughly?

42:28Izar Tarandach I wish I knew because I didn't go and read all the code.

42:33Chris Romeo How many, how many, good, this is, I feel like a lawyer on one of those shows because you're walking right into my, you're walking right into my trap here. I am, I am, I see where I'm, I see where I'm going. How many How many lines of code then did you review yourself to enhance the trust that you had in the output that was coming from the coding agent?

42:51Izar Tarandach Less than 100 of what got produced, probably, because I don't know how much got produced.

42:57Chris Romeo Matt, your honor, I rest my case. Hit the gavel.

43:00Izar Tarandach So, so— No, I'm going to— no, no, no. Now I'm going to get to take you on another tangent. Not one single line of the code that I had produced. Was critical in any way, shape, or form. This was all stuff that I was willing to throw away.

43:15Chris Romeo So it was all prototyping.

43:17Izar Tarandach Because what it did was shape up something that I had in my head to give me the possibility of seeing that I was going somewhere valid with that. Now, the moment that that thing becomes a product, the moment that that thing goes somewhere critical, the moment that people depend on that thing, the way that I relate to that code will be very different. Because that's what I've been asking from my developers for the past 30 years.

43:40Matt Coles That's the, that's the point. Trust. Trust. How do

43:46Izar Tarandach you, that's the point.

43:47Matt Coles Where do you, where do you, how, how do you get, how do you establish trust in the code that gets written? And you would do it whether it's a developer or AI. AI is just a developer.

44:00Chris Romeo Formal verification, Matt. Of course.

44:02Matt Coles Of course.

44:03Chris Romeo Full circle.

44:04Matt Coles There we go.

44:05Chris Romeo We came all the way back around.

44:07Izar Tarandach But actually, before we go to the formal verification, I would stop on what we already have. We use the deterministic tools that we already have.

44:14Matt Coles Right.

44:15Izar Tarandach We, of course, definitely, completely, always use threat modeling.

44:20Matt Coles Right.

44:21Izar Tarandach Because that's the point where you look at that mass of code that got created and you decide there's enough critical stuff in here to rewrite or to completely go and read.

44:30Matt Coles Right. And by the way—

44:32Izar Tarandach These are the big flaws that might happen in the way, and this is how I'm going to stop them from happening.

44:37Matt Coles And let's bring back another topic that we just talked about. You have this data to information to knowledge to wisdom stack, right? Use the tools to find data, then turn it into information and knowledge and wisdom. And you pass all that information back, whether you're training your developers You have security champions, you're training them on security techniques or on good code constructs or guardrails and paved roads, right? The, whether you're doing that to a human developer or a team of agents and subagents, it's that feedback loop. Nothing changes, nothing changes, right? It's just another set of hands.

45:22Izar Tarandach Uh, one thing changes and it's, yeah, I think it's very important. Sorry, what's the term of the Zeitgeist? It's load-bearing.

45:29Matt Coles Oh God, don't do that.

45:31Chris Romeo It's load-bearing.

45:33Matt Coles It's load-bearing. I don't know who, where that was introduced. Somebody trained their models on bridge construction or something. And that's where that's—

45:40Izar Tarandach So when we're training people, you are able to an extent to say, please don't do this and walk away with the hope and some trust that they won't do that. Apply the same thing to an LLM and it's a suggestion that may or may not be taken into consideration.

46:02Matt Coles It's a suggestion unless you do other things, but it's the same thing with a, with a human, right? A human could ignore the suggestion.

46:10Chris Romeo Humans are, humans are opportunistic.

46:12Izar Tarandach You can tell

46:12Chris Romeo a human,

46:14Izar Tarandach you can tell a human, if you don't follow this code standard, you're fired.

46:18Matt Coles And why can't you do the same with an AI?

46:20Izar Tarandach Because the AI doesn't care. It acts as if it does, but it doesn't.

46:25Chris Romeo Yeah, but if that, if that was true, we would have solved our problems a long time ago. Look, if, if we could have said, just, if you don't follow this, but as people, if we, if we were able to, to go to the engineering team and say, here's our secure coding standard, it's, I know it's 300 pages. If you don't follow this, you're fired. If it was that simple, we could have done it 20 years ago.

46:46Izar Tarandach We can't do that because as some Altman said, Nobody saw the, the, the, the, the curve coming, right? The, the, the intuition of nobody took security seriously, right?

47:00Chris Romeo Fabrication or something. I don't know what it's called.

47:02Matt Coles If the tool, if we hadn't, didn't have AI, you would've had better and better tooling, right?

47:07Izar Tarandach Yes.

47:08Matt Coles And we would've potentially still hit this curve over time.

47:12Izar Tarandach Yes. Potentially over time.

47:14Matt Coles But we just hit it so fast, right? This curve.

47:16Izar Tarandach Yes.

47:17Matt Coles On time went vertical.

47:19Izar Tarandach People just saw this all of a sudden. It's not that we hit it so fast. People just saw it all of a sudden. We've been telling people at a less steep angle for the past, I don't know how many years, but now all of a sudden it's thrown in their faces.

47:36Matt Coles By the way,

47:38Izar Tarandach by the way,

47:38Matt Coles by the way, you can fire your agent. It's called creating a new session. And this goes back to the throw it away and start from scratch.

47:46Izar Tarandach Right. But you can't just fire your

47:49Chris Romeo team. Okay. When

47:50Izar Tarandach you get mad at

47:50Chris Romeo their output,

47:51Matt Coles I can

47:51Izar Tarandach delete all I want.

47:53Chris Romeo No, I, I keep mine. I'm like, I don't care if you're at the context window. You and I are friends,

47:58Izar Tarandach but they

48:00Matt Coles copy

48:00Izar Tarandach that. That's clear. That's trust. But my point is that, um, no, that's

48:06Chris Romeo not trust. That's odd. You can say it.

48:09Matt Coles That's misplaced trust right there.

48:11Izar Tarandach My point is that LLMs are not compilers, and people keep relating to them as if. I'm going to say, do no mistakes, make no mistakes, and that's going to be my next pragma, and the compiler is going to always take that into consideration and not create these constructs, because the pragma is in there. LLMs are not compilers. Start talking to them or feeling them as they are.

48:33Matt Coles Compilers are deterministic.

48:35Izar Tarandach Exactly.

48:36Matt Coles They're rule-based.

48:37Izar Tarandach And if I had the mic, I would just drop it now, but I don't because it's expensive.

48:41Chris Romeo With that, we'll wrap up this episode because Izar wanted to have a mic drop, but I'm going to talk about, I'm going to talk over it so that the mic drop gets kind of run out to the end.

48:51Izar Tarandach Damn it, Carl.

48:52Chris Romeo Carl will be making an appearance soon on the AI Security Table. He's our correspondent. He's in the field. It's in the field, I should say.

49:02Matt Coles Somewhere.

49:03Chris Romeo We could actually send Carl into the CPU for an update. It's Carl coming to us from the CPU. Have the fan blowing in the background like he's a weather reporter.

49:12Matt Coles Wait, wait, wait. Not the CPU. He's not.

49:17Chris Romeo The GPU.

49:18Matt Coles The

49:18Chris Romeo GPU. Well, he can move around inside the computer components. Come on. So it'd be like an after-school special. He's just a bill on Capitol Hill. It'll be that kind of a style.

49:31Matt Coles He's writing the GPU. He's writing the NPU.

49:35Chris Romeo You gotta be a certain age to understand. I was, I'm just a bill on Capitol Hill.

49:41Matt Coles Just a Carl on my computer. There's no, it's, it doesn't roll off the tongue as well.

49:47Chris Romeo No. All right, folks. Thanks for listening to another episode of the AI Security Table. Thanks for joining us at the AI Security Table. Subscribe, rate, review, and follow wherever you listen. New episodes every week. AI Security on the Table.

Transcript supplied by AssemblyAI. It may contain transcription errors.