The ebpf-for-windows maintainers have been working with the PREVAIL verifier maintainers for some time now on improving the implementation for everyone, since we agree that addressing such limitations is critical. For example, the PREVAIL maintainers added program termination verification back in January 2021. Check it out at https://github.com/vbpf/ebpf-verifier

This is all super exciting. A weird aside: one thing that'd be really nice to have is a userland verifier that we could build into our CI system; testing verifiability involves a lot of really contrived steps in our current process.

the PREVAIL implementation seems to be more robust then Linux's verifier, are there any plans to port it to Linux?

From the counter examples directory, this implementation seems very promising.

Re: termination, can't you use Ethereum gas style termination? I always found termination verification strange, because "gas" is usually more practical alternative.

The ZFS file system supports running Lua programs in Kernel mode. It supports setting a limit on the number of instructions run and the amount of memory used:

https://www.delphix.com/blog/delphix-engineering/zfs-channel...

So it’s been done before. I think traditional BPF programs were really short and ran in performance critical contexts. Disallowing backwards branches and limiting size was preferred to slowing down these code paths with instruction counting.

How would you maintain the gas cout? Per instruction or per basic block?

>Additionally, the PREVAIL paper explicitly doesn't verify program termination, which is kind of a dealbreaker for kernel BPF.

I'd be more alarmed if someone had solved the Halting Problem and I hadn't heard about it, to be honest.

Microsoft did termination proof for Windows drivers in 2006. Termination proof does not require solving halting problem.

Termination proofs for systems code (PLDI 2006): https://dl.acm.org/doi/10.1145/1133255.1134029

As mentioned in a sibling reply, there goes my week. Thanks for the reference! Time to learn something I apparently did not know!

I think you can reason it like this.

Assuming certain constraints (what you can define bounded analysis rules for) you can prove that things terminate. These rules things are usually far more advanced than we suspect initially, but they're not still not fully unbounded.(And we can often come up with more rules to make things practical even if unwieldy)

Deciding termination for an arbitrarily large program in a turing complete system CAN require no less than execution of such a program thus we CANNOT guarantee to be able to verify termination for EVERY program. (This is the halting problem)

I spent a lot of time on my thesis learning about type inference systems and as many such systems for uncooperative languages(JS,Python,etc) need to do abstract interpretation they fall into the same kind of issues and this is why practical systems use JIT compilation instead of AOT even if there are exceptions (Shed Skin Python is quite impressive for example).

I thought any general system contain arithmetic (as the proof based on transformation) cannot be proved it will be halted. Termination ... can it be terminated without halting?

Halting is indeed the same as termination. The halting problem DOES allow you to prove that some programs terminate. The problem is that there will be other programs that do terminate, but you won't be able to prove that they terminate.

So there is no way to know, for EVERY possible program, whether that program will terminate or not. But there are still some programs that you can know for certain that those programs will terminate.

From my understanding eBPF is sufficiently constrained to where the halting problem is solvable for all representable programs (in eBPF).

BPF verifiers don't accept arbitrary programs.

Awww shit.

I knew this day would come. Be back in like a week. Gotta get my neurons warmed up and translating Theoretic CompSci/discrete math notation again.

If I don't come back send a search party. I'll probably be stuck somewhere around pumping lemmas screaming "This is arbitrary bullshit!"

It’s not magic, just constraints. there are some obvious tricks (which have since been relaxed).

No unbounded loops for one. I think no backward jumps was previously a rule? I think the ability to tail call another bpf program was added, so not sure if you can accidentally loop forever between individually terminating programs.

You can't; each program is verified independently, and there's a small limit to the number of tail calls you can do.

Being able to run an unbounded loop in eBPF would be a big deal (doesn't mean it can't be done; in fact: it almost surely can be) --- a serious vulnerability.