The kernel space BPF JIT in particular, is an huge attack vector and has been repeatably exploited (or facilitated other exploits) in the past. If you don't need BPF JIT, I recommend disabling it. Sure, tcpdump or nftable may be slower, but often it doesn't matter, unless it's a cutting edge production system which actually relies on BPF JIT. It can either be removed completely when building the kernel, setting "net.core.bpf_jit_enable" in sysctl to disable it globally, or setting "kernel.unprivileged_bpf_disabled" to disable it for unprivileged programs.
# Turn off unprivileged eBPF access.
kernel.unprivileged_bpf_disabled = 1
# Turn on BPF JIT hardening, if the JIT is enabled.
net.core.bpf_jit_harden = 2
...can be abused to execute arbitrary code in Kernel mode
to complete what has been cut off in the title.
Ironically tough, running user code in the kernel was kind of the original idea.
A "direct" correctness proof of a BPF compiler written in C would be hard because C is hard to reason about. If you pulled it off, you could do this verification before compiling the kernel.
It would certainly be easier to implement an "indirect" approach using translation validation, i.e., taking the code generated by the compiler and checking that it is semantically equivalent to the input BPF code. The problem with this is that this would need to be done at run time, i.e., you would add a lot of verification time when the user is already waiting for the BPF program to run.
Overall: Yes, this is a good candidate, and people are on it.
To quote the relevant bit:
"The patch produced by git format-patch is in UNIX mailbox format, with a fixed "magic" time stamp to indicate that the file is output from format-patch rather than a real mailbox".
The date "Mon Sep 17 00:00:00 2001" is that magic date.