From: 孟祥宇 <sekiro_meng@mail.nwpu.edu.cn>
To: "Alexei Starovoitov" <alexei.starovoitov@gmail.com>
Cc: bpf@vger.kernel.org
Subject: Re: Re: [BPF Security] what security properties does verifier guarantee?
Date: Fri, 10 May 2024 13:16:48 +0800 (GMT+08:00) [thread overview]
Message-ID: <2fbf4e8f.11475.18f60eeb808.Coremail.sekiro_meng@mail.nwpu.edu.cn> (raw)
In-Reply-To: <CAADnVQKroXpteX+TvWja=BOC-hLbKgaGMt-5GJ2ZfxEQqK5Q2Q@mail.gmail.com>
Our team is currently working on enhancing the security of the eBPF subsystem, both for privileged and unprivileged BPF programs.
In our efforts to fully understand the verifier's behavior and the security guarantees it provides, we have examined the checks implemented in the verifier, especially in the context of the strictest case where all checks are performed. Our intention is to establish a solid foundation for further customization based on program type and CAP.
> >
> > 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.
>
We agree that for priv bpf use cases, many of the checks are disabled, and most of checks are for unpriv bpf, which is disabled by default. For example, prog with CAP_PERFMON can write pointers to maps, and the speculation sanitizer is removed. This article ["Reconsidering unprivileged BPF"](https://lwn.net/Articles/796328/) also discussed the checks verifier posed on unpriv bpf.
> > 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).
>
Thanks for pointing out this. We saw some helpers like `bpf_probe_read/write()` can be used to access arbitrary kernel memory, but bpf prog cannot access arbitrary kernel memory by its own load/store instructions *directly*, as they are checked by the `check_mem_access()` function in verifier. So we consider adjust 1.1 as below:
1.1 Programs can only directly 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.
>
> Not true for all 3.
>
Specifically,
2.1 For unpriv bpf, we saw in `check_mem_access()` and `check_alu_op()`, the pointers can not be leaked or calculated. And for priv bpf, these checks are canceled.
2.2 For unpriv bpf, bpf prog cannot read uninitialized stack.
2.3 bpf_bypass_spec_v1/v4() checks are performed/instrumented for unpriv bpf.
> > 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.
We acknowledge that our focus is on the strictest use case that represents a small percentage of overall scenarios. However, we believe that a comprehensive understanding of the verifier's security properties in the strictest case is crucial for our objective of enhancing the eBPF subsystem's security.
Therefore, we kindly request your assistance in reviewing our summary and providing any corrections, additions, or clarifications. Additionally, if there are any relevant resources or documentation that we may have missed, we would be grateful for your guidance in accessing them.
prev parent reply other threads:[~2024-05-10 5:16 UTC|newest]
Thread overview: 3+ messages / expand[flat|nested] mbox.gz Atom feed top
2024-05-09 14:07 [BPF Security] what security properties does verifier guarantee? 孟祥宇
2024-05-09 14:32 ` Alexei Starovoitov
2024-05-10 5:16 ` 孟祥宇 [this message]
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=2fbf4e8f.11475.18f60eeb808.Coremail.sekiro_meng@mail.nwpu.edu.cn \
--to=sekiro_meng@mail.nwpu.edu.cn \
--cc=alexei.starovoitov@gmail.com \
--cc=bpf@vger.kernel.org \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).