3 ms·
I think the main issue is that eBPF cannot have loops. It restricts the programs you can write. Wasm does not have that property, so you cannot prove that it wi
by nynx 6y ago
I think the main issue is that eBPF cannot have loops. It restricts the programs you can write. Wasm does not have that property, so you cannot prove that it will complete.
- rkeene2 6y agoTo be clear, eBPF programs can have loops -- they're just jumps that have negative offsets (which are signed 16-bit numbers), but for security reasons many verifiers do not allow them so they can ensure that the program halts.
- smasher164 6y agoI'd like to see more proof-carrying code techniques extended to WASM. Some of the work could be handed off to the compiler, embedding the proof in the binary. This could make expensive proofs, like termination checking, more tractable.
- rubatuga 6y agoare you aware of the halting problem?
- smasher164 6y agouh..yeah. The halting problem doesn’t mean you can’t do termination checking. It just means there’s no general algorithm for deciding if a machine halts. We only care about the specific subset of programs that the compiler is able to prove properties about. https://en.m.wikipedia.org/wiki/Termination_analysis https://en.m.wikipedia.org/wiki/Termination_analysis