BPF List
 help / color / mirror / Atom feed
From: Eduard Zingerman <eddyz87@gmail.com>
To: bpf@vger.kernel.org, ast@kernel.org
Cc: andrii@kernel.org, daniel@iogearbox.net, martin.lau@linux.dev,
	kernel-team@fb.com, yonghong.song@linux.dev, memxor@gmail.com,
	awerner32@gmail.com, john.fastabend@gmail.com,
	Eduard Zingerman <eddyz87@gmail.com>
Subject: [PATCH bpf-next v2 0/7] exact states comparison for iterator convergence checks
Date: Sun, 22 Oct 2023 04:08:05 +0300	[thread overview]
Message-ID: <20231022010812.9201-1-eddyz87@gmail.com> (raw)

Iterator convergence logic in is_state_visited() uses state_equals()
for states with branches counter > 0 to check if iterator based loop
converges. This is not fully correct because state_equals() relies on
presence of read and precision marks on registers. These marks are not
guaranteed to be finalized while state has branches.
Commit message for patch #3 describes a program that exhibits such
behavior.

This patch-set aims to fix iterator convergence logic by adding notion
of exact states comparison. Exact comparison does not rely on presence
of read or precision marks and thus is more strict.
As explained in commit message for patch #3 exact comparisons require
addition of speculative register bounds widening. The end result for
BPF verifier users could be summarized as follows:

(!) After this update verifier would reject programs that conjure an
    imprecise value on the first loop iteration and use it as precise
    on the second (for iterator based loops).

I urge people to at least skim over the commit message for patch #3.

Patches are organized as follows:
- patches #1,2: moving/extracting utility functions;
- patch #3: introduces exact mode for states comparison and adds
  widening heuristic;
- patch #4: adds test-cases that demonstrate why the series is
  necessary;
- patch #5: extends patch #3 with a notion of state loop entries,
  these entries have to be tracked to correctly identify that
  different verifier states belong to the same states loop;
- patch #6: adds a test-case that demonstrates a program
  which requires loop entry tracking for correct verification;
- patch #7: just adds a few debug prints.

The following actions are planned as a followup for this patch-set:
- implementation has to be adapted for callbacks handling logic as a
  part of a fix for [1];
- it is necessary to explore ways to improve widening heuristic to
  handle iters_task_vma test w/o need to insert barrier_var() calls;
- explored states eviction logic on cache miss has to be extended
  to either:
  - allow eviction of checkpoint states -or-
  - be sped up in case if there are many active checkpoints associated
    with the same instruction.

The patch-set is a followup for mailing list discussion [1].

Changelog:
V1 -> V2 [2], applied changes suggested by Alexei offlist:
- __explored_state() function removed;
- same_callsites() function is now used in clean_live_states();
- patches #1,2 are added as preparatory code movement;
- in process_iter_next_call() a safeguard is added to verify that
  cur_st->parent exists and has expected insn index / call sites.

[1] https://lore.kernel.org/bpf/97a90da09404c65c8e810cf83c94ac703705dc0e.camel@gmail.com/
[2] https://lore.kernel.org/bpf/20231021005939.1041-1-eddyz87@gmail.com/

Eduard Zingerman (7):
  bpf: move explored_state() closer to the beginning of verifier.c
  bpf: extract same_callsites() as utility function
  bpf: exact states comparison for iterator convergence checks
  selftests/bpf: tests with delayed read/precision makrs in loop body
  bpf: correct loop detection for iterators convergence
  selftests/bpf: test if state loops are detected in a tricky case
  bpf: print full verifier states on infinite loop detection

 include/linux/bpf_verifier.h                  |  16 +
 kernel/bpf/verifier.c                         | 469 +++++++++++--
 tools/testing/selftests/bpf/progs/iters.c     | 620 ++++++++++++++++++
 .../selftests/bpf/progs/iters_task_vma.c      |   1 +
 4 files changed, 1053 insertions(+), 53 deletions(-)

-- 
2.42.0


             reply	other threads:[~2023-10-22  1:08 UTC|newest]

Thread overview: 18+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2023-10-22  1:08 Eduard Zingerman [this message]
2023-10-22  1:08 ` [PATCH bpf-next v2 1/7] bpf: move explored_state() closer to the beginning of verifier.c Eduard Zingerman
2023-10-22  1:08 ` [PATCH bpf-next v2 2/7] bpf: extract same_callsites() as utility function Eduard Zingerman
2023-10-22  1:08 ` [PATCH bpf-next v2 3/7] bpf: exact states comparison for iterator convergence checks Eduard Zingerman
2023-10-22  4:16   ` Andrii Nakryiko
2023-10-23 13:38     ` Eduard Zingerman
2023-10-22  1:08 ` [PATCH bpf-next v2 4/7] selftests/bpf: tests with delayed read/precision makrs in loop body Eduard Zingerman
2023-10-22  3:00   ` kernel test robot
2023-10-22  1:08 ` [PATCH bpf-next v2 5/7] bpf: correct loop detection for iterators convergence Eduard Zingerman
2023-10-22  4:28   ` Andrii Nakryiko
2023-10-23 14:47     ` Eduard Zingerman
2023-10-23 16:16       ` Andrii Nakryiko
2023-10-22  1:08 ` [PATCH bpf-next v2 6/7] selftests/bpf: test if state loops are detected in a tricky case Eduard Zingerman
2023-10-22  3:11   ` kernel test robot
2023-10-22  1:08 ` [PATCH bpf-next v2 7/7] bpf: print full verifier states on infinite loop detection Eduard Zingerman
2023-10-22  4:28   ` Andrii Nakryiko
2023-10-23 17:17 ` [PATCH bpf-next v2 0/7] exact states comparison for iterator convergence checks Eduard Zingerman
2023-10-23 21:40   ` Eduard Zingerman

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=20231022010812.9201-1-eddyz87@gmail.com \
    --to=eddyz87@gmail.com \
    --cc=andrii@kernel.org \
    --cc=ast@kernel.org \
    --cc=awerner32@gmail.com \
    --cc=bpf@vger.kernel.org \
    --cc=daniel@iogearbox.net \
    --cc=john.fastabend@gmail.com \
    --cc=kernel-team@fb.com \
    --cc=martin.lau@linux.dev \
    --cc=memxor@gmail.com \
    --cc=yonghong.song@linux.dev \
    /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