You guys are missing the forest for the trees.
They used an AI agent sending ideas to a fuzzer and discovered a heap buffer overflow in Lean. This is big.
Lean proved this program correct; then I found a bug
51–60 of 186 posts
Re: Lean proved this program correct; then I found a bug
#52Earlier quoted context omitted.
This feels like a thought exercise rather than an argument. By your logic, it's impossible to prove that a car is driving at 60mph. There could be an error in the speedometer which makes it impossible to verify that said car is going at the speed. You can get asymptomatically close to being sure that you're driving at 60 mph but you can never be 100% sure. This is useless and serves no purpose.
That's not correct. You can prove a car is driving 60mph as soon as you measure it doing that. "proving a negative" is for statements like "There are no purple zebra". You can never prove this because there is always the possibility the purple zebra is somewhere you haven't looked yet. As soon as you find one the statement becomes falsified, but until then it always remains unresolved even if almost certainly true. L…
You can prove there is no purple zebra on earth by actually surveying the population of zebras which is finite.
Re: Lean proved this program correct; then I found a bug
#53I’ve had similar experiences with code I’ve proven correct, although my issues were of the more common variety than the overflow issue - subtle spec bugs. (I think the post mentions the denial of service issue as related to this: a spec gap) If you have a spec that isn’t correct, you can certainly write code that conforms to that spec and write proofs to support it. It just means you have verified a program that does…
Whenever I read an article about formal verification systems there is always that nagging thought in the back of my head. Why can you trust your formal verification system to be bug free but you can't trust the program. should not the chance of bugs be about equal in both of them? You have a program that does something and you write another program to prove it. What assurance do you have that one program has fewer bu…
> Whenever I read an article about formal verification systems there is always that nagging thought in the back of my head. Why can you trust your formal verification system to be bug free but you can't trust the program. should not the chance of bugs be about equal in both of them?
A bug in the formal verification tool could be potentially noticed by any user of that formal verification tool. (And indirectly by any of their users noticing a bug about which they say "huh, I thought the tool told me that was impossible.")
A bug in your program can only be potentially noticed by you and your users.
There are also entirely categories of bugs that may not be relevant. For instance, if I'm trying to prove correctness of a distributed concurrent system and I use a model+verifier that verifies things in a sequential, non-concurrent way, then I don't have to worry about the prover having all the same sort of race conditions as my actual code.
But yeah, if you try to write your own prover to prove your own software, you could screw up either. But that's not what is being discussed here.
Re: Lean proved this program correct; then I found a bug
#54I’ve had similar experiences with code I’ve proven correct, although my issues were of the more common variety than the overflow issue - subtle spec bugs. (I think the post mentions the denial of service issue as related to this: a spec gap) If you have a spec that isn’t correct, you can certainly write code that conforms to that spec and write proofs to support it. It just means you have verified a program that does…
Whenever I read an article about formal verification systems there is always that nagging thought in the back of my head. Why can you trust your formal verification system to be bug free but you can't trust the program. should not the chance of bugs be about equal in both of them? You have a program that does something and you write another program to prove it. What assurance do you have that one program has fewer bu…
I think formal verification brings a bit more to the table. The logical properties are not just a second implementation. They can be radically simpler. I think quantifiers are doing a lot of work here (forall/exists). They are not usable directly in regular code. For example, you can specify that a shortest path algorithm must satisfy:
forall paths P from A to B:
len(shortest(A,B)) Re: Lean proved this program correct; then I found a bug
#55I’ve had similar experiences with code I’ve proven correct, although my issues were of the more common variety than the overflow issue - subtle spec bugs. (I think the post mentions the denial of service issue as related to this: a spec gap) If you have a spec that isn’t correct, you can certainly write code that conforms to that spec and write proofs to support it. It just means you have verified a program that does…
Whenever I read an article about formal verification systems there is always that nagging thought in the back of my head. Why can you trust your formal verification system to be bug free but you can't trust the program. should not the chance of bugs be about equal in both of them? You have a program that does something and you write another program to prove it. What assurance do you have that one program has fewer bu…
Formal verification is just an extra step up from the static types that you might have in a language such as Rust.
Common static types prove many of the important properties of a program. If I declare a variable of type String then the type checker ensures that it is indeed a String. That's a proof. Formal verification takes this further and proves other properties such as the string is never empty.
Common static types are very effective. Many users of Rust or Haskell will claim that if a program compiles then it usually works correctly when they go to run it.
However there is a non-linear relationship between probability of program correctness and the amount of types required to achieve it. Being almost certain requires vastly more types than just being confident.
That's the real issue with formal verification, being 75% sure and having less code is better than being 99% sure in most situations, though if I were programming a radiotherapy machine I might think differently.
Re: Lean proved this program correct; then I found a bug
#56Nice work. Amusing that Lean's own standard library has a buffer overflow bug, which "leaked out" due to being exempted from the verification.
Regarding the DoS in the lean-zip application itself: I think this is a really neat example of the difficult problem of spec completeness, which is a subcase of the general problem (mentioned by porcoda in a sibling comment) of being sure that the spec is checking the right things. For a compression program, the natural, and I would also say satisfyingly beautiful thing to prove is that decomp(comp(x)) = x for all possible inputs x. It's tempting to think that at that point, "It's proven!" But of course the real world can call decomp() on something that has never been through comp() at all, and this simple, beautiful spec is completely silent on what will happen then.
Re: Lean proved this program correct; then I found a bug
#57I'll probably get a lot of hate mail for this but here goes nothing... Despite what many people like to claim, you cannot prove that a program has no bugs. That means proving the absence of bugs, and you cannot prove a negative. The best thing you can do is fail to find a bug, but that doesn't mean it isn't there. Before everyone starts blabbing about formal verification, etc., consider this: how do you know that you…
Formal methods practitioner here.
> That means proving the absence of bugs, and you cannot prove a negative. The best thing you can do is fail to find a bug, but that doesn't mean it isn't there.
You can conclusively (up my next point) prove a specific bug or class of bugs aren't there. But "entirely free of (all) bugs" is indeed a big misconception for what formal methods does.
> how do you know your formal verification is bug-free? Answer: you don't. Or if you try to formally verify your formal verification then you're just translating the problem to a new layer. It's just a chain of proofs that is always ultimately based on an unproven one, which invalidates the whole chain.
It's another misconception of formal methods to say that any result is established conclusively, without any caveats whatsoever. But then again neither is mathematics, or any other intellectual discipline. What formal methods does is reduce the surface area where mistakes could reasonably be expected to reside. Trusting the Rocq kernel, or a highly scrutinized model of computation and language semantics, is much easier than trusting the totality of random unannotated code residing in the foggiest depths of your average C compiler, for instance.
Re: Lean proved this program correct; then I found a bug
#58Earlier quoted context omitted.
And Alonzo Church proved in 1940 that you can avoid this problem by using a typed language in which all programs halt. But sadly some programmers still resist this.
Some correct programs are supposed to run forever. When is an OS supposed to halt? When you shut it down, or when you power down the hardware, and no other times . So if you don't do either of those things, then the OS is supposed to run forever. Does that, by itself , mean that the program is incorrect, or that the language is inadequate? No, it means that the definition is worthless (or at least worthless for progr…
you can still verify arbitrarily long running programs - there are instances of such software, such as sel4 (https://sel4.systems/) and certikos (https://flint.cs.yale.edu/certikos/), you simply model them as finite programs that run on an infinite stream of events.
Re: Lean proved this program correct; then I found a bug
#59Earlier quoted context omitted.
Been thinking about this a lot recently. I think we need a way to verify the specs. A combo of formal logic and adversarial thinking (probably from LLMs) that will produce an exhaustive list of everything the program will do, and everything it won’t do, and everything that is underspecified. Still not quite sure what it looks like, but if you stipulate that program generation will be provable, it pushes the correctne…
What’s important is to prove useful, high-level properties derived from the specs. The specs of program behavior are just the price of admission.
I agree. It’s kind of like secure boot, in reverse: the high level stuff has to be complete and correct enough that the next level down has a chance to be complete and correct.
Re: Lean proved this program correct; then I found a bug
#60Earlier quoted context omitted.
And Alonzo Church proved in 1940 that you can avoid this problem by using a typed language in which all programs halt. But sadly some programmers still resist this.
Some correct programs are supposed to run forever. When is an OS supposed to halt? When you shut it down, or when you power down the hardware, and no other times . So if you don't do either of those things, then the OS is supposed to run forever. Does that, by itself , mean that the program is incorrect, or that the language is inadequate? No, it means that the definition is worthless (or at least worthless for progr…
This is not actually a problem for total languages, which simply model these kinds of processes using corecursion/coinduction/codata.