eBPF byte code and x64 machine code equivalence

[Alan-Jowett]

Prevail folks,

Assuming I have a block of eBPF byte code and a block of x64 machine code, both generated from the same LLVM IR, would it be reasonable to assume safety properties proven using prevail on the eBPF byte code would still hold for the same x64 machine code?

Specifically, given:

clang -emit-llvm -g -target bpf -O2 -Werror -c foo.c -o foo.bc 
llc --mtriple=bpf -filetype=obj foo.bc -o foo_ebpf.o
llc --mtriple x86_64-pc-linux-gnu -filetype=obj foo.bc -o foo_x64.o 

Is is reasonable to assume that safety properties that are proven for foo_ebpf.o apply equally to foo_x64.o?

[elazarg]

There is no such guarantee - even if you assume correct compilation to both EBPF and x86, which the eBPF system does not.

[elazarg]

To take an easy example, if the LLVM code has undefined behavior (e.g. illegal memory access) the compiler is allowed to emit anything. Including safe eBPF code and unsafe x86 code.

[Alan-Jowett]

Thanks, appreciate the feedback. Two follow up questions:

1. Is this specifically related to undefined behavior in the LLVM code?
2. If the LLVM code was generated from the verified eBPF byte code would this still appy?

[elazarg]

1. It is not specific to UB. The LLVM code defines a set of valid traces L; it is compiled to eBPF which in turn defines another set of traces E; the compilation is valid if the E is subset of L. The eBPF bytecode E is verified to not include erroneous traces. This says nothing about the difference L-E. The x86 code defines a set of traces X. Valid compilation means X is a subset of L, too. But you need a guarantee that the intersection between X and L-E is empty (or contains only safe traces). PREVAIL cannot provide such guarantee; one can imagine an LLVM compiler that does - essentially your suggestion in 2.
   This is all abstract. I apologize but it's not easy for me to come up with a concrete example.
   Note that the issue of UB is a specific case of this - UB means that any trace is valid.
2. Given the above explanation, you are supposed to have the safety guarantees intact in this case. However, it may be tricky to guarantee that the compilation to LLVM is indeed valid, since the abstract machines considered in eBPF, LLVM and x86 are all different. Maybe that's an easy exercise for compiler designers.

[elazarg]

Maybe if the original LLVM program is somehow guaranteed to be deterministic on any input, then safety of the eBPF code would also imply safety of the original LLVM code - for some definition of safety. This would require, in particular, absence of UB in the LLVM code.

[elazarg]

Note that eBPF is specifically designed to be easily compiled directly to x86/ARM machine code. If it is compiled to LLVM first, then its design is very far from ideal, from verification perspective.

[Alan-Jowett]

Thanks, I appreciate the feedback. Was hoping we could leverage LLVM's code generation, but it sounds like this is would be problematic.

[elazarg]

Maybe a partial-evaluation framework can be used. Something like Truffle/GRAAL.

[iopta]

Hello @elazarg, jumping in here. I want to go back to Alan-Jowett's 2nd question above. The question was, if I understood it correctly, whether in a flow of [verified eBPF bytecode] -> [LLVM IR] -> [x86 machine code] the safety properties demonstrated for the eBPF bytecode could be safely assumed applicable to the x86 output. I believe you answered this should hold in your opinion, so long as the conversion to LLVM IR was done properly.

My follow-up question is if this is true in both directions. If the flow were [x86 machine code] -> [LLVM IR] -> [verified eBPF bytecode], in your opinion, could the safety properties demonstrated for the eBPF bytecode be safely assumed applicable to the x86 input?

[elazarg]

The answer is no, for essentially the same reason as in the first answer. Safety of a source code implies the safety of the compiled code (assuming valid compilation), but safety of a compiled code does not imply the safety of the source code.

The important thing is that code is not 100% deterministic, meaning it often admits more than one possible execution for any given input. As in my disclaimer above, if the code is deterministic (and in particular can never have UB), then compilation only dress it with a different syntax, and any semantic property of the compiled code also holds for the source code (and vice versa).

But to the best of my knowledge, x86 code may be nondeterministic, and in particular it may have undefined behavior. Let's say it has no input, and only two possible behaviors: GOOD and BAD. It is valid to translate it to the eBPF program "exit" whose only behavior is GOOD, so it is safe. But the original x86 code is unsafe.

[elazarg]

It is also unrealistic, I think. Safe x86 code may translate to unverifiable, though safe, eBPF code.

[Alan-Jowett]

Thank you for the feedback, @elazarg.

I am currently examining the feasibility of generating C code from the eBPF byte code, with each eBPF instruction translating into the code that the interpreter would have run for that instruction (essentially unwind the loop of the interpreter). I think this should be preserve the safety properties of the eBPF program (as much as an interpreter would have).

microsoft/ebpf-for-windows#757

Sample generated C looks like this:
https://github.com/microsoft/ebpf-for-windows/files/8044534/droppacket.c.txt