Mitigating Linux verifier bugs using Prevail?

[luisgerhorst]

I am sure you are aware that the Linux kernel verifier has repeatedly suffered from bugs that allowed eBPF programs to break out of their sandbox. Would it be possible to mitigate those by doing a second (normally redundant) verification in userspace (e.g., using Prevail)?

Idea would be that even if the Linux verifier has a bug that allows a certain (malicious) pattern in eBPF bytecode, Prevail is very unlikely to have the same bug. Therefore the program would still be rejected by the system.

I so far looked into CVE-2017-16995 (NUS-Curiosity/KernJC#6) and Prevail (as expected) does not appear to be vulnerable.

[luisgerhorst]

Hmm, thinking about it, I might have found a very simple construction that allows you to combine two separate exploits (F1() and F2() working for the individual verifiers) into one that works even if the same program is checked by both verifiers:

r1 = F1() # trick Linux kernel into thinking F1() returns 0 while it is actually 0x1000'0000'0000'0000
r2 = F2() # trick PREVAIL into thinking F2() returns 0 while it is actually 0x1000'0000'0000'0000
r3 = r1 & r2 # both Linux kernel and PREVAIL will conclude r3 is always 0
r4 = PTR_TO_MAP_ELEM()
r4 += r3 # simulated as +=0 by both, ptr is still valid
*r4 = ...

Both (inlined) subprograms F1() and F2() are accepted by the respectively other verifier as having a large constant in a register is not forbidden.

For the Linux kernel, the program appears as:

r1 = 0 # incorrect
r2 = 0x1000'0000'0000'0000 # correct
r3 = 0 # incorrect
r4 = ptr
r4 = ptr+0
*(ptr+0) = ...

For PREVAIL, this would appear as

r1 = 0x1000'0000'0000'0000 # correct
r2 = 0 # incorrect
r3 = 0 # incorrect
r4 = ptr
r4 = ptr+0
*(ptr+0) = ...

However, when executed by the CPU the following happens:

r1 = 0x1000'0000'0000'0000
r2 = 0x1000'0000'0000'0000
r3 = 0x1000'0000'0000'0000
r4 = ptr
r4 = ptr+0x1000'0000'0000'0000
*(ptr+0x1000'0000'0000'0000) = ...

For example, F1() could be lines 29 to 34 of https://github.com/NUS-Curiosity/KernJC/blob/7c5fe8e764001268a77d8197837cf3106aac0e5b/db/pocs/cve-2017-16995/bpf-obj/poc.bpf.s#L30

For PREVAIL, it is likely not impossible that a instruction sequence that could act as F2() exists.