Re: BPF64: proposal of platform-independent hardware-friendly backwards-compatible eBPF alternative

Hello,

New user here, not a contributor.

> Ensuring kernel stability? Just don't allow arbitrary pointers, like original BPF.
> Guaranteed termination time? It's possible if you place some restrictions. For
> example, don't allow backward jumps but allow function calls - in case of
> stack overflow, terminate program. Really need backward jumps? Let's analyze
> for what purpose. You'll find these are needed for loops on packet contents.
> Solve it but supporting loops in "hardware"-controlled loops, which can't be
> infinite.

If I understand Turing-completeness correctly, the "no backward jumps
but allow recursion and quit on stack overflow" is exactly equivalent to
having non-infinite loops.

I'm not entirely sure, but I think the lack of backwards jumps would be
"simple" to check on LLVM IR: just make sure that a basic block does not
jump, directly or indirectly, to a basic block that dominates it. [1]

[1]: https://en.wikipedia.org/wiki/Dominator_(graph_theory)

And then the stack overflow mechanic would be an entirely runtime check,
which is safer than pure static checking.

But the good thing about this is that FreeBSD could use LLVM IR as the
BPF64 language, which means any language that compiles to LLVM is a
possible target.

As for restricting access, I think it would be possible to check the
instructions in LLVM IR for any unsafe instructions or calls to
restricted functions.

The downsides:

* Someone would need to write an LLVM analyze pass or whatever they're
  called. Maybe more than one.
* The kernel would need the ability to compile LLVM IR, making LLVM part
  of the Ring 0 domain.
	* Either that, or someone builds an LLVM-to-bytecode translator.
	* But the analysis pass(es) must still live in the kernel.
* There would need to be tutorials or some docs on how to write whatever
  language so that backwards jumps are avoided.

Please take my words with a full dose of salt; I'm not an expert on this
or on FreeBSD goals.

Gavin Howard