Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Lean proved this program correct; then I found a bug

kirancodes.me

Post reply on HN
Print view View original

151–160 of 186 posts

Re: Lean proved this program correct; then I found a bug

#151

Post by amoss »

danparsonson wrote: post #113
amoss wrote: post #108

Earlier quoted context omitted.

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 "wa…

Yes but, without wishing to be snarky, did you read the article? There is no program as such, in either sense - the announcement from Lean only mentions "a C compression library" (zlib). Not only that, but since we're talking about formal verification, a programmer would likely understand that that is about proving a bounded, specific codebase at source code level, and not operating on a binary along with its associa…

The article describes fuzzing the library, this execution requires a program to be compiled. Typically fuzzing involves a minimal harness around the payload (a single call into the library in this case). There is clearly a bug in this program, and it does not exist in the minimal harness. It must be in the library code, which was covered by the proof.

The bounded, specific codebase that you refer to is typically the library *and all of its dependencies*, which in this case includes the Lean runtime. This is why formal verification is difficult: the proof chain needs to extend all the way down to the foundations. In this case the original gushing claim that everything was verified is incorrect and premature. The article seems like a good exposition of why.

Re: Lean proved this program correct; then I found a bug

#152

Post by NewsaHackO »

brabel wrote: post #110
NewsaHackO wrote: post #77

Earlier quoted context omitted.

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.

I do not think you are completely grasping what you are talking about (what is a 'memory unsafe bug'?). Even in the example you give, that title would be literally wrong, as there will be no bug in your Java code; there would be a bug in the execution due to a deviation in the runtime executing your program.

Re: Lean proved this program correct; then I found a bug

#153

Post by IshKebab »

gopiandcode wrote: post #148
IshKebab wrote: post #123

Earlier quoted context omitted.

> if the software you were running was advertised as formally verified as free of bugs. Nobody should be advertising that. Even ignoring the possibility of bugs in the runtime, there could also be bugs in the verifier and bugs or omissions in the specification. Formally verified never means guaranteed to be free of bugs.

As quoted in the article itself, please take it up with the chief architect of the Lean FRO: > ... converted zlib (a C compression library) to Lean, passed the test suite, and then proved that the code is correct. > Not tested. Proved. For every possible input. lean-zip

Yeah well he shouldn't. That looks like slop tbf.

Re: Lean proved this program correct; then I found a bug

#155

Post by ctmnt »

gopiandcode wrote: post #147
ctmnt wrote: post #126

Earlier quoted context omitted.

Yes, it isn’t performant. Lean isn’t a language for writing software, though you technically can; it’s a language for proving math.

Where are you coming up with this from? This is awfully confident for a fact you seem to have conjured up without evidence. As far as I am aware, Lean is interested in being used as a programming language (see: https://lean-lang.org/functional_programming_in_lean/ ) and people are deploying Lean in production: https://docs.aws.amazon.com/clean-rooms/latest/userguide/dif...

You’re right, there is that one example. Feels like we’re in exception that proves the rule territory. But I’d be very interested in being proven wrong! This isn’t a desire of mine, just what I’ve seen. Do you have other examples?

Also, part of my confidence comes from both having been a professional programmer for decades, across many languages, and also having programmed in Lean. It’s a great language for math, perhaps the best choice right now. But as a general purpose language it’s incredibly quirky.

Re: Lean proved this program correct; then I found a bug

#156

Post by ctmnt »

gopiandcode wrote: post #145
ctmnt wrote: post #129

Earlier quoted context omitted.

Hi Kiran, thanks for following up. FWIW, I enjoy your blog and your work. And I do think it was a valuable bug you found; also nice to see how quickly Henrik fixed it. Say more about people running Lean in production. I haven’t run into any. I know of examples of people using Lean to help verify other code (Cedar and Aeneas being the most prominent examples), but not the actual runtime being employed. I took a quick…

Yes, here's a concrete example: https://github.com/leanprover/SampCert This is an implementation of a verified sampler, in lean. Not an embedding in some other language. The implementation itself is in lean, and a python ffi is used to call into the verified implementation. I don't know if AWS is big enough for your standards, but here is at least one example. Besides that, I'm more reporting on the general vibe I ha…

You’re right, I should have been more careful in my reference to AWS. No need to be snarky about it.

Let me rephrase: aside from that one example from a couple years ago, I haven’t seen any examples of production code written in Lean. I’d be very interested in being proven wrong, this isn’t something I desire, just what I’ve observed. Have you seen any others?

More generally, you implicitly make a good point: writing important libraries in Lean and calling in from another language is probably the most likely use case. So not programs / apps / binaries written in Lean, but small critical components.

Re: Lean proved this program correct; then I found a bug

#157

Post by NewsaHackO »

aidenn0 wrote: post #84
NewsaHackO wrote: post #77

Earlier quoted context omitted.

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.

I think it's ambiguous and fair game for the idea of answering the question "if we write programs in this manner, will there be exploitable bugs?

>I think it's ambiguous and fair game for the idea of answering the question "if we write programs in this manner, will there be exploitable bugs?

You're strawmanning the original authors' argument. The creator of lean-zip said that they proved there are no implementation bugs in the lean-zip program. A bug in lean-runtime does not contradict this claim.

Re: Lean proved this program correct; then I found a bug

#158

Post by j2kun »

grg0 wrote: post #24

Clickbait title, the proved part of the program had no bugs? As an aside, why can't people just write factually? This isn't a news site gamed for ad revenue. It's also less effort. I felt this post was mostly an insulting waste of time. I come to HN to read interesting stuff.

It reads to me as a cogent and measured response to a very clickbaity advertisement about the result.

> Not tested. Proved. For every possible input.

Finding inputs that crashed and then saying, "be clear about what is in the scope of what you proved" is interesting and factual.

Re: Lean proved this program correct; then I found a bug

#159

Post by danparsonson »

amoss wrote: post #151
danparsonson wrote: post #113

Earlier quoted context omitted.

Yes but, without wishing to be snarky, did you read the article? There is no program as such, in either sense - the announcement from Lean only mentions "a C compression library" (zlib). Not only that, but since we're talking about formal verification, a programmer would likely understand that that is about proving a bounded, specific codebase at source code level, and not operating on a binary along with its associa…

The article describes fuzzing the library, this execution requires a program to be compiled. Typically fuzzing involves a minimal harness around the payload (a single call into the library in this case). There is clearly a bug in this program, and it does not exist in the minimal harness. It must be in the library code, which was covered by the proof. The bounded, specific codebase that you refer to is typically the…

Thank you, I understand what fuzzing is; that test harness was presumably provided either by the blog post author or generated by Claude somehow, and therefore would not have been part of the proven code, nor part of the original claim by the Lean devs. That's what I meant by saying there is no program as such.

> The bounded, specific codebase that you refer to is typically the library and all of its dependencies, which in this case includes the Lean runtime.

How does that work? I thought the main idea is to write code in the Lean language which has some specific shape conducive to mathematical analysis, along with mathematical proofs that operate on that code. How then does a system like this handle a third party dependency? I've searched around and I can't find any information about how it works. I assumed that the boundary of the proof was the source code - surely they can't also be proving things like, say, DirectX?

> This is why formal verification is difficult: the proof chain needs to extend all the way down to the foundations.

The difficulty is not in explosions of computational complexity due to problems of incompleteness, decidability, the halting problem, those kinds of things? As I said this is not something I know much about but it's surprising to me if 'analysing all the code' is really the difficult bit.

Re: Lean proved this program correct; then I found a bug

#160

Post by NewsaHackO »

gopiandcode wrote: post #7
davesque wrote: post #3

Am I reading the article wrong? It appears that the author did not test the claims of the proof. Wouldn't a "bug" in this case mean she found an input that did not survive a round trip through the compression algorithm? Update: Actually, I guess this may have been her point: "The two bugs that were found both sat outside the boundary of what the proofs cover." So then I guess the title might be a bit click baity.

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.…

I notice you didn't put a code reference for the second bug. Where is the code exactly?
Post reply on HN