[bpf-next,v6,0/4] verify scalar ids mapping in regsafe()

Message

Eduard Zingerman June 13, 2023, 3:38 p.m. UTC

Update regsafe() to use check_ids() for scalar values.
Otherwise the following unsafe pattern is accepted by verifier:

  1: r9 = ... some pointer with range X ...
  2: r6 = ... unbound scalar ID=a ...
  3: r7 = ... unbound scalar ID=b ...
  4: if (r6 > r7) goto +1
  5: r6 = r7
  6: if (r6 > X) goto ...
  --- checkpoint ---
  7: r9 += r7
  8: *(u64 *)r9 = Y

This example is unsafe because not all execution paths verify r7 range.
Because of the jump at (4) the verifier would arrive at (6) in two states:
I.  r6{.id=b}, r7{.id=b} via path 1-6;
II. r6{.id=a}, r7{.id=b} via path 1-4, 6.

Currently regsafe() does not call check_ids() for scalar registers,
thus from POV of regsafe() states (I) and (II) are identical.

The change is split in two parts:
- patches #1,2: update for mark_chain_precision() to propagate
  precision marks through scalar IDs.
- patches #3,4: update for regsafe() to use a special version of
  check_ids() for precise scalar values.

Changelog:
- V5 -> V6:
  - check_ids() is modified to disallow mapping different 'old_id' to
    the same 'cur_id', check_scalar_ids() simplified (Andrii);
  - idset_push() updated to return -EFAULT instead of -1 (Andrii);
  - comments fixed in check_ids_in_regsafe() test case 
    (Maxim Mikityanskiy);
  - fixed memset warning in states_equal() reported in [4].
- V4 -> V5 (all changes are based on feedback for V4 from Andrii):
  - mark_precise_scalar_ids() error code is updated to EFAULT;
  - bpf_verifier_env::idmap_scratch field type is changed to struct
    bpf_idmap to encapsulate temporary ID generation counter;
  - regsafe() is updated to call scalar_regs_exact() only for
    env->explore_alu_limits case (this had no measurable impact on
    verification duration when tested using veristat).
- V3 -> V4:
  - check_ids() in regsafe() is replaced by check_scalar_ids(),
    as discussed with Andrii in [3],
    Note: I did not transfer Andrii's ack for patch #3 from V3 because
          of the changes to the algorithm.
  - reg_id_scratch is renamed to idset_scratch;
  - mark_precise_scalar_ids() is modified to propagate error from
    idset_push();
  - test cases adjusted according to feedback from Andrii for V3.
- V2 -> V3:
  - u32_hashset for IDs used for range transfer is removed;
  - mark_chain_precision() is updated as discussed with Andrii in [2].
- V1 -> v2:
  - 'rold->precise' and 'rold->id' checks are dropped as unsafe
    (thanks to discussion with Yonghong);
  - patches #3,4 adding tracking of ids used for range transfer in
    order to mitigate performance impact.
- RFC -> V1:
  - Function verifier.c:mark_equal_scalars_as_read() is dropped,
    as it was an incorrect fix for problem solved by commit [3].
  - check_ids() is called only for precise scalar values.
  - Test case updated to use inline assembly.

[V1]  https://lore.kernel.org/bpf/[e-mail]/
[V2]  https://lore.kernel.org/bpf/[e-mail]/
[V3]  https://lore.kernel.org/bpf/[e-mail]/
[V4]  https://lore.kernel.org/bpf/[e-mail]/
[V5]  https://lore.kernel.org/bpf/[e-mail]/
[RFC] https://lore.kernel.org/bpf/[e-mail]/
[1]   https://gist.github.com/eddyz87/a32ea7e62a27d3c201117c9a39ab4286
[2]   https://lore.kernel.org/bpf/[e-mail]/T/#mc21009dcd8574b195c1860a98014bb037f16f450
[3]   https://lore.kernel.org/bpf/[e-mail]/T/#m89da8eeb2fa8c9ca1202c5d0b6660e1f72e45e04
[4]   https://lore.kernel.org/oe-kbuild-all/[e-mail]/

Eduard Zingerman (4):
  bpf: use scalar ids in mark_chain_precision()
  selftests/bpf: check if mark_chain_precision() follows scalar ids
  bpf: verify scalar ids mapping in regsafe() using check_ids()
  selftests/bpf: verify that check_ids() is used for scalars in
    regsafe()

 include/linux/bpf_verifier.h                  |  25 +-
 kernel/bpf/verifier.c                         | 206 +++++-
 .../selftests/bpf/prog_tests/verifier.c       |   2 +
 .../selftests/bpf/progs/verifier_scalar_ids.c | 659 ++++++++++++++++++
 .../testing/selftests/bpf/verifier/precise.c  |   8 +-
 5 files changed, 867 insertions(+), 33 deletions(-)
 create mode 100644 tools/testing/selftests/bpf/progs/verifier_scalar_ids.c

Comments

[e-mail] June 13, 2023, 10:20 p.m. UTC | #1

Hello:

This series was applied to bpf/bpf-next.git (master)
by Andrii Nakryiko <[e-mail]>:

On Tue, 13 Jun 2023 18:38:20 +0300 you wrote:
> Update regsafe() to use check_ids() for scalar values.
> Otherwise the following unsafe pattern is accepted by verifier:
> 
>   1: r9 = ... some pointer with range X ...
>   2: r6 = ... unbound scalar ID=a ...
>   3: r7 = ... unbound scalar ID=b ...
>   4: if (r6 > r7) goto +1
>   5: r6 = r7
>   6: if (r6 > X) goto ...
> 
> [...]

Here is the summary with links:
  - [bpf-next,v6,1/4] bpf: use scalar ids in mark_chain_precision()
    https://git.kernel.org/bpf/bpf-next/c/904e6ddf4133
  - [bpf-next,v6,2/4] selftests/bpf: check if mark_chain_precision() follows scalar ids
    https://git.kernel.org/bpf/bpf-next/c/dec020280373
  - [bpf-next,v6,3/4] bpf: verify scalar ids mapping in regsafe() using check_ids()
    https://git.kernel.org/bpf/bpf-next/c/1ffc85d9298e
  - [bpf-next,v6,4/4] selftests/bpf: verify that check_ids() is used for scalars in regsafe()
    https://git.kernel.org/bpf/bpf-next/c/18b89265572b

You are awesome, thank you!