From nobody Fri Dec 19 19:23:32 2025 Received: from mail-wr1-f41.google.com (mail-wr1-f41.google.com [209.85.221.41]) (using TLSv1.2 with cipher ECDHE-RSA-AES128-GCM-SHA256 (128/128 bits)) (No client certificate requested) by smtp.subspace.kernel.org (Postfix) with ESMTPS id A49A0337BBA for ; Thu, 6 Nov 2025 12:53:44 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=209.85.221.41 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1762433627; cv=none; b=nrBNFhYpg7N0gj8sZyN6i/xnoZ7NGkHXBb8SN0jr1m7AN2+5suxxJVpoUKJr5/x/zYEPyKWaJNt9DU8sl61ccyyFQPtt/nD+ftaAubHamZAQ6JTFFAI8mT9qISj76MpgxM3VDA9mdTpenVMLp0y8GrV8FZjFBYdjEebMwOSyh2I= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1762433627; c=relaxed/simple; bh=VcMIYDcgbIp7gzck2lmzT1DdYedQDnPc1OGCfRsQ8Rw=; h=From:To:Cc:Subject:Date:Message-Id:In-Reply-To:References: MIME-Version; b=TtDtnNRQwOy5o3tAVpgkZyQJo0zzyRxnJ89+Xb57/kEhi4b/42OmebJyBTh5UQLdMV5jXMGeEDn5VMd2wA9kS1yFLxqr4tMG3ZPvo9jo/tpx8zo2WRPn5bEaXdAOpbmwiEb24i0x9AAsFk4E4TKSJ2J/h7YXEdA6dfPoVS+eq5E= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=gmail.com; spf=pass smtp.mailfrom=gmail.com; dkim=pass (2048-bit key) header.d=gmail.com header.i=@gmail.com header.b=Wg1bueW+; arc=none smtp.client-ip=209.85.221.41 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=gmail.com Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=gmail.com Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=gmail.com header.i=@gmail.com header.b="Wg1bueW+" Received: by mail-wr1-f41.google.com with SMTP id ffacd0b85a97d-42421b1514fso516602f8f.2 for ; Thu, 06 Nov 2025 04:53:44 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20230601; t=1762433623; x=1763038423; darn=vger.kernel.org; h=content-transfer-encoding:mime-version:references:in-reply-to :message-id:date:subject:cc:to:from:from:to:cc:subject:date :message-id:reply-to; bh=uAHXlerzYNMFVMdi3HCj0A57dbSsWmdWDXdM/zHlcgQ=; b=Wg1bueW+3QVsiD1y43hZKpA9SiKfrNpOG1yhK41STqCEKrv/lZ1/Vp9hEeze79znuh tox5FTE52Z3H3aQKgwQtr/r6WG/cqLzzu8tu4JdzP/XnBglw4uVWy3E4pQI4tWiwKiN7 2ny7j7ZT1Sg4hmag9Q2WRSFu9EPCcN6l1QQWnzBHHO4Y0RYqiM3JNP+LkurMTuKSZetH j25fKmYZIB/Sd/96xt7sFDwZ/Gen0fWfABbi9A3psimBIH/wZpuNFzSr44pHks9Kg2wk ESOLWWravQ3QhbgmhGKF0QmsbFVSA3e7zjcbxUr59K5p74Emv9lTOfecbF8WtPEfs3rE U+oQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1762433623; x=1763038423; h=content-transfer-encoding:mime-version:references:in-reply-to :message-id:date:subject:cc:to:from:x-gm-message-state:from:to:cc :subject:date:message-id:reply-to; bh=uAHXlerzYNMFVMdi3HCj0A57dbSsWmdWDXdM/zHlcgQ=; b=AtiWiCHl7d+SQmUAshCXwDM0p1wgvMnwMqcJ4MrGgqYLqyGjCuv8GbKTmW+DxUO3h7 y7lQAmvCs0kdamHuezFMUk1HclYo3lcrTzV8pegZCRkLz1tNZd9PXV3V8OavHKODNxjC Ns4AoJ2jZX32i2EHNf0gAMvCsis0Nv9635KshO0oemUTOZb/K4d4xj+sjKTON09biyHC 0nuqtFqnofwR9Jke8fajcjTvJT0kcvLr3SeVxkb1sDsAYxarblcNb/yxvpFivgno4Q1l c3UKBD87SBH8DgtZIjGNOsAw4cNX40eoIhsRmhmWrPaSOC4nZ8J7KfNzBtsVjRV1xaWE Tsjw== X-Forwarded-Encrypted: i=1; AJvYcCUDLoFtN1rq+ibuZM1624PMzjatQLjwv0dYjee1epAq15+mL/1xYKjz2FVrRpZ/iRCpBbiwt3O2snvHeRQ=@vger.kernel.org X-Gm-Message-State: AOJu0YxbdLLsRKoejtbnJNLRtoZj1JciK/jdkM9qEEGAhGFGgoY0EyGF PRrzFf0xHZR4wzD91Y8DO52JONVRdHJu429VFDce6SpfOm+v0iFcFe0= X-Gm-Gg: ASbGncupIfq9bcPlUvotMfrdnF6N71nU28bWMbn9STsm7/GPzrmS9uO4kszHmPIkOw7 vnuieV6KykZ6P16fF5+rVcUhHcQg+lXZh71j7EIY51oCMIhgWJ4bkiQHCEc1Wn4eAww8Kfxf2/t 5f2LjXpyFZxT86qOadv3LdkfzWzuFt/rBse7KFpHFGqr+fl3n30YUk7Y9+rn90LTtSndBshQem9 6H1wBS94N80+UKbRjhvIryxmcj34TQwQ6SrEEdw1mTO4d0Y0jmk6ar6WeMX8GNmKODgAMs5Kz2j mLKf798qGZb5+bi8DCEPXRX4nJeQhRRgmUg/buekmbkq3ULsFpZ4S5GQcJPIlqNzE9JnhAxLYUJ J8K4TOee7t3+TB9d/bIvGYPJEG/StVB0VxEzWBci3sWhylElgYSBB6RcFql3N2sa6qwObVaW8LG hYwq4zzm8AnVbXO76ODYEg+A40OUhmDnAAkq6xapIvjCZwnUlQWqo0SuU= X-Google-Smtp-Source: AGHT+IEpSkzz80Ete4RN99YnH1gQLlKEKMFwhAKzS6oQ8PF5tpjR7FJdfvzr60LpAUuxBGi+08V9xA== X-Received: by 2002:a5d:5f87:0:b0:429:bc93:9d8a with SMTP id ffacd0b85a97d-429e3307958mr6150736f8f.37.1762433622868; Thu, 06 Nov 2025 04:53:42 -0800 (PST) Received: from ast-epyc5.inf.ethz.ch (ast-epyc5.inf.ethz.ch. [129.132.161.180]) by smtp.gmail.com with ESMTPSA id ffacd0b85a97d-429eb40379esm4788856f8f.9.2025.11.06.04.53.42 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Thu, 06 Nov 2025 04:53:42 -0800 (PST) From: Hao Sun X-Google-Original-From: Hao Sun To: bpf@vger.kernel.org Cc: ast@kernel.org, daniel@iogearbox.net, andrii@kernel.org, eddyz87@gmail.com, john.fastabend@gmail.com, martin.lau@linux.dev, song@kernel.org, yonghong.song@linux.dev, linux-kernel@vger.kernel.org, sunhao.th@gmail.com, Hao Sun Subject: [PATCH RFC 12/17] bpf: Track path constraint Date: Thu, 6 Nov 2025 13:52:50 +0100 Message-Id: <20251106125255.1969938-13-hao.sun@inf.ethz.ch> X-Mailer: git-send-email 2.34.1 In-Reply-To: <20251106125255.1969938-1-hao.sun@inf.ethz.ch> References: <20251106125255.1969938-1-hao.sun@inf.ethz.ch> Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" Record per-branch conditions during `bcf_track()` and build a single conjunction to represent the path suffix constraint. - Add `record_path_cond()`: after processing each instruction under trackin= g, examine the previous instruction; if it is a conditional jump over scalar= s, construct a boolean condition that matches the taken/not-taken edge, and = then append the condition id to `env->bcf.br_conds`. - When tracking completes, if there are recorded conditions, build `env->bcf.path_cond` as either the single condition or a BCF_BOOL|BCF_CONJ of all collected conditions. - In `bcf_refine()`, if both `path_cond` and a refinement-specific `refine_cond` exist, combine them via a 2-ary conjunction so userspace pr= oves exactly the path-specific condition. Signed-off-by: Hao Sun --- kernel/bpf/verifier.c | 113 +++++++++++++++++++++++++++++++++++++++--- 1 file changed, 107 insertions(+), 6 deletions(-) diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c index 3f2981db1d40..f1e8e70f9f61 100644 --- a/kernel/bpf/verifier.c +++ b/kernel/bpf/verifier.c @@ -20589,6 +20589,70 @@ static int bcf_match_path(struct bpf_verifier_env = *env) return PATH_MATCH; } =20 +static int record_path_cond(struct bpf_verifier_env *env) +{ + int prev_insn_idx =3D env->prev_insn_idx; + struct bpf_reg_state *regs =3D cur_regs(env); + struct bpf_reg_state *dst, *src; + int dst_expr, src_expr; + struct bpf_insn *insn; + u8 class, op, bits; + bool jmp32, non_taken; + int cond_expr; + + if (prev_insn_idx < 0) + return 0; + + insn =3D &env->prog->insnsi[prev_insn_idx]; + class =3D BPF_CLASS(insn->code); + op =3D BPF_OP(insn->code); + if (class !=3D BPF_JMP && class !=3D BPF_JMP32) + return 0; + if (op =3D=3D BPF_CALL || op =3D=3D BPF_EXIT || op =3D=3D BPF_JA || op = =3D=3D BPF_JCOND) + return 0; + if (insn->off =3D=3D 0) + return 0; + + dst =3D regs + insn->dst_reg; + src =3D regs + insn->src_reg; + if (BPF_SRC(insn->code) =3D=3D BPF_K) { + src =3D &env->fake_reg[0]; + memset(src, 0, sizeof(*src)); + src->type =3D SCALAR_VALUE; + __mark_reg_known(src, insn->imm); + } + if (dst->type !=3D SCALAR_VALUE || src->type !=3D SCALAR_VALUE) + return 0; + + jmp32 =3D (class =3D=3D BPF_JMP32); + bits =3D jmp32 ? 32 : 64; + dst_expr =3D bcf_reg_expr(env, dst, jmp32); + src_expr =3D bcf_reg_expr(env, src, jmp32); + if (dst_expr < 0 || src_expr < 0) + return -ENOMEM; + + non_taken =3D (prev_insn_idx + 1 =3D=3D env->insn_idx); + if (op =3D=3D BPF_JSET) { + int and_expr, zero_expr; + + and_expr =3D bcf_build_expr(env, BCF_BV | BPF_AND, bits, 2, + dst_expr, src_expr); + zero_expr =3D bcf_val(env, 0, jmp32); + op =3D BPF_JNE; + if (non_taken) + op =3D BPF_JEQ; + cond_expr =3D bcf_build_expr(env, BCF_BOOL | op, 0, 2, + and_expr, zero_expr); + } else { + if (non_taken) + op =3D rev_opcode(op); + cond_expr =3D bcf_build_expr(env, BCF_BOOL | op, 0, 2, dst_expr, + src_expr); + } + + return bcf_add_cond(env, cond_expr); +} + static int do_check(struct bpf_verifier_env *env) { bool pop_log =3D !(env->log.level & BPF_LOG_LEVEL2); @@ -20656,8 +20720,9 @@ static int do_check(struct bpf_verifier_env *env) =20 if (path =3D=3D PATH_MISMATCH) goto process_bpf_exit; - else if (path =3D=3D PATH_DONE) - return 0; + err =3D record_path_cond(env); + if (err || path =3D=3D PATH_DONE) + return err; } =20 if (signal_pending(current)) @@ -24023,11 +24088,37 @@ static int bcf_track(struct bpf_verifier_env *env, if (!err && !same_callsites(env->cur_state, st)) err =3D -EFAULT; =20 - if (!err) { - tracked_regs =3D cur_regs(env); - for (i =3D 0; i < BPF_REG_FP; i++) - regs[i].bcf_expr =3D tracked_regs[i].bcf_expr; + if (err) + goto out; + + tracked_regs =3D cur_regs(env); + for (i =3D 0; i < BPF_REG_FP; i++) + regs[i].bcf_expr =3D tracked_regs[i].bcf_expr; + + /* Build the path constraint. */ + if (bcf->br_cond_cnt =3D=3D 1) { + bcf->path_cond =3D *bcf->br_conds; + } else if (bcf->br_cond_cnt > 1) { + struct bcf_expr *cond_expr; + int cond; + + cond =3D bcf_alloc_expr(env, bcf->br_cond_cnt + 1); + if (cond < 0) { + err =3D cond; + goto out; + } + cond_expr =3D bcf->exprs + cond; + cond_expr->code =3D BCF_BOOL | BCF_CONJ; + cond_expr->params =3D 0; + cond_expr->vlen =3D bcf->br_cond_cnt; + memcpy(cond_expr->args, bcf->br_conds, + sizeof(u32) * bcf->br_cond_cnt); + bcf->path_cond =3D cond; } +out: + kfree(bcf->br_conds); + bcf->br_conds =3D NULL; + bcf->br_cond_cnt =3D 0; =20 free_verifier_state(env->cur_state, true); env->cur_state =3D NULL; @@ -24134,6 +24225,7 @@ static int __used bcf_refine(struct bpf_verifier_en= v *env, refine_state_fn refine_cb, void *ctx) { struct bpf_reg_state *regs =3D st->frame[st->curframe]->regs; + struct bcf_refine_state *bcf =3D &env->bcf; struct bpf_verifier_state *base; int i, err; =20 @@ -24168,6 +24260,15 @@ static int __used bcf_refine(struct bpf_verifier_e= nv *env, if (!err && refine_cb) err =3D refine_cb(env, st, ctx); =20 + /* The final condition is the conj of path_cond and refine_cond. */ + if (!err && bcf->refine_cond >=3D 0 && bcf->path_cond >=3D 0) { + bcf->refine_cond =3D bcf_build_expr(env, BCF_BOOL | BCF_CONJ, 0, + 2, bcf->path_cond, + bcf->refine_cond); + if (bcf->refine_cond < 0) + err =3D bcf->refine_cond; + } + if (!err && (env->bcf.refine_cond >=3D 0 || env->bcf.path_cond >=3D 0)) mark_bcf_requested(env); =20 --=20 2.34.1