On Thu, May 9, 2024 at 7:09 AM 孟祥宇 <sekiro_meng@xxxxxxxxxxxxxxxx> wrote: > > Since eBPF verifier often changes, is there a conclusion that list all the security properties verifier guarantees? With the conclusion, developers won’t make the same mistakes due to missing some security property checks. safety != security. The verifier is focusing on safety for 99% of the use cases. The security static and run-time checks are for unpriv bpf only, which was disabled years ago and strongly not advised to be enabled, since CPUs are still full of speculation bugs. > Since we didn’t find any public document to describe the security principles of the verifier, we have read most of the checks in it, especially for the full-path analysis (`do_check()`) and related function, and we summarized the security properties (for the strictest case) as follows: > > 1. Memory Safety: > 1.1 Programs can only access BPF memory and specific kernel objects such as context. No. Certain progs can read arbitrary kernel memory (depending on type and CAPs). > 2. Information Leakage Prevention: > 2.1 Programs cannot write pointers into maps, and calculation among pointers is not allowed. > 2.2 Programs cannot read uninitialized memory. > 2.3 Programs cannot speculatively access areas outside the BPF program’s memory. Not true for all 3. > 3. DoS Prevention: > 3.1 Programs cannot crash while executing. > 3.2 Programs cannot execute for too long. yes. that's the goal. > Is my summary right and comprehensive? I hope we can negotiate a manual to conclude the security properties, so that developers can have a reference. No. Since security != safety and sounds like you're after 0.01% use case.
