On Sun, Sep 24, 2023 at 6:02 PM Eduard Zingerman <eddyz87@xxxxxxxxx> wrote: > > On Fri, 2023-09-22 at 13:52 -0700, Andrii Nakryiko wrote: > > > > I can't say I understand what exactly you are proposing and how you > > > > are going to determine these conservative precision marks. But I'd > > > > like to learn some new ideas, so please elaborate :) > > > > > > I'll send a follow-up email, trying to figure out what to do with pointers. > > > > Ok, sounds good. > > (below explains why DFA was a bad idea, please proceed to the next > section if that's not interesting). ok, that's what I'm doing :) > > My initial thought was that it would be possible to use a simple > live-variable DFA in order to compute conservative read and precise > marks. Like a textbook version: > - split code in basic blocks; > - for each instruction propagate liveness information backwards: > - define USE(insn) to be a set of registers / stack slots read by > this instruction; > - define KILL(insn) to be a set of registers / stack slots written > to by this instruction. > - compute set of live variables before insn as: > LIVE_in(insn) = USE(insn) U (LIVE_out(insn) / KILL(insn)) > - compute basic block BB_out as a union of BB_in of each successor; > - etc... iterate in postorder until fixed point is reached. > > However, this is a moot point because of presence of pointers. > For series of instructions like: > "r1 = r10; r1 += -8; r1 = *(u64 *)(r1 + 0);" > Such algorithm would need to know possible range of values for r1. > Meaning that before executing liveness DFA some sort of value range > analysis would have to be run. > And these things might get complicated [1] > (I never implemented one, maybe it's not that bad). > So, basically that would be a mini-copy of the verifier but > implemented as a thing that computes fixed point instead of "tracing". > Probably a no-go. > > [1] https://boxbase.org/entries/2017/oct/23/range_analysis_papers/ > > --- > > However, I think there are two more relatively simple options that > should give correct results. > > Option A. "Exit or Loop" > ------------------------ > > - Similar to Andrii's suggestion postpone exploration of > bpf_iter_*_next() #N->#N+1 states for as long as there are other > states to explore. > - When evaluating is_state_visited() for bpf_iter_*_next() #N->#N+1 > allow to use visited state with .branches > 0 to prune current > state if: > - states_equal() for visited and current states returns true; > - all verfication paths starting from current instruction index with > current iterator ref_obj_id either run to safe exit or run back to > current instruction index with current iterator ref_obj_id. > > The last rule is needed to: > - Ensure presence of read and precision marks in a state used for pruning. > - Give a meaning to the precise scalars comparisons in regsafe() which > I think is currently missing for bpf_iter_*_next() .branches > 0 case. > Precise scalars comparison for visited states with .branches == 0 > could be read as: "using any value from a specific range it is > possible to reach safe exit". > Precise scalars comparison for looping states from above > could be read as: "using any value from a specific range it is > possible to reach either safe exit or get back to this instruction". > > This algorithm should be able to handle simple iteration patterns like: > > bpf_iter_*_new(&it1, ...) > while (!bpf_iter_*_next(&it1)) { ... } > bpf_iter_*_destroy(&it1) > > And also handle nested iteration: > > bpf_iter_*_new(&it1, ...) > while (!bpf_iter_*_next(&it1)) { > bpf_iter_*_new(&it2, ...) > while (!bpf_iter_*_next(&it2)) { ... } > bpf_iter_*_destroy(&it2) > } > bpf_iter_*_destroy(&it1) > > But it would fail to handle more complex patterns, e.g. interleaved > iteration: > > for (;;) { > if (!bpf_iter_*_next(&it1)) // a > break; > if (!bpf_iter_*_next(&it2)) // b > break; > ... > } > > For any state originating in (a) there would always be a state in (b) > pending verification and vice versa. It would actually bail out even > if it1 == it2. not working for this intermixed iterator case would be ok, I think most practical use cases would be a properly nested loops. But, compiler can actually do something like even for a proper loop. E.g., something like below for (; bpf_iter_num_next(&it); ) { .... } in assembly could be layed out as bpf_iter_num_next(&it); ... again: r0 = bpf_iter_num_next(&it) ... if (r0) goto again Or something along those lines. So these assumptions that the iterator's next() call is happening at the same instruction is problematic. > > Option B. "Widening" > -------------------- > > The trivial fix for current .branches > 0 states comparison is to > force "exact" states comparisons for is_iter_next_insn() case: > 1. Ignore liveness marks, as those are not finalized yet; > 2. Ignore precision marks, as those are not finalized yet; > 3. Use regs_exact() for scalars comparison. > > This, however, is very restrictive as it fails to verify trivial > programs like (iters_looping/simplest_loop): > > sum = 0; > bpf_iter_num_new(&it, 0, 10); > while (!(r0 = bpf_iter_num_next())) > sum += *(u32 *)r0; > bpf_iter_num_destroy(&it); > > Here ever increasing bounds for "sum" prevent regs_exact() from ever > returning true. > > One way to lift this limitation is to borrow something like the > "widening" trick from the abstract interpretation papers mentioned > earlier: > - suppose there is current state C and a visited is_iter_next_insn() > state V with .branches > 0; > - suppose states_equal(V, C) returns true but exact states comparison > returns false because there are scalar values not marked as precise > that differ between V and C. > - copy C as C' and mark these scalars as __mark_reg_unbounded() in C'; > - run verification for C': > - if verification succeeds -- problem solved; > - if verification fails -- discard C' and proceed from C. > > Such algorithm should succeed for programs that don't use widened > values in "precise" context. > > Looking at testcases failing with trivial fix I think that such > limitations would be similar to those already present (e.g. the big > comment in progs/iters.c:iter_obfuscate_counter would still apply). > This makes sense. I was originally thinking along those lines (and rejected it for myself), but in a more eager (and thus restrictive) way: for any scalar register where old and new register states are equivalent thanks to read mark or precision bit (or rather lack of precision bit), force that precision/mark in old state. But that is too pessimistic for cases where we truly needed to simulate N+1 due to state differences, while keeping the old state intact. What you propose with temporary C -> C' seems to be along similar lines, but will give "a second chance" if something doesn't work out: we'll go on N+1 instead of just failing. But let's think about this case. Let's say in V R1 is set to 7, but imprecise. In C we have R1 as 14, also imprecise. According to your algorithm, we'll create C1 with R1 set to <any num>. Now I have two questions: 1. How do we terminate C' validation? What happens when we get back to the next() call again and do states_equal() between V and C'? We just assume it's correct because C' has R1 as unbounded? 2. Assuming yes. What if later on, V's R1 is actually forced to be precise, so only if V's R1=P7, then it is safe. But we already concluded that C' is safe based on R1 being unbounded, right? Isn't that a violation? > --- > > Option B appears to be simpler to implement so I'm proceeding with it. > Will share progress on Monday. Please let me know if there are any > obvious flaws with what I shared above. > > Thanks, > Eduard
