Halting problem

Posted Dec 4, 2018 16:18 UTC (Tue) by farnz (subscriber, #17727)
In reply to: Halting problem by nix
Parent article: Bounded loops in BPF programs

This actually sounds like a potential application for proof-carrying code. The user-space verifier could attach a simple-to-verify proof to the program it's about to attach (even if it's an arbitrary program with loops and other such weirdnesses) that the kernel can check.

Halting problem

Posted Dec 4, 2018 23:49 UTC (Tue) by nix (subscriber, #2304) [Link] (2 responses)

It really does. Heck the original Necula and Lee paper might as well have had 'BPF' written all over it in letters of fire ten miles high :)

Halting problem

Posted Dec 5, 2018 10:16 UTC (Wed) by farnz (subscriber, #17727) [Link] (1 responses)

It would be rather surprising if a researcher at Berkeley working on Packet Filters was completely unaware of BPF :-)

Halting problem

Posted Dec 11, 2018 17:45 UTC (Tue) by nix (subscriber, #2304) [Link]

Oh yeah, that's true. I had forgotten their affiliation. :)