6 ms·

Why can't they build the eBPF bytecode offline using the correct kernel API and ship the bytecode to the Android device?

• derefr 7y ago
  If it’s anything like GPU shaders, it’s because the bytecode format itself is Turing-complete and not-so-sandboxed, and the actual security/fault-tolerance comes from a static analysis pass done during compilation that ensures the source code being compiled isn’t doing anything crazy. If you were able to load bytecode directly, you’d skip this verification step. (I’ve always thought VM runtimes should have signing keys, sign build artifacts—e.g. bytecode—as they create them, and then have the VM’s module loader check the signature. This way, you could still rely on build-time static verification for your security, while also being able to share compiled artifacts among any set of runtimes that trust one-another’s signing keys.)
  • a_t48 7y ago
    eBPF is not Turing complete, and from my understanding is made to be sandboxed.
  • stefan_ 7y ago
    eBPF is specifically not Turing-complete because you can not prove any property of Turing-complete language code.
    • sp332 7y ago
      eBPF is not Turing-complete, but static analysis can absolutely prove things about individual programs in Turing-complete languages.
      • colechristensen 7y ago
        You can prove some code in Turing complete languages. You can construct non-turing-complete languages which all code can be proven, and that is the point the parent is making.
        • comex 7y ago
          Forbidding loops in a language does make all code written in that language provably terminating. But there’s not much else it lets you prove for all code, at least not if you want to get results before the heat death of the universe. For example, you can’t determine what inputs to a program will yield a given output: even classic BPF is probably expressive enough to implement a cryptographic hash, and eBPF definitely is. You can’t enumerate all possible paths through the program: the number of paths is exponential in the size of the program. On the other hand, forbidding loops does make some properties easier to prove for restricted classes of programs. For instance, Linux’s BPF verifier tracks, for each instruction, the minimum and maximum value of each register at that point in the program. It uses that to determine whether array accesses in the program are bounds checked, and complain if not: that way, it doesn’t have to insert its own bounds check, which might be redundant. Doing the same in the presence of loops would require a more expensive algorithm, so forbidding them is a benefit. Yet... Linux’s verifier is sound: it will forbid all programs that could possibly index out of bounds, at least barring bugs. But it is not fully precise: it does not pass all programs that have the property of never indexing out of bounds for any input. For example, you could have a program that takes a 256-bit input and indexes out of bounds only if its SHA-256 hash is a specific value. That program is safe iff there happen to be no 256-bit strings that hash to that value, something that you could theoretically verify – but only by going through all 2^256 possible strings and hashing each of them. Linux does not. Nor would it be reasonable to, why does that hypothetical matter? Because the ability to prove arbitrary properties about all programs, at the cost of arbitrarily long analysis time, is sort of the main mathematical benefit to non-Turing-completeness. But from a practical standpoint that’s useless. And if you don’t need that – if you only care about the ability to prove things about restricted classes of programs – well, you can achieve that even with loops. After all, that’s what a type system does, and there are plenty of Turing-complete languages with type systems. As I said, disallowing loops makes the job easier in some cases. But that’s more of a matter of degree, not the kind of hard theoretical barrier that “non-Turing-complete = analyzable” makes it sound like. That makes it a less convincing rationale for disallowing them.
    • monocasa 7y ago
      The bytecode format of eBPF is Turing complete, it's the verification pass that makes sure the code flow graph is a DAG for instance. cBPF was different, and only allowed you to jump forward (guaranteeing termination), but eBPF is a much more general VM.
    • kyberias 7y ago
      Of course one can make proofs of programs written in Turing complete languages.
  • monocasa 7y ago
    I think singularity did at least a piece of what you're describing, signing the bartok compiler output after install time and post verification so that it could be saved to disk and retrieved later without the compilation and verification steps.
• lmb 7y ago
  The problem is that different kernel configurations end up changing the layout of important data structures. Basically, you need to change the offsets that the eBPF uses. There is another proposal that uses BTF to do the fixup at load (not compile) time, but that ends up having it's own complications.
• ndesaulniers 7y ago
  Lol Joel (the author) and I discussed that this week. Sounds like bpftools will need some modifications to reload a precompiled bpf program. We'd like to avoid having another copy of LLVM on device (renderscript has an old version of LLVM).