Verifier.md

Verifier Documentation

static int verifier_remove_insns(struct bpf_verifier_env *env, u32 off, u32 cnt)
{
	struct bpf_insn_aux_data *aux_data = env->insn_aux_data;
	unsigned int orig_prog_len = env->prog->len;
	int err;

	if (bpf_prog_is_offloaded(env->prog->aux))
		bpf_prog_offload_remove_insns(env, off, cnt);

	err = bpf_remove_insns(env->prog, off, cnt);
	if (err)
		return err;

	err = adjust_subprog_starts_after_remove(env, off, cnt);
	if (err)
		return err;

	err = bpf_adj_linfo_after_remove(env, off, cnt);
	if (err)
		return err;

	memmove(aux_data + off, aux_data + off + cnt,
		sizeof(*aux_data) * (orig_prog_len - off - cnt));

	return 0;
}

How verifier reallocate the program:

prog_adj = bpf_prog_realloc(prog, bpf_prog_size(insn_adj_cnt),
			    GFP_USER);

Bridging

Using our framework to connect with the verifier.

Verifier-aware IR?

Utilize the verifier information for the IR.

Memory access

if (cond) { write xxx }

if (another_cond) { read xxx }

Verifier cannot infer cond == another_cond ==> Error!