Verification fails for program of sample extension type.

[shankarseal]

While working on #342 I encountered an issue where verification fails on an eBPF program of the sample_extension type. To repro please checkout https://github.com/shankarseal/ebpf-for-windows/tree/utility_functions and build the solution. Then run unit_tests.exe verify_test1.
The eBPF program is tests\sample\test_sample_ebpf.c with the following section name.
#pragma clang section text = "sample_ext/1"

The source code is annotated with comments on what causes the verification to succeed and what to fail. In short, the verifier fails with the following report

Verification failed
33: r0 = sample_ebpf_extension_replace:65538(mem r1[r2], uint64_t r2)
  r3 is number

1 errors

where prototype of the helper function is:

     "sample_ebpf_extension_replace",
     EBPF_RETURN_TYPE_INTEGER,
     {EBPF_ARGUMENT_TYPE_PTR_TO_MEM,
      EBPF_ARGUMENT_TYPE_CONST_SIZE,
      EBPF_ARGUMENT_TYPE_ANYTHING,
      EBPF_ARGUMENT_TYPE_PTR_TO_MEM,
      EBPF_ARGUMENT_TYPE_CONST_SIZE}

The 3rd parameter to this function is return value from another helper function. If the local variable storing this value is either initialized to 0 or if this is the last helper function of the program then verification succeeds.

I need help to investigate this further.

[dthaler]

Code has this:

 int64_t position;

        if (values[0])
            position = sample_ebpf_extension_find(
                context->data_start, context->data_end - context->data_start, values[0], VALUE_SIZE);
        if (values[1]) {
            result = sample_ebpf_extension_replace(
                context->data_start, context->data_end - context->data_start, position, values[1], VALUE_SIZE);
            if (result < 0)
                goto Exit;
        }

Verification fails because the verifier believes that values[0] could be false while values[1] could be true, in which case the 3rd parameter is uninitialized memory.

[shankarseal]

OK makes sense. But the exact same program will verify successfully if there are no more helper functions invoked after call to _replace(...). This issue is what is more interesting to me. You can remove the calls to the 2 helper functions at the end of the program - keep position uninitialized - and the program will verify successfully. This is essentially same as the code in the previous section - which has the same "bug" - but verifier has to problem with that.

[dthaler]

It worked by chance because in the passing case (sample_ext) but not in the failing case (sample_ext/1), the compiler put a "r0 = 42" instruction after the call to bpf_map_lookup_elem, which meant it was initialized to 42 since that register was copied to the 3rd argument. In the failing case, r0 held the result of bpf_map_lookup_elem which was not an integer. So the byte code would verify even if the source code had a bug. The verified code was safe but probably didn't do what you wanted it to do.

BTW, the fact that the output only showed the first two args to sample_ebpf_extension_replace is a display bug, fixed in vbpf/ebpf-verifier#253

[shankarseal]

Understood - this was really subtle. I missed this line
22: r0 = 42
And that is why verifier was happy. But why did the compiler put this instruction before potential calls and jumps?
Does this not necessarily "break' the verfier?

I will update the test eBPF program. In a way I am glad that there was this bug in the eBPF code. :-)

[dthaler]

The verifier's job is only to prove that the code is safe, not that the code is correct.

[shankarseal]

My argument is this. Both sections had the same "defect". In one case verifier thinks it is safe and in another instance it thinks it isnt - for essentially the same source - compiler optimization notwithstanding. Is that OK?

[dthaler]

The bytecode does not have a "defect" per se. You might argue that the compiler has a defect in generating that bytecode, but the bytecode is the same as a case where the source code initialized the variable to 42.

[shankarseal]

Hmm yes - the byte code generated for 2 source sections are different. Thanks for explaining Dave.