Formal verification proves specific bug classes are absent

Transcript

Transcribed by machine (Whisper) from the episode’s audio, so a word may be off here and there.

1. 2:44

   exactly what Aristotle does. So when things are more verifiable, explain how that prevents hacks. Well, it doesn't prevent all hacks. So I think there's a meme on Twitter that, you know, verifying everything prevents all bugs. You can imagine verifying code just means that you're 100% sure the code does what it says it does. So if you formally verified some code, like a web server, and then you run it with a configuration that says the password to it is password, you're going to get hacked no matter how verified that code is but but it turns out a lot of exploits in really security sensitive code like c code chains together these things called memory exploits where the programmer allows for some behavior that was not intended like writing to some memory you don't own or using some data after you technically had permission to use it and then combining memory

2. 3:36

   exploits with things like privilege escalation other bad behavior if you can completely get rid to that first class of issues like memory safety issues, you actually limited a lot of vectors for hacks. And so that's one way in which verifying your code can reduce your risk of security breaches. If we're thinking of a specific example, for example, the Binance theft, this is 6.3. three billion dollars is one of the probably the biggest crypto hack ever to date can aristotle help out here is there anything that aristotle could have done to rule it out and prevent this attack well i think that one happened yesterday so i don't know if anyone knows exactly outside of binance knows exactly what happened there um we do have some security related things we've discovered in very popular open source systems that we're gonna work with the maintainers to

3. 4:28

   fix and those we know we've prevented hacks also if you just look back at the history of hacks i mean there was this hugely popular one called or famous one called heart bleed do you remember that yeah yeah heart bleed was a classic memory safety issue and if you had run aerosol on the code you of course would have caught it and then fixed it ahead of time yeah so tell us a little bit about this i mean right now you have ai is now running a lot of these verifications itself and you have like AI actually verifying its own output. But that's not always that reliable. It's not always 100% verifiable in that way. And so tell us a little bit about what are the other systems that people are using for verification and why that's not something that can scale into what we need now. Yeah, I think the biggest conceptual difference is that for 40 years in software

4. 5:20

   engineering, what we've been getting better at is bug finding. So you used to have humans find bugs and then they find security bugs. And now these latest AI systems that are really, really powerful, still what they're doing is finding bugs. But the thing is, if you have a really powerful AI system that finds bugs, you don't really know when you're done. So you can always run it more and see if it finds some other bug. But let's say you run an AI system to try to find a bug in your code base and it says, I haven't found a bug. You can't really be 100% sure that you've ruled out an entire class of bugs. That's where formal verification is a bit different. When it comes to certain classes of errors, like the memory safety one, like certain privilege escalation issues, with formal verification, you get a checkmark that you've actually analyzed all the possible bugs that

5. 6:03

   could arise and you prove that none exist. So that's one way in which it's different. You know when you're done. And the other way in which it's different is what I mentioned before, which is that here you have a formal system that's checking the AI reasoning. So it is a computer tool, but it's not a non-deterministic one like AI. It's one that really just runs an algorithm that's very simple and checks reasoning step by step. Yeah. And it also just comes to actually doing