Earlier quoted context omitted.
Are you sensitive to colors?
[flagged]
[deleted]
Lean proved this program correct; then I found a bug
101–110 of 186 posts
Re: Lean proved this program correct; then I found a bug
#102Earlier quoted context omitted.
Repeating myself, 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.…
> when we speak of bugs in a verified software system, I think it's fair to consider the entire binary a fair target. I agree, but it’s not fair to imply that the verification was incorrect if the problem lies elsewhere. This is a nice example of how careful you have to be to build a truly verified system.
But is fair to state that the verification was *incomplete*, which is what the article does.
Re: Lean proved this program correct; then I found a bug
#103Earlier quoted context omitted.
Repeating myself, 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.…
> Repeating myself, when we speak of bugs in a verified software system, I think it's fair to consider the entire binary a fair target. Yes, and that would be relevant if this was a verified software system. But it wasn't: the system consisted of a verified X and unverified Y, and there were issues in the unverified Y. The article explicitly acknowledges this: "The two bugs that were found both sat outside the bounda…
the good news I guess are
1/ lean-zip is open source so it's much easier to have more Claude's eyes looking at it
2/ I don't think Claude could prove anything substantial about the zip algorithm. That's what lean is for. On the other side, lean could not prove much about what's around the zip algorithm but Claude can be useful there.
So in the end lean-zip is now stronger!
Re: Lean proved this program correct; then I found a bug
#104This article’s framing and title are odd. The author, in fact, found no bugs or errors in the proven code. She says so at the end of the article: > The two bugs that were found both sat outside the boundary of what the proofs cover. The denial-of-service was a missing specification. The heap overflow was a deeper issue in the trusted computing base, the C++ runtime that the entire proof edifice assumes is correct. St…
Repeating myself, 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.…
> 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.
Reminds of what some people in the Rust community do: they fight how safe this is or not. I always challenge that the code is composed of layers, from which unsafe is going to be one. So yes, you are righ to say that. Unsafe means unsafe, safe means safe and we should respect the meaning of those words instead of twisting the meaning for marketing (though I must say I heard this from people in the community, not from the authors themselves, ever).
Re: Lean proved this program correct; then I found a bug
#105Earlier 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…
Two different meanings of "forever" there. An OS runs for an arbitrarily large finite time, which is different from an infinite time.
Same way you can count to any finite integer with enough time, but you can never count to infinity.
Those kinds of interactive programs take in a stream of input events, which can be arbitrarily long, but eventually ends when the computer is shut down.
Termination checkers don't stop you from writing these interactive loops, they only stop non-interactive loops
Re: Lean proved this program correct; then I found a bug
#106You 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.
Indeed this is a nice discovery and I think it is useful in its own right.
Re: Lean proved this program correct; then I found a bug
#107claude making a statement that sounds impressive but it is actually the first codebase it has ever analyzed. "This is genuinely one of the most memory-safe codebases I've analyzed."
Maybe we do not know what Claude has been doing and he keeps it secret...? :D
Re: Lean proved this program correct; then I found a bug
#108Earlier quoted context omitted.
Sorry, I'm not sure I follow. We are talking about bugs in a verified system, that is, in this case, a verified implementation of a zlib-based compression tool. Did it have bugs? yes. Several in fact. I'd recommend reading the article for a detailed listing of the bugs in the tool.
Further to my earlier reply - a more succinct way to look at it might be: - When they fix the run time, bug A goes away. So the proof still holds and the zlib code is still correct. - When they add a system of proofs for the parser and modify that, then bug B goes away. So the proof still holds and the zlib code is still correct; and now more of the library is proven correct. The formulation of the title is "I was to…
What is the program?
There are two different answers to this question, and which one is "correct" depends entirely on the context of who is asking it.
1. It's the code that is specific to this program that sits above the run-time layer (internal view, that most programmers would take).
2. It's the code in the binary that is executed (external view, that most users would take).
The key question does not seem to be "was the proof correct", rather "did the proof cover everything in the program". The answer depends on whether you are looking at it from the perspective of a programmer, or a user. Given the overly strong framing that the article is responding to - highlighting the difference in this way does seem to be useful. The title is correct from the perspective that most users would take.
Re: Lean proved this program correct; then I found a bug
#109This article’s framing and title are odd. The author, in fact, found no bugs or errors in the proven code. She says so at the end of the article: > The two bugs that were found both sat outside the boundary of what the proofs cover. The denial-of-service was a missing specification. The heap overflow was a deeper issue in the trusted computing base, the C++ runtime that the entire proof edifice assumes is correct. St…
Yeah, the title made me think the author found a bug in the Lean kernel, thus making an invalid proof pass Lean's checks. The article instead uncovers bugs in the Lean runtime and lean-zip, but these bugs are less damning than e.g. the kernel, which must be trusted to be correct, or else you can't trust any proof in Lean.
When the Lean runtime has bugs, all Lean applications using the Lean runtime also have those bugs. I can’t understand people trying to make a distinction here. Is your intent to have a bug free application or to just show the Lean proof kernel is solid?? The latter is only useful to Lean developers, end users should only care about the former!
Re: Lean proved this program correct; then I found a bug
#110This article’s framing and title are odd. The author, in fact, found no bugs or errors in the proven code. She says so at the end of the article: > The two bugs that were found both sat outside the boundary of what the proofs cover. The denial-of-service was a missing specification. The heap overflow was a deeper issue in the trusted computing base, the C++ runtime that the entire proof edifice assumes is correct. St…
To me, saying that there is a bug in the lean runtime means lean-zip has a bug is like saying a bug in JRE means a Java app that uses the runtime has a bug, even though the Java app code itself does have a bug. It seems like the author is being intentionally misleading about his findings.
No. It would be like finding a memory unsafe caused bug in a Java application that is due to a bug in the JRE. That would absolutely warrant a title like “I found memory unsafe bug in my Java code” when everyone expects Java code to be memory safe, which is analogous to the article in question.