False negative with BPF_JNE

[harishankarv]

Mailing list thread shows an example of a BPF_JNE range tracking bug. The bug seems to be triggered when reg_combine_min_max() is invoked with input register states containing ranges that are non-overlapping. E.g. if these are the input register states:

dst_reg.var_off_value == 0xfffffff8
dst_reg.var_off_mask ==  0xffffffff00000007
dst_reg.smin_value ==    -9223372032559808520
dst_reg.smax_value ==    9223372036854775807
dst_reg.umin_value ==    4294967288
dst_reg.umax_value ==    18446744073709551615
dst_reg.s32_min_value == -5
dst_reg.s32_max_value == -1
dst_reg.u32_min_value == -5
dst_reg.u32_max_value == -1

src_reg.var_off_value == 0x0
src_reg.var_off_mask ==  0xff
src_reg.smin_value ==    0
src_reg.smax_value ==    255
src_reg.umin_value ==    0
src_reg.umax_value ==    255
src_reg.s32_min_value == 0
src_reg.s32_max_value == 255
src_reg.u32_min_value == 0
src_reg.u32_max_value == 255

Where, dst: [4294967288, 18446744073709551615], and src: [0, 255]

This bug seems to have existed in the kernel for a while, and should have been caught by Agni. Thanks @pchaigno for bringing this to our notice.

[harishankarv]

The SMT encoding for BPF_JNE looks to be correct. Given the inputs from above, the SMT encoding produces the same output that the verifier's C code produces. The bug is not in the LLVM to SMT translation. It is likely in the verification condition generation.

[pchaigno]

For context, here is the example program that triggers the bug:

        call %[bpf_get_prandom_u32];
        r8 = r0;
        r6 = r0;
        r6 &= 0x00f;
        r8 &= 0xf00;
        r8 |= 0x0ff;
        if r8 != r6 goto +1;
        w0 >>= w8;       /* shift-out-bounds here */

r6 has range [0; 15], r8 has range [255, 4095]. After the conditional jump, due to the bug, both registers get an incorrect range [255; 15] for the false branch (i.e., r6 == r8).

This doesn't actually look like a bypass of the verifier. It only happens for the false branch and only if the two registers had non-overlapping ranges. If they have non-overlapping ranges, they can't be equal and at runtime the false branch will therefore never be visited.

---

Could you help me understand what this bit of code does?

https://github.com/bpfverif/ebpf-range-analysis-verification-cav23/blob/bd1d363742b99b131ddb2e7e7a9f835807a1db8c/bpf-verification/lib_reg_bounds_tracking/lib_reg_bounds_tracking.py#L810-L814

My rough understanding is that it conditions the assignment of each branch's registers on the equality of the concrete values. Couldn't that explain why Agni doesn't notice this bug? The bug triggers only in a case where the two concrete values are unequal (since non-overlapping ranges can be inferred) but the verifier still runs through the branch where they are considered equal.

[pchaigno]

FYI, this bug also affects BPF_JEQ and the 32-bit variants AFAIU.

[mshachnai]

@pchaigno Your understanding of that code segment is correct, based on the concrete value comparison, it will set the registers to either take on the values from the true branch execution or the values from the false branch execution. Just to make sure I understand- since the ranges of the two registers are non-overlapping, the concrete values will never be equal in at runtime so the true branch will always be taken. Yet the bug happens in the false branch? AGNI can't find a satisfying assignment such that the false branch will be taken which is why it doesn't find this bug (at this point at least).

So the bottom line is this: because AGNI is intertwining concrete values with the abstract values in its assignment of the jump condition, it doesn't detect this possible violation of the abstract domains because the concrete values can never be satisfied. So I think your observation about why this is failing, @pchaigno, is spot on.

[pchaigno]

Your understanding of that code segment is correct, based on the concrete value comparison, it will set the registers to either have the true branch mappings (other_branch dst/src) or the false branch mapping (dst_reg/src_reg).

Thanks for confirming!

Just to make sure I understand- since the ranges of the two registers are non-overlapping, the concrete values will never be equal in at runtime so the true branch will always be taken. Yet the bug happens in the false branch? AGNI can't find a satisfying assignment such that the false branch will be taken which is why it doesn't find this bug (at this point at least).

Yes, that's my understanding.

So the bottom line is this: because AGNI is intertwining concrete values with the abstract values in its assignment of the jump condition, it doesn't detect this possible violation of the abstract domains

If we wanted to detect such bugs, any idea how we could and what the cost would be? I guess we could change the code I linked above to instead explore both the false and true branches. Would that be some sort of OR statement instead of the IF? If so, I guess it would increase runtime a lot, no?

Note this bug "only" triggered an unspecified behavior in the verifier (the shift out-of-bounds). Maybe that unspecific behavior can be turned into a verifier bypass somehow, but it isn't really a direct verifier bypass. So maybe it's okay (though unideal) to consider it out of scope for Agni.

[harishankarv]

Note this bug "only" triggered an unspecified behavior in the verifier (the shift out-of-bounds).

I do not follow. This is the log that I got (after instruction 16), from the verifier.

16: (5d) if r8 != r6 goto pc+4
R0_w=inv(id=1,umax_value=4294967295,var_off=(0x0; 0xffffffff)) 
R1=ctx(id=0,off=0,imm=0) 
R2_w=inv(id=0,umax_value=3,var_off=(0x0; 0x3)) 
R3_w=inv(id=0,umin_value=8,umax_value=13,var_off=(0x8; 0x5)) 
R4_w=inv(id=3,umax_value=4294967295,var_off=(0x0; 0xffffffff)) 
R5_w=inv(id=0) 
R6_w=inv(id=0,umin_value=4294967288,umax_value=255,var_off=(0xfffffff8; 0x7),s32_min_value=-8,s32_max_value=-1) 
R7_w=inv(id=0) 
R8_w=inv(id=0,umin_value=4294967288,umax_value=255,var_off=0xfffffff8;0x7),s32_min_value=-5,s32_max_value=-1,u32_min_value=-5) 
R10=fp0

In the false-branch evaluation that the verifier does, it concludes that for R8, umin_value > umax_value. There's no shift happening that triggers this unsoundness. What am I missing?

[pchaigno]

That unsoundness triggers a normal shift in the verifier logic (tnum_rshift) to be out-of-bounds. So it's not the out-of-bounds shift that causes the unsoundness, but the other way around. I'm guessing it could cause other issues; the verifier code tends to assume than umin_value <= umax_value is an invariant. But the out-of-bounds shift is how the unsoundness was initially uncovered (cf. first email).

I don't know if the same unsoundness could cause an actual verifier bypass.

[mshachnai]

If we wanted to detect such bugs, any idea how we could and what the cost would be? I guess we could change the code I linked above to instead explore both the false and true branches. Would that be some sort of OR statement instead of the IF? If so, I guess it would increase runtime a lot, no?

In terms of Agni, this kind of problem shouldn't exist - Agni views this as a false positive and prunes it. We could have Agni explore branches regardless of the concrete execution, but this would raise possible false positives, and also significant runtime costs (exponential I believe).

I'm still unclear on how this bug takes place. The shift happens after the false branch is taken where the register values are out of bounds due to the JNE. But the false branch can never be taken in an actual execution supposedly, so how is it happening here? We're missing some assumption that the verifier makes and if we can understand it, we'll be able to update Agni accordingly.

[pchaigno]

We're still unclear on how this bug takes place. The shift happens after the false branch is taken where the register values are out of bounds due to the JNE. But the false branch can never be taken in an actual execution supposedly, so how is it happening here?

This bug is not happening at runtime when a BPF program is executed. It is happening during verification, in the verifier itself, when the program is loaded. The verifier walks the false branch (because it doesn't realize it can never be taken) and ends up in this buggy state. The verifier is walking a branch that is actually dead code.

[harishankarv]

Thank you for the clarification Paul, that makes sense.

[harishankarv]

In the interest of closing this issue, here are some more details.

The following is the verification condition used by Agni (Equation 3 in the paper), instantiated for the BPF_JNE instruction. Here, g_JNE captures the verifier's algorithm for modifying abstract values (u32, s32, s64, u64 and tnum). The verifier's algorithm takes as input two abstract values, and produces four abstract values: two for the true branch, and two for the false branch. During program execution, input registers x and y to the BPF_JNE instruction can either be equal (x = y ) or unequal (x ≠ y). Our verification condition takes into account these possible scenarios in the actual execution of an eBPF program, and sets the output abstract value accordingly.

The member precondition to the formula ensures that when ranges P and Q are chosen such that they do not overlap, it will always be the case that x ≠ y. Consequently, our verification condition for BPF_JNE never "follows" the false branch (sets the output abstract values to P_o^f and Q_o^f) when input ranges P and Q don't overlap.

The verifier incorrectly follows the false branch, and updates the ranges using code that was only meant to be used when the ranges P and Q overlap (reg_combine_min_max), causing the bug.

The following is the definition of member. It should be straightforward for ranges (u32, s64, etc.), but for tnums please refer to the tnums paper.

[harishankarv]

Within Agni, we are able to modify our verification condition to capture such bugs in the verifier straightforwardly. With a few simple modifications, we can essentially force our verification condition to follow both branches.

As @pchaigno suggested, output values abstract values are selected using an exclusive-or clause, without placing any restrictions on them (such as their values being implicated by values in registers x and y). Finally, we check if the output abstract values are all wellformed. We check for well-formedness of the abstract domains, which weaker than membership, to avoid trivial counterexamples outputted by the SMT, where the solver ends up choosing one of the branches and checking for membership in the other branch.

[harishankarv]

Using the modified verification condition from the above comment, Agni outputs the following example. The first two set of register states are the inputs P and Q to g_JNE in our formula. The next four set of register states are the outputs P_o^f, Q_o^f P_o^t Q_o^t. Agni was able to find that it is possible that umin > umax in Q_o^f (look for the section # output register state (src): false branch )

This is similar to the bug mentioned in the mailing list.

# input register state (dst)
dst_reg_st_input.var_off.value = 4015384735087317537;
dst_reg_st_input.var_off.mask = 0;
dst_reg_st_input.smin_value = -3064565657428870622;
dst_reg_st_input.smax_value = 7029685143153439236;
dst_reg_st_input.umin_value = 2733919515743612561;
dst_reg_st_input.umax_value = 7777596866761841292;
dst_reg_st_input.s32_min_value = 15451396;
dst_reg_st_input.s32_max_value = 1935286801;
dst_reg_st_input.u32_min_value = 1091305492;
dst_reg_st_input.u32_max_value = 2005664980;

# input register state (src)
src_reg_st_input.var_off.value = 1689968972;
src_reg_st_input.var_off.mask = 268440576;
src_reg_st_input.smin_value = 187221551;
src_reg_st_input.smax_value = 3494786320;
src_reg_st_input.umin_value = 1689968972;
src_reg_st_input.umax_value = 3494786324;
src_reg_st_input.s32_min_value = 1084229128;
src_reg_st_input.s32_max_value = 1881424412;
src_reg_st_input.u32_min_value = 65676;
src_reg_st_input.u32_max_value = 1694517157;

# output register state (dst): false branch
dst_reg_output.var_off.value = 4015384735087317537;
dst_reg_output.var_off.mask = 0;
dst_reg_output.smin_value = -3064565657428870622;
dst_reg_output.smax_value = 7029685143153439236;
dst_reg_output.umin_value = 2733919515743612561;
dst_reg_output.umax_value = 7777596866761841292;
dst_reg_output.s32_min_value = 15451396;
dst_reg_output.s32_max_value = 1935286801;
dst_reg_output.u32_min_value = 1091305492;
dst_reg_output.u32_max_value = 2005664980;

output register state (src): false branch
src_reg_st_output.var_off.value = 4015384735109538124;
src_reg_st_output.var_off.mask = 268440576;
src_reg_st_output.smin_value = 4015384735109538124;
src_reg_st_output.smax_value = 4015384735087317537;
src_reg_st_output.umin_value = 4015384735109538124;
src_reg_st_output.umax_value = 4015384735087317537;
src_reg_st_output.s32_min_value = 1689968972;
src_reg_st_output.s32_max_value = 1958409548;
src_reg_st_output.u32_min_value = 1689968972;
src_reg_st_output.u32_max_value = 1958409548;

output register state (dst): true branch
other_branch_dst_reg_output.var_off.value = 4015384735087317537;
other_branch_dst_reg_output.var_off.mask = 0;
other_branch_dst_reg_output.smin_value = -3064565657428870622;
other_branch_dst_reg_output.smax_value = 7029685143153439236;
other_branch_dst_reg_output.umin_value = 2733919515743612561;
other_branch_dst_reg_output.umax_value = 7777596866761841292;
other_branch_dst_reg_output.s32_min_value = 15451396;
other_branch_dst_reg_output.s32_max_value = 1935286801;
other_branch_dst_reg_output.u32_min_value = 1091305492;
other_branch_dst_reg_output.u32_max_value = 2005664980;

output register state (src): true branch
other_branch_src_reg_output.var_off.value = 1689968972;
other_branch_src_reg_output.var_off.mask = 268440576;
other_branch_src_reg_output.smin_value = 1689968972;
other_branch_src_reg_output.smax_value = 1958409548;
other_branch_src_reg_output.umin_value = 1689968972;
other_branch_src_reg_output.umax_value = 1958409548;
other_branch_src_reg_output.s32_min_value = 1689968972;
other_branch_src_reg_output.s32_max_value = 1958409548;
other_branch_src_reg_output.u32_min_value = 1689968972;
other_branch_src_reg_output.u32_max_value = 1958409548;

[pchaigno]

Within Agni, we are able to modify our verification condition to capture such bugs in the verifier straightforwardly. With a few simple modifications, we can essentially force our verification condition to follow both branches.

@harishankarv Would you have that patch somewhere? Given such weakened condition is useful in speculative execution context, I'm thinking of supporting it behind a flag.

[harishankarv]

@pchaigno we quickly hacked a solution locally for the weakened verification condition, so we don't have a patch for that yet. We can support it behind a flag. @mshachnai said will take a look at this!