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
A trivial example[1]:
int main() {
while (true) {}
int x = foo();
return x;
}
I feel like the halting problem is incredibly widely misunderstood to be similar to be about "ANY program" when it really talks about "ALL programs".
[1]: In C++, this is undefined behavior technically, but C and most other programming languages define the behavior of this (or equivalent) function.
[2]: Fun relevant xkcd: https://xkcd.com/1266/
Nit: In many languages, doesn't this depend on what foo() does? e.g:
foo() {
exit(0);
}but there are always sets of programs for which it is clearly possible to guarantee their termination
e.g. the program `return 1+1;` is guaranteed to halt
e.g. given program like `while condition(&mut state) { ... }` with where `condition()` is guaranteed to halt but otherwise unknown is not guaranteed to halt, but if you turn it into `for _ in 0..1000 { if !condition(&mut state) { break; } ... }` then it is guaranteed to halt after at most 1000 iterations
or in other words eBPF only accepts programs which it can proof will halt in at most maxins "instruction" (through it's more strict then my example, i.e. you would need to unroll the for-loop to make it pass validation)
the thing with programs which are provable halting is that they tend to also not be very convenient to write and/or quite limited in what you can do with them, i.e. they are not suitable as general purpose programming languages at all
"The Maneuvering Characteristics Augmentation System (MCAS) is a flight stabilizing [software] feature developed by Boeing that became notorious for its role in two fatal accidents of the 737 MAX in 2018 and 2019, which killed all 346 passengers and crew among both flights."
https://en.wikipedia.org/wiki/Maneuvering_Characteristics_Au...
"The Boeing Orbital Flight Test (OFT) was an uncrewed orbital flight test launched on December 20, 2019, but after deployment, an [incorrect] 11-hour offset in the mission clock of Starliner caused the spacecraft to compute that "it was in an orbital insertion burn", when it was not. This caused the attitude control thrusters to consume more fuel than planned, precluding a docking with the International Space Station.[79][80]"
[79] https://spacenews.com/starliner-suffers-off-nominal-orbital-... "Starliner suffers "off-nominal" orbital insertion after launch". SpaceNews. December 20, 2019. Archived from the original on June 6, 2024. Retrieved December 20, 2019.
[80] https://www.cnbc.com/2019/12/20/boeings-starliner-flies-into... Sheetz, Michael (December 20, 2019). "Boeing Starliner fails mission, can't reach space station after flying into wrong orbit". CNBC. Archived from the original on February 8, 2021. Retrieved December 20, 2019.
They wouldn't say it was "over 20,000 lines" in that case. And 20,000 lines of C is far too big to audit.
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 all, and then we are back to square one.
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.
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.
This is just such a naive view. "We can prevent programs from crashing by just taking care to stop them when they do bad things". Well, sure, that's why you have a kernel and userland. But it turns out, some things need to run in the kernel. Or "just deny permission". Then it turns out some programs need to run as admin. And so on.
There is a generality in the halting problem, and saying "we'll just kill long runing programs" just misses the point entirely.
Likely what will happen is that you will kill useful long-running programs, then an exception mechanism will be invented so some programs will not be killed, because they need to run longer, then one of those programs will go into an infinite loop despite all your mechanisms preventing it. Just like the crowdstrike driver managed to bring down the OS despite all the work that is supposed to prevent the entire computer crashing if a single program tries something stupid.
Linux and windows are completely monolithic kernels; the crowdstrike agent isn't running in a sandbox and has complete unfettered access to the entire kernel address space. There is no separate "the kernel" to detect when the agent does something wrong; once a kernel module is loaded, IT IS the kernel.
Lots of people have indeed realized this is undesirable and that there should be a sandboxed way to run kernel code such that bugs in it can't cause arbitrarily bad undefined behavior. Thus they invented eBPF. That's precisely what eBPF is.
I don't know whether it's literally true that someday you will be able to write all possibly useful kernel-mode code in eBPF. But the spirit of the claim is true: there's a huge amount of useful software that could be written in eBPF today on Linux instead of as kernel modules, and this includes crowdstrike. Thus Windows supporting eBPF, and crowdstrike choosing to use it, would have solved this problem. That set of software will increase as the eBPF verifier is enhanced to accept a wider variety of programs.
Just like you can write pretty much any useful program in JavaScript today -- a sandboxed language.
You're also correct that due to the halting problem, we'll either have to accept that eBPF will never be Turing complete, OR accept that some eBPF programs will never halt and deal with the issues in other ways. Just like Chrome's JavaScript engine has to do. I don't really view this as a fundamentally unsolvable issue with the nature of eBPF.
> 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 interesting comment at the top:
I haven't inspected the code, but I thought that checking for infinite loops would imply solving the halting problem. Where's the catch?