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

161–170 of 186 posts

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

#161

Post by DonaldPShimoda »

gopiandcode wrote: post #58
AnimalMuppet wrote: post #50

Earlier quoted context omitted.

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.

> finite programs that run on an infinite stream of events

This requires coinduction, right? (That's my understanding of the formal representation of infinite streams.) If so, that does limit your options, since most of the proof assistants don't handle coinductive data, as I understand it.

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

#162

Post by spinningslate »

SAI_Peregrinus wrote: post #150
danparsonson wrote: post #66

Earlier quoted context omitted.

We're not speaking about bugs in a verified system so much as writing articles making specific claims about that. Surely if we're at the level of precision of formal verification, it's incumbent upon us to be precise about the nature of a problem with it, no? "Lean proved this program correct and then I found a bug" heavily implies a flaw in the proof, not a flaw in the runtime (which to my mind would also be a compe…

Or it implies a bug in the specification. The spec differing from the intent is a frequent source of bugs, it doesn't matter what language the spec is written in. Most people have experience with (or have seen news stories about) specification bugs in natural-language specifications: legal loopholes!

This is the biggest risk with the rejuvenated interest in formal proof. That LLMs can generate proofs is useful. Proof assistants that can check them (Lean/FStar/Isabelle/...) similarly so.

But it just moves the question to whether the theorems covered in the proof are sufficient. Underlying it all is a simple question:

Does the system meet its intended purpose?

To which the next question is:

What is the intended purpose?

Describing that is the holy grail of requirements specification. Natural language, behaviour-driven development, test-driven development and a host of other approaches attempt to bridge the gap between implicit purpose and explicit specification. Proof assistants are another tool in that box.

It's also one of the key motivators for iterative development: putting software in front of users (or their proxies) is still the primary means of validation for a large class of systems.

None of which is implied criticism of any of those approaches. Equally, none completely solves the problem. There is a risk that formal proofs, combined with proof assistants, are trumpeted as "the way" to mitigate the risk that LLM-developed apps don't perform as intended.

They might help. They can show that code is correct with respect to some specification, and that the specification is self-consistent. They cannot prove that the specification is complete with regards its intended purpose.

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

#163

Post by thomastjeffery »

ctmnt wrote: post #6

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

Misalignment of trust is a category of bug in my book; right next to logic error.

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

#164

Post by necovek »

eithed wrote: post #144
necovek wrote: post #91

Earlier quoted context omitted.

A test suite never proves anything except that the code works for the test cases in it. But yes, it would be equivalent to stating "No tests failed but I found a bug" and one would correctly deduce that test coverage is insufficient.

These were my thoughts as well and it's nothing new, I think, regarding testing altogether: - testing libraries (and in this case - language itself) can have bugs - what is not covered by tests can have bugs Additionally would add that tests verify the assumptions of coder, not expectations of the business. To give benefit to the author - I'd read the article as: having tests for given thing ensures that it does the…

I like to differentiate between coverage by lines and semantic coverage: sometimes you need to exercise a single line multiple times to get full semantic coverage, and better semantic coverage usually beats larger line coverage for detecting problems and preventing regressions.

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

#165

Post by eithed »

necovek wrote: post #164
eithed wrote: post #144

Earlier quoted context omitted.

These were my thoughts as well and it's nothing new, I think, regarding testing altogether: - testing libraries (and in this case - language itself) can have bugs - what is not covered by tests can have bugs Additionally would add that tests verify the assumptions of coder, not expectations of the business. To give benefit to the author - I'd read the article as: having tests for given thing ensures that it does the…

I like to differentiate between coverage by lines and semantic coverage: sometimes you need to exercise a single line multiple times to get full semantic coverage, and better semantic coverage usually beats larger line coverage for detecting problems and preventing regressions.

I think mutation testing helps in defining semantic coverage, if I understand what you're saying

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

#166

Post by amoss »

danparsonson wrote: post #159
amoss wrote: post #151

Earlier quoted context omitted.

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 , w…

There are standard convex assumptions to handle incompleteness, decidability etc, i.e. the results are an over-approximation that terminates. Picking a approximation that is precise enough in the properties that you care about is part of the challenge, but it is an in-band problem. There are no hard edges between the theory and reality.

As with most engineering problems the out-of-band issues tend to be the hardest to solve. Models of the part underneath the interesting part need to be complete/accurate enough to make the results useful. Compare it to crypto where people do not usually try to break the scheme - they try to break the specific implementation of the scheme because the weakest points will be at the interface between the theoretical construction and the actual concrete instantiation of the device that it will run on.

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

#167

Post by [deleted] »

minimaltom wrote: post #40
nickvec wrote: post #28

Earlier quoted context omitted.

Yeah, extremely misleading title even if it is technically true semantically. The phrasing gives the impression that a bug was found in `lean-zip` as part of the proof boundary when it was part of the unverified archive-handling code.

The archive-handling code was in lean-zip, it just seems the verifiers forgot to write proofs for it (still a bug). Thats not the main finding of the article however. The main bug found was actually in the lean runtime, affecting all proofs using scalar arrays where the size of the array is not bounded.

[deleted]

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

#168

Post by NewsaHackO »

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.

Also, he even just created the second bug out of thin air. There is no code reference, and the reason why he downplays it is because he knows that if someone looks into it, they will realize he misrepresented the actual code.

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

#169

Post by aidenn0 »

NewsaHackO wrote: post #157
aidenn0 wrote: post #84

Earlier quoted context omitted.

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.

I'm saying that both the headline of TFA and the statement of the lean-zip creator can be correct.

If they e.g. specially crafted a .zip file that caused it to flip bits via row-hammer like memory accesses, the same would be true.

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

#170

Post by necovek »

eithed wrote: post #165
necovek wrote: post #164

Earlier quoted context omitted.

I like to differentiate between coverage by lines and semantic coverage: sometimes you need to exercise a single line multiple times to get full semantic coverage, and better semantic coverage usually beats larger line coverage for detecting problems and preventing regressions.

I think mutation testing helps in defining semantic coverage, if I understand what you're saying

Yes, mutation testing and similar techniques like fuzzing can help with it, but sometimes you want to be more deterministic: there are usually a lot of hidden side effects that are not obvious, and probably a source of majority of software bugs today.

Eg. something as simple as

  function foo(url) {
     data = fetch(url);
     return data;
  }
has a bunch of exceptions that can happen in fetch() not covered with your tests, yet you can get 100% line coverage with a single deterministic happy path test.

Basically, any non-functional side-effect behavior is a source of semantic "hiding" when measuring test coverage by lines being executed, and there is usually a lot of it (logging is another common source of side-effects not tested well). Some languages can handle this better with their typing approaches, but ultimately, there will be things that can behave differently depending on external circumstances (even bit flips, OOMs, full disk...) that were not planned for and do not flow from the code itself.

Post reply on HN