Add verifier passes #41
Conversation
|
I'm not familiar with how the test framework works (I don't have the necessary python expertise to make it work locally), but I'd like to try enabling the verifier passes for all tests that are supposed to be valid programs. If this is desired, could someone help me determine the right invocation to set this up? |
|
I figured out how to run the tests locally; I'll try to get them all running and passing with the verifier enabled. |
|
I'm also going to add a pass to ensure all accessed registers are initialized before use, which should be a suitable alternative to #37. |
jpsamaroo
force-pushed
the
jps/verifier
branch
from
2e34572
to
eed1861
Compare
|
One slight caveat with the uninitialized registers pass: the pass doesn't confirm that a used register is initialized for a given instruction for all of the branches leading to the instruction. I'd be happy to fix this later, but I think for now the current implementation should at least catch the most common cases. |
| } | ||
| if (visited[next_pc] == 0) { | ||
| cmd = ubpf_walk_paths(vm, walk_fn, data, next_pc, visited); | ||
| if (cmd == UBPF_WALK_STOP || cmd == UBPF_WALK_INVALID) |
There was a problem hiding this comment.
I'd prefer an iterative algorithm, or at least, a tail recursive algorithm.
There was a problem hiding this comment.
Agreed, this recursive approach also makes me slightly uncomfortable 😄
vm/ubpf_verifier.c
Outdated
| _walker_no_loops(struct ubpf_vm *vm, struct ebpf_inst inst, void *data, int inst_off, char *visited) | ||
| { | ||
| if (isjmp(inst) && (inst_off+1+inst.offset < inst_off) && visited[inst_off+1+inst.offset]) { | ||
| fprintf(stderr, "Loop detected at offset %d\n", inst_off); |
There was a problem hiding this comment.
I don't think that's correct. Consider the following graph:
When you follow the edge from 5 to 1, you may have already visited 1, but that doesn't mean there's a cycle. And in general, I don't think there's a relation between the position of the code and the presence of back-edges; the compiler can reorganize code blocks at will.
We should also have a couple test cases for this, with handwritten bytecode.
There was a problem hiding this comment.
Good catch! To fix this, I suspect that it would probably be best to construct a CFG so that we can reason about blocks which branch to a predecessor block, right? So then, to determine if we have a loop, we check if we can get back to our current block by following each edge exiting our block. Does this sound reasonable, and if so, should I start constructing a CFG?
There was a problem hiding this comment.
Maybe it would be beneficial to describe the algorithm here before diving into its implementation? What did you have in mind?
Last time I had to implement an algorithm to find loops (for Oko, Apache2 license), I only needed to annotate the vertices and edges IIRC. It seems DPDK has a different approach which we may also use (BSD license AFAICT).
There was a problem hiding this comment.
I was thinking that for each block, if you walk along each path leaving the block, for any path you take, you'll either end up at a program terminator (exit), or back at the same block. But how to do that efficiently (instead of doing a full walk for every block), we should probably copy from somewhere else.
Since it seems like you have a full copy of ubpf in oko, how would you feel about me copying the relevant loop verifier bits from oko? It would be great if you didn't need to maintain two copies of ubpf then 😄
| if 'asm' not in data and 'raw' not in data: | ||
| raise SkipTest("no asm or raw section in datafile") | ||
| if 'result' not in data and 'verifier error' not in data: | ||
| raise SkipTest("no result or verifier error section in datafile") |
There was a problem hiding this comment.
Shouldn't we also run on test cases that don't result in verifier errors, to check for false positives?
| return true; | ||
| } | ||
| } else { | ||
| return false; |
There was a problem hiding this comment.
I would prefer to list explicitly all the return false cases, and default to return true. We're less likely to have false negatives that way.
| (cls == EBPF_CLS_JMP)) { | ||
| return false; | ||
| } | ||
| return true; |
jpsamaroo
force-pushed
the
jps/verifier
branch
from
ec7bdab
to
c877969
Compare
Add dead instruction-detection pass Add loop-detection pass Add instruction walker utility
|
Closing out stale PRs. Please re-open the PR if it's still being worked on. |
Add dead instruction-detection pass
Add loop-detection pass
Add instruction walker utility