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

No More Blue Fridays

brendangregg.com

Post reply on HN
Print view View original

61–70 of 282 posts

Re: No More Blue Fridays

#61

Post by chc4 »

aksdlf wrote: post #35
shrx wrote: post #18

From the article: > If the verifier finds any unsafe code, the program is rejected and not executed. The verifier is rigorous -- the Linux implementation has over 20,000 lines of code [0] -- with contributions from industry (e.g., Meta, Isovalent, Google) and academia (e.g., Rutgers University, University of Washington). [0] links to https://github.com/torvalds/linux/blob/master/kernel/bpf/ver... which has this inter…

I'm glad to hear that Meta and Google code is "rigorous". I'd prefer INRIA, universities that fund theorem provers, industries where correctness matters like aerospace or semiconductors.

Windows doesn't use the Linux eBPF verifier, they have their own implementation named PREVAIL[0] that is based on an abstract interpretation model that has formal small step semantics. The actual implementation isn't formally proven, however.

0: https://github.com/vbpf/ebpf-verifier

Re: No More Blue Fridays

#63

Post by lucianbr »

School-Cotton wrote: post #53
lucianbr wrote: post #45

Earlier quoted context omitted.

So this "solves" the halting problem by creating a new class "might-not-halt-but-not-sure" and lumping it with "does-not-halt". I find it hard to believe the new class is small enough for this to be useful, in the sense that it will avoid all kernel crashes. I rather expect useful or needed code would be rejected due to "not-sure-it-halts", and then people will use some kind of exception or not use the verifier at al…

Well it is useful in practice, there are some pretty useful products based on eBPF on Linux, most notably Cilium (and, shameless plug for the one I’m working on: Parca, an eBPF-based CPU profiler).

Bad wording on my part, and I still don't know how to word it better. I'm sure this thing is useful, I don't think everyone who contributed code was just clueless.

However, the claim "in the future, computers will not crash due to bad software updates, even those updates that involve kernel code" must be false. There is no way it is true. Whatever Cilium is, I cannot believe it generally prevents kernel crashes.

Re: No More Blue Fridays

#64

Post by School-Cotton »

Smaug123 wrote: post #34
kayo_20211030 wrote: post #15

This isn't right. If I need a system to run with a piece of code, then it shouldn't run at all if that piece of code is broken. Ignoring the failure is perverse. Let's say that the driver code ensures that some medical machine has safety locks (safeguards) in place to make sure that piece of equipment won't fry you to a crisp; I'd prefer that the whole thing not run at all rather than blithely operate with the safegu…

I think the premise is false? It's up to the eBPF implementor what to do in the case of invalid input; the kernel could choose to perform a controlled shutdown in that case. (I have no idea what e.g. Linux actually does here, but one could imagine worlds where the action it takes on invalid input is configurable.) Also your statement is sometimes not true, although I certainly sympathise in the mainline case. In some…

> I have no idea what e.g. Linux actually does here

If you attempt to load an eBPF program that the verifier rejects, the syscall to load it fails with EINVAL or E2BIG. What your user-space program then does is up to you, of course.

Re: No More Blue Fridays

#65

Post by lordnacho »

gtsop wrote: post #56
lordnacho wrote: post #11

Earlier quoted context omitted.

They could have helped their luck by doing some of the common sense things suggested in the article. For instance, why not find a subset of your customers that are low risk, push it out to them, and see what happens? Or perhaps have your own fleet of example installations to run things on first. None of which depends on any specific technology.

Why even do that? We have virtualization, they could emulate real clients and networks of clients. This particular bug would have been prevented for sure

Yeah I thought maybe the VM thing might not catch the bug for some reason, but it seems like the natural thing to do. Spin up VM, see if there's a crash. I heard the technical reason had something to do with a file being full of nulls, but that sort of thing you should catch.

Honestly, the most generous excuse I can think of is that CS were informed of some sort of vulnerability that would have profound consequences immediately, and that necessitated a YOLO push. But even that doesn't seem too likely.

Re: No More Blue Fridays

#66

Post by CodeWriter23 »

> an unprecedented example of the inherent dangers of kernel programming

I take issue with that. Kernel programming was not to blame; looking up addresses from a file and accessing those memory locations without any validation is. The same technique would yield the same result at any Ring.

Re: No More Blue Fridays

#67

Post by lolinder »

shrx wrote: post #18

From the article: > If the verifier finds any unsafe code, the program is rejected and not executed. The verifier is rigorous -- the Linux implementation has over 20,000 lines of code [0] -- with contributions from industry (e.g., Meta, Isovalent, Google) and academia (e.g., Rutgers University, University of Washington). [0] links to https://github.com/torvalds/linux/blob/master/kernel/bpf/ver... which has this inter…

I'm not able to comment on what this code is doing, but as for the theory:

The halting problem is only unsolvable in the general case. You cannot prove that any arbitrary piece of code will stop, but you can prove that specific types of code will stop and reject anything that you're unable to prove. The trivial case is "no jumps"—if your code executes strictly linearly and is itself finite then you know it will terminate. More advanced cases can also be proven, like a loop over a very specific bound, as long as you can place constraints on how the code can be structured.

As an example, take a look at Dafny, which places a lot of restrictions on loops [0], only allowing the subset that it can effectively analyze.

[0] https://ece.uwaterloo.ca/~agurfink/stqam/rise4fun-Dafny/#h25

Re: No More Blue Fridays

#68

Post by School-Cotton »

lucianbr wrote: post #63
School-Cotton wrote: post #53

Earlier quoted context omitted.

Well it is useful in practice, there are some pretty useful products based on eBPF on Linux, most notably Cilium (and, shameless plug for the one I’m working on: Parca, an eBPF-based CPU profiler).

Bad wording on my part, and I still don't know how to word it better. I'm sure this thing is useful, I don't think everyone who contributed code was just clueless. However, the claim "in the future, computers will not crash due to bad software updates, even those updates that involve kernel code" must be false. There is no way it is true. Whatever Cilium is, I cannot believe it generally prevents kernel crashes.

Correct, you will never be able to write any possible arbitrary code and have it run in eBPF. It necessarily constrains the class of programs you can write. But the constrained set is still quite useful and probably includes the crowdstrike agent.

Also, although this isn't the case now, it's possible to imagine that the verifier could be relaxed to allow a Turing-complete subset of C that supports infinite loops while still rejecting sources of UB/crashes like dereferencing an invalid pointer. I suspect from reading this post that that is the future Mr. Gregg has in mind.

> Whatever Cilium is, I cannot believe it generally prevents kernel crashes.

It doesn't magically prevent all kernel crashes from unrelated code. But what we can say is that Cilium itself can't crash the kernel unless there are bugs in the eBPF verifier.

Re: No More Blue Fridays

#69

Post by lucianbr »

CodeWriter23 wrote: post #66

> an unprecedented example of the inherent dangers of kernel programming I take issue with that. Kernel programming was not to blame; looking up addresses from a file and accessing those memory locations without any validation is. The same technique would yield the same result at any Ring.

Obviously in userspace it would only crash the running program and not the entire operating system? It's a significant difference.

All of the service interruptions would have been just "computer temporarily not protected by crowdstrike agent". Not the same thing at all.

Re: No More Blue Fridays

#70

Post by tptacek »

lucianbr wrote: post #45
skywhopper wrote: post #24

Earlier quoted context omitted.

If the verifier can't determine that the loop will halt, the program is disallowed. Also, if the program gets passed and then runs too long anyway, it's force-halted. So... I guess that solves the halting problem.

So this "solves" the halting problem by creating a new class "might-not-halt-but-not-sure" and lumping it with "does-not-halt". I find it hard to believe the new class is small enough for this to be useful, in the sense that it will avoid all kernel crashes. I rather expect useful or needed code would be rejected due to "not-sure-it-halts", and then people will use some kind of exception or not use the verifier at al…

Lots of useful code is rejected due to "not-sure-it-halts". That's the premise.
Post reply on HN