Should verification be done in the kernel?
Should verification be done in the kernel?
Posted Aug 5, 2019 17:16 UTC (Mon) by ecree (guest, #95790)In reply to: Should verification be done in the kernel? by anadav
Parent article: Bounded loops in BPF for the 5.3 kernel
The eBPF developers are aware of this work, and we looked into whether any of it could be of use. The following analysis is my own, but I believe the other devs broadly agree with it.
There are some problems which are non-trivial, at least, with trying to extend PREVAIL to cover the full feature set of the existing verifier, including:
* the zone domain can only support relational difference constraints _or_ relational integer congruence constraints (Miné 2004 §5.4.6), not both at once (the paper just states this is 'straightforward' without further explanation) which is needed for alignment checking.
* similarly, the paper doesn't actually explain how abstract interpretation can check loop termination; once you've got a fixed-point state set, how do you determine that the program doesn't go round in circles within that set? Just stating that it's possible doesn't guide implementors much.
* the verifier today has checks more complicated than simple 'safety of execution', for instance it can detect certain speculative-execution vulnerabilities (don't ask me how this works). It's not clear that an abstract semantics can be written that deals with this.
* sure your runtime complexity is good, but that memory usage!
Our conclusion was that the best use we could make of PREVAIL was to incorporate some of its detail ideas, while rejecting the overall architecture. In particular, I was intrigued by the concept (§7.3) of having userspace supply (essentially) a safety proof which the kernel merely validates; the equivalent of this in the existing verifier's architecture would be to specify explored_states at pruning points which are both sufficient to prove safety downstream and provable from the upstream code (which currently are discovered by the verifier and often overly precise, leading to path explosion); this would be particularly useful in the form of loop invariants as the kernel verifier would only need to prove (a) holds at loop entry, (b) maintained by loop and (c) sufficient to prove safety from loop exit. I haven't had the time to dig into this myself (and expect to be far too busy in the near future).
There are some problems which are non-trivial, at least, with trying to extend PREVAIL to cover the full feature set of the existing verifier, including:
* the zone domain can only support relational difference constraints _or_ relational integer congruence constraints (Miné 2004 §5.4.6), not both at once (the paper just states this is 'straightforward' without further explanation) which is needed for alignment checking.
* similarly, the paper doesn't actually explain how abstract interpretation can check loop termination; once you've got a fixed-point state set, how do you determine that the program doesn't go round in circles within that set? Just stating that it's possible doesn't guide implementors much.
* the verifier today has checks more complicated than simple 'safety of execution', for instance it can detect certain speculative-execution vulnerabilities (don't ask me how this works). It's not clear that an abstract semantics can be written that deals with this.
* sure your runtime complexity is good, but that memory usage!
Our conclusion was that the best use we could make of PREVAIL was to incorporate some of its detail ideas, while rejecting the overall architecture. In particular, I was intrigued by the concept (§7.3) of having userspace supply (essentially) a safety proof which the kernel merely validates; the equivalent of this in the existing verifier's architecture would be to specify explored_states at pruning points which are both sufficient to prove safety downstream and provable from the upstream code (which currently are discovered by the verifier and often overly precise, leading to path explosion); this would be particularly useful in the form of loop invariants as the kernel verifier would only need to prove (a) holds at loop entry, (b) maintained by loop and (c) sufficient to prove safety from loop exit. I haven't had the time to dig into this myself (and expect to be far too busy in the near future).