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. 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. 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. 3. DoS Prevention: 3.1 Programs cannot crash while executing. 3.2 Programs cannot execute for too long. 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.
