Podcast
Root Causes 436: Formal Proofs
Hosted by
Tim Callan
Chief Compliance Officer
Jason Soroko
Fellow
Original broadcast date
October 29, 2024
Formal proofs are critical to cryptography. We discuss how better processes and AI can accelerate formal proofs of cryptographic concepts.
Podcast Transcript
Tim CallanSo I feel like I'm going to be taken all the way back to high school, Jay, because you want to talk to me about proofs.
Jason SorokoShow your work. Divide this number by this number and show me your work.Tim CallanQED.Jason SorokoI remember those days too.Tim CallanLet's talk about proofs.Jason SorokoSo all of a sudden, formal proofs, which have been around forever, but they could become really important when we're trying to accelerate our trust in cryptographic algorithms.During these Toronto sessions, we talked about things such as diversity in cryptographic algorithms and different math and how do we know any of this stuff is trustworthy. How do we know it's secure?
Tim CallanSo let's start with, how do we know RSA is trustworthy?Jason SorokoAnd I'll tell you what, what that comes down to is, I think that - -Tim CallanNobody has broken it yet, and a lot of people have tried.Jason SorokoNobody has broken yet and it's taken a long time, and it still holds, but it could be deprecated tomorrow morning.And it would be deprecated by really, really clever math. Quadratic sieve is a type of math where it's basically pattern finding. You might recall my little explanation about pattern finding in Shor's algorithm.
So, formal proofs. I want to talk about not just the formal proofs themselves. That's awfully dry. That's dry like the Nevada desert. Where's the juiciness in that story right now?
Leonardo de Moura - and I could be pronouncing his name wrong. I have not personally met the man. I believe he's out of England. Worked originally in Microsoft research and came up with an idea, I think around 2013, of hey, can we codify formal proofs?
So in other words, not just computer assisted formal proofs, but can we write a formal proof, turn it into a language like C++?
So Fermat’s Last Theorem, correct me if I'm wrong world, I'm not even I'm not looking at notes. I'm doing this off the cuff. I think Fermat’s Last Theorem was written up in about 100 pages of paper. And that's Fermat’s Last Theorem. And you really have to understand the symbology of the math to prove it out. In other words, good old-fashioned high school show your work is what this person did in order to be able to prove Fermat’s Last Theorem. So there's the theory and there's the proof for it that's written out. But what happens if you could proof as code? Would that help us to utilize AI in proofing? In other words, computer-assisted proofs. In other words, iterating the kicking of the can.
Tim CallanSure. You could see that being a very interesting application of AI. Where you let it kind of give you candidates of proofs, and then those would still be vetted by humans to make sure we agree, but it might get us to places that would be really hard to get to on our own.Jason Soroko100%. And AI I'm just throwing out as a why not. It's a buzz term. But we can also, through good old-fashioned, classic ways of doing things, just accelerate the iteration of finding what's the scenario that would unravel this cryptographic algorithm. And I would say that with these kinds of new computer assisted means, codifying the proofs, there couldn't be a more important time than now to start really putting the foot to the gas pedal of these kinds of innovations, because we don't have the trust yet in these post-quantum cryptographic algorithms. Lattice has a lot of promise, but you've heard yourself, Tim, the amount of like, geez, we don't want to put all the eggs in that basket.And the reason is because we don't have the kind of trust in it that we do with RSA or even ECC. What happens if we could write a true formal proof for it?
Tim CallanLike I understand the principle here. The principle is true formal proof is you do something mathematically that proves, in a way that's indisputable by anybody who looks at it, that you basically can't circumvent or break this cryptographic algorithm? And maybe this is a naive question, but isn't that proof itself based on a set of assumptions and a framework, and if someone could have an idea that is outside those assumptions and framework, doesn't that mean that the proof didn't deal with that?Jason SorokoWell, let's talk about ECC. And the answer is yes in that case. ECC as a math, solving for points on that elliptic curve, well, it turns out that if you chose the wrong parameters for the curve, everything fell apart.But then that was figured out, and there was a three letter agency that was involved in that shenanigans. Let's not talk about that. I don't want to get into controversial stuff in this podcast, but there you go. Therefore, yes, but then, therefore you could put an additional set of proofs on well, here are the acceptable parameters and other assumptions.
Tim CallanThen that assumes that that's fine, but then it all hinges on your assumptions being right, and if your assumptions are not right, if your assumptions are, let's say, too narrow, then that's a problem.Jason SorokoHowever, words aren't used lightly in math, and so when we say proof, we mean proof. It's not like, let's go out in the street and look at some marketing when they say they approve something. It's not the same kind of proof, where it's loosey goosey proof. You're right in saying that part of the academic community back when I was part of it, being upfront about your assumptions was what made you a good scientist.Jason SorokoThe better you were about declaring your assumptions, the better you were as a scientist. And those are the people who were truly respected.Let's talk about Fermat’s Last Theorem as an example. Not a lot of assumptions going on. Like the equation that was written out is right there in front of you. And is it true, or is it not true? Is now understood by Fermat's Last Theorem proof as being no this is proven. And so when we talk about cryptographic algorithms, there are a finite number of assumptions. So it's not like oops, we missed an assumption. So if we were in a type of environment with ECC, where oops, we missed an assumption about parameters, then that situation did, in fact, occur, but that was just because I think things were being sloppy. Now, that's controversial. I don't really want to get into that so much, but I think to answer your question is lattice geometry appropriate? I think that a formal proof could probably be written for that. It is a certain number of parameters around the way that you choose specific geometries. Is this appropriate for a post-quantum algorithm? Therefore, just in asking that question lays out some of the assumptions. Therefore you can write a proof about that. So would we find other assumptions or other problems that would help to unravel after that? I think this is what the exercise really needs to be. But this is really all about talking about how we can utilize the tools we have in order to be able to kick the can harder and faster.
Tim CallanSo is that being done today?Jason SorokoComputer-assisted proofs I think are used all over the place. Look, I can't speak for the teams who are coming up with these cryptographic algorithms, but if you look at some of the paperwork, the research papers that are around this, you can tell there's some, definitely some classical proofs being done to help to make people understand pieces of the story. But I think complete proof sets that are codified are something that we're probably a ways away from getting but I definitely think that's there's some exciting innovation in the tool sets in order to be able to do that. That's really what this is all about.Tim CallanAll right. Cool. Thank you, Jay.Jason SorokoThank you, Tim.Tim CallanThis has been Root Causes.Stay informed with expert insights
Subscribe to Root Causes for engaging discussions on PKI, digital security, and best practices for protecting your organization's critical assets. Don’t miss an episode!
