by gopiandcode 3 days ago
Hi! Author here. When we speak of bugs in a verified software system, I think it's fair to consider the entire binary a fair target.
If a buffer overflow causes the system to be exploited and all your bitcoins to be stolen, I don't think the fact that the bug being in the language runtime is going to be much consolation. Especially if the software you were running was advertised as formally verified as free of bugs.
Secondly, I did find a bug in the algorithm. in Archive.lean, in the parsing of the compressed archive headers. That was the crashing input.
> I think it's fair to consider the entire binary a fair target.
Yes, it's still very much a bug. But it has nothing to do with your program being formally verified or not. Formal verification can do nothing about any unverified code you rely on. You would really need a formal verification of every piece of hardware, the operating system, the runtime, and your application code. Short of that, nobody should expect formal verification to ensure there are no bugs.
I read it as that’s also the point. Adding formal verification is not a strict defense against bugs. It is in a way similar to having 100% test coverage and finding bugs in your untested edge cases.
I don’t think the author is attempting to decry formal verification, but I think it a good message in the article everyone should keep in mind that safety is a larger, whole system process and bugs live in the cracks and interfaces.
You're right. It just seems as though it should be self-evident. Especially to those sophisticated enough to understand and employ formal verification.
It does seem that way doesn't it? But as software bugs are becoming easier to find and exploit, I'm expecting more and more people, including those not "sophisticated enough" to understand and employ formal verification to start using it
> I'm expecting more and more people
Then it would help to not introduce any confusion into the ecosystem by using a click-baity title that implies you found a bug which violated the formal specification.
We should not cater to people who make decisions based on titles instead of reading the actual article.
That's a shitty rationale for click-bait titles. Good titles are for the benefit of people who actually read the articles too.
Thanks for responding!
> When we speak of bugs in a verified software system, I think it's fair to consider the entire binary a fair target.
Yeah, I would actually agree. We wouldn't want to advertise that a system is formally verified in some way if that creates a false sense of security. I was just pointing out that, by my reading, the title appears to suggest that the core mechanism of the Lean proof is somehow flawed. When I read the title, I immediately thought, "Oooh. Looks like someone demonstrated a flaw in the proof. Neat." But that's not what is shown in the article. Just feels a bit misleading is all.
OK, so now I see the shadow edit you did for the code source, thanks. Unfortunately, it shows that you are incorrect. For one, the function is a private function and can only be called by local code. Everywhere that the function is called, the size given to it is verified by the program; there is even a note that says it limits the maximum zip file size to avoid a zip bomb. In addition, the code you are quoting isn't even the final code; it is an interim step from what Claude was iterating on. Sucks that this got so much traction, as you are purposely being deceptive in trying to say that this is a bug. You intentionally removed the 'private' keyword in the function signature, as you knew that it would tip off most people to then check when it is actually used.
sorry to hijack the thread. Really cool post. How long did the whole exercise including porting zlib to lean take?
i have a hard real time system that i would love to try this on, but that's a lot of tools to learn and unclear how to model distributed systems in lean.
also, please add rss so i could subscribe to your blog
Lean-zip was not my project but one by others in the lean community. I'm not sure about the methodological details of their process - you might want to check with the original lean-zip authors (https://github.com/kim-em/lean-zip)
I notice you didn't put a code reference for the second bug. Where is the code exactly?