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

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

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

quoted

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

quoted

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.

patch #8 'handle pseudo BPF_LD_IMM64 insn' of this set
handles first type == map. Other types will be added in the future.
The same verification can be done in user space.
It's pretty much copy paste for everything from the kernel.
I don't understand yet why you really must do it in in userspace
in addition to doing it in kernel. It's definitely doable.
Instead of asking kernel to create a map, user space
can just remember map attributes (key_size, value_size)
and continues verification in userspace.

quoted

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 don't follow. What info are you talking about?
are you saying that program only that references maps via fds
is not verifiable unless one knows what this fds refer to?
yeah, but we're talking user space verification here.
user knows what maps it creates with what attributes.
Also we can add a command to this syscall to fetch map
attributes. That would be trivial _incremental_ addition, right?

That would also work, I suppose.

quoted

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.

we can add extra info to the program that will encode
program assumptions about maps. Sure. Though I think
it's extra info that kernel doesn't really need, since it can
only check that program assumptions match to what
kernel already knows. Kernel cannot rely on them.
So I'm not sure what this extra check really buys.

Anyway, if you think it's a smallish change, we can do it
incrementally on top of existing stuff, right?
Why this arguing then?
Sounds like you want to help with the development?
This is great! I'm all for it :)

-- 
Andy Lutomirski
AMA Capital Management, LLC