Re: eBPF verifier thoughts (Re: [PATCH v15 net-next 00/11] eBPF syscall, verifier, testsuite)

On Fri, Sep 26, 2014 at 1:09 PM, Alexei Starovoitov [off-list ref] wrote:

On Fri, Sep 26, 2014 at 12:51 PM, Andy Lutomirski [off-list ref] wrote:

quoted

On Fri, Sep 26, 2014 at 12:34 PM, Andy Lutomirski [off-list ref] wrote:

To add one more point:

With the current verifier design, it's impossible to write a userspace
tool that can take an eBPF program and check it.  The verification is
far too context-dependent for that to be possible.  I won't go so far
as to say that a userspace tool needs to *exist*, but I strongly
object to exposing a verification algorithm that *precludes* writing
such a tool.

that's just not true.
why is it not possible?

Because the types of referenced objects aren't encoded in the blob
that a user program loads, unless I'm missing something.

quoted

I think that the eBPF program format needs to encode all context
needed for verification.  Then verification should check that the
program is compliant with the context and that the context is correct.
The former could, in principle, be done in userspace, too.

one can have maps and other future objects equally
represented in user space. Nothing stops doing exactly the same
logic there.

But the eBPF binary doesn't encode this information. In fact, the
caller of an ebpf syscall may not even have access to this
information.

I really think that the information needed to check type safety should
be encapsulated in the program.

quoted

Here, "context" includes the program type (i.e. what type R1 hasis),
the key and value sizes of all referenced maps, the fact that the maps
are maps (damnit, "every object implements exactly the same interface
and is called a 'map'" is a bad type system*), and possible also
things like the intended stack size and any other relevant details
about the entry calling convention.

Andy, I'm not sure where you're going with this.
Sounds like you want to redesign the whole thing?
How long it will take?
Did you consider all the cases I did?
I think I understand your concerns. What I don't understand
why you think we cannot address them step by step.
imo what this does covers a ton of use cases.
Some futuristic stuff may be better and may be not.
But here I have it working, tested and proven over many
use cases, whereas some future unclear stuff will take
unknown amount of time to redesign...

I think this is addressable as a smallish change on top of your code.
Rather than looking up a map when you need to learn its key and value
size, I think that all you need to do is to look in a program section
for the key and value size (and the fact that it's a map) and confirm
that the referenced map *matches* the stored values.

--Andy

-- 
Andy Lutomirski
AMA Capital Management, LLC