Live data from Hacker News

eBPF Verification Is Untenable

twitter.com

111–116 of 116 posts

Re: eBPF Verification Is Untenable

#111

Earlier quoted context omitted.

I never said that it's anywhere near a complete set. My point is that they exist as something that must be a helper because they represent a type of raw computation expected of bpf programs, but incompatible with it's verifier model. The original parent was talking about removing all helpers, > They show that various escape hatches can be eliminated or simplified. However they don't have a plan to eliminate all escap…

I don't think it's super common to do any kind of serious string manipulation in BPF. I happened to have Facebook's `dnswatch` open in my editor, and there are zero calls to strtol or printf. The idiomatic design here is to do that kind of thing in userland, piping raw stuff down a perf or ring buffer to postprocess in a "real" language runtime. So my rebuttal would be: you could just remove those few string helpers,…

It's common enough in seccomp filters; I've personally used them there. Sometimes you trap into a user space dameon via seccomp_unotify to do relatively unbounded brain surgery on the unprivileged process, but that's pretty expensive to trap out and back to a daemon and it's much better if possible to make the decision in the filter program if you can get away with it.

Edit: Perhaps you'd be happy with another example that isn't a string processing function, but follows the same core idea I'm trying to get across of compute offload from the verified program to create useful verifiable programs: bpf_l3_csum_replace. It's not too hard to hit an mtu where you'd run out of instructions just recomputing the checksum because of the complexity of per byte computation required if it were to happen in regular bpf. This helper is not exposing a specific of the network stack or kernel really (other than who else needs one's complement?), but is instead really a unit of computation not super amenable to bpf verification that's still required of the use cases expected of bpf.

Re: eBPF Verification Is Untenable

#112
post #94

Earlier quoted context omitted.

OK then! Back to C it is I guess. More seriously, we're talking about the Linux kernel here: it's written in C, and there's some momentum to write new code in Rust. You're asking for the moon, but you may have to settle for a picture of it.

Back to dTrace would be the obvious solution. Only OracleLinux has that. Seemless probes across the kernel, libs and user-facing app. No arrays. Works for decades, but linux devs thought it they could do better.

[deleted]

Re: eBPF Verification Is Untenable

#113
post #97

Hm. Doesn’t look viable to me. I’m not against language-based security, proof-carrying code, and all that, but I have less than perfect confidence that the Rust compiler currently is or will soon be sound enough to be secure against actively hostile code—AFAIU the language designers haven’t even written down their core calculus, let alone proven it sound. Putting the entirety of the Rust compiler (including, at least…

Also JVM, ART, .NET verifiers show how complexity hard is to write bytecode verifiers and that is with bytecode that was designed for verification to start with.

I’m not sure how true that is. I seem to remember that some of the problems in JVM bytecode verification are due to a wrong design and not shared by e.g. WASM, and I’m under the impression that (if you don’t try for the absolute best performance and streaming) WASM verification is fairly straightforward. Also, eBPF should probably also fall into the “designed for verification” category, so I can’t figure out what your point is here.

Re: eBPF Verification Is Untenable

#114
post #97

Earlier quoted context omitted.

Also JVM, ART, .NET verifiers show how complexity hard is to write bytecode verifiers and that is with bytecode that was designed for verification to start with.

I’m not sure how true that is. I seem to remember that some of the problems in JVM bytecode verification are due to a wrong design and not shared by e.g. WASM, and I’m under the impression that (if you don’t try for the absolute best performance and streaming) WASM verification is fairly straightforward. Also, eBPF should probably also fall into the “designed for verification” category, so I can’t figure out what you…

If it had been we wouldn't been having this discussion thread on a security paper.

Re: eBPF Verification Is Untenable

#115

Earlier quoted context omitted.

They didn't mistake rust safety for anything. This is called out by them as a shrotcoming of their approach that has to be mitigated separately.

Because my comment was "in general" not specific to any specific case I very intentionally did not refer to the paper at all.

I guess I find it weird that you posted something totally random and unrelated to the paper as a direct reply to the paper.

Re: eBPF Verification Is Untenable

#116

Earlier quoted context omitted.

You should read Ken Thompson's "Reflections on trusting trust". Outsourcing security to a tool which you have to blindly trust, and can't verify is very, very dangerous.

You've obviously misunderstood the proposal - there's nothing about this that is "blind trust" at all.

Anything based on PKI which at some unknown time in the future can be leaked or otherwise compromised is “blind trust”.

This is why perfect forward secrecy techniques have been developed.

Post reply on HN