ebpf-verifier-repair

Name: ebpf-verifier-repair
Author: eunomia-bpf

18stars1forks

How to install ebpf-verifier-repair?

eunomia-bpf/bpfix/ebpf-verifier-repair

$npx -y skills add eunomia-bpf/bpfix --skill ebpf-verifier-repair

Installs into the current project.

Summary

End-to-end workflow for diagnosing and repairing eBPF verifier rejections in C, Rust/Aya, libbpf, libbpf-rs, BCC, bpftool, and CI logs from raw verbose verifier logs, BPFix diagnostics, or source/test failures. Use when Codex is asked to fix, explain, or patch verifier errors, ve

Files · 1

View on GitHub

SKILL.md

1	# eBPF Verifier Repair
2
3	## Overview
4
5	Repair verifier failures as missing proof obligations, not as string-matched
6	terminal errors. A full verbose verifier log plus source is sufficient evidence
7	to start; use `bpfix` only when it is available and helpful. Make the smallest
8	verifier-visible source change that preserves program semantics and proves the
9	required safety fact to the kernel verifier.
10
11	Do not split work into one skill per verifier error family. `BPFIX-E*`,
12	`failure_class`, and `next_action` values are routing signals inside this
13	workflow; the reusable user job is "repair this verifier rejection."
14
15	## Resource Routing
16
17	- Read `references/log-collection.md` when the user did not provide a full
18	verbose verifier log, the log is incomplete, or the framework/loader command
19	is unclear.
20	- Read `references/raw-log-triage.md` whenever repairing from a raw verifier
21	log. Use its rejected-instruction and proof-lifecycle procedure before
22	selecting a source rewrite.
23	- Read `references/diagnostic-routing.md` only when a BPFix diagnostic is
24	provided or generated. Do not block raw-log repair on this file.
25	- Read `references/repair-patterns.md` before editing source, selecting a
26	verifier-visible rewrite, or reviewing a proposed patch.
27	- Read `references/semantic-preservation.md` before editing a nontrivial
28	program, especially when it updates maps, emits events, has fallback policy,
29	or uses multiple acquired resources.
30	- Read `references/failure-directed-retry.md` after any candidate fails to
31	compile, load, or pass the semantic oracle. Route the next edit by the failure
32	stage instead of starting a new speculative repair.
33	- Run `scripts/run-bpfix-diagnostic.sh` only when BPFix is available and a
34	repeatable plain-text diagnostic artifact would make the repair loop clearer.
35	- Run `scripts/extract_verifier_failure.py verifier.log` when a raw log is too
36	large for the working context. Keep the original log and inspect omitted PCs
37	when the initial slice does not reveal proof origin or loss.
38
39	## Repair Workflow
40
41	1. Establish the failing load path.
42	Identify the loader command, framework, BPF source file, compiled object if
43	available, kernel/program type, and the exact command that produced the
44	rejection. Preserve the full verbose verifier/build/load log; the final
45	`Permission denied` or `invalid argument` line is not enough.
46
47	2. Choose the evidence path.
48	If only source and a raw verbose verifier log are available, work directly
49	from them. Find the rejected instruction, terminal verifier message,
50	register state, helper call, source annotation, and the earlier branch or
51	check that should have established the missing proof. Do not wait for BPFix.
52
53	If BPFix is available and the user did not ask for a raw-log-only repair, it
54	can add proof-aware plain-text evidence:
55
56	```bash
57	bpfix verifier.log
58	bpfix --fail-on-unsupported verifier.log > bpfix-diagnostic.txt
59	bpfix --object prog.o verifier.log
60	```
61
62	If this skill is checked out with the BPFix repo, the helper script can
63	produce a repeatable plain-text artifact:
64
65	```bash
66	skills/ebpf-verifier-repair/scripts/run-bpfix-diagnostic.sh --out .bpfix-agent verifier.log
67	skills/ebpf-verifier-repair/scripts/run-bpfix-diagnostic.sh --object prog.o verifier.log
68	```
69
70	3. Route by proof evidence, not by prose alone.
71	Inspect the diagnostic class, safety/confidence labels, next action,
72	required proof, source spans, and verifier evidence when a diagnostic
73	exists. With raw logs, infer the same facts manually from the
74	rejected PC, register classes/ranges, helper arguments, and source lines. If
75	the log is incomplete, fix log collection first. If the evidence points to
76	environment/configuration failure, confirm kernel/program-type/helper/BTF
77	availability before editing source.
78
79	4. Freeze the semantic contract.
80	List the observable behavior that the repair must preserve: program section
81	and return actions, packet or context fields consumed, map keys and values,
82	state mutations, event contents, helper calls, resource lifecycle, fallback
83	behavior, and meaningful branch outcomes. Read the project's tests and
84	loader when available. Distinguish a safety guard from a policy decision;
85	do not turn a missing proof into a new policy.
86
87	5. Form a proof-obligation hypothesis.
88	State the fact the verif

People who liked this also viewed

6 picks

Type

ebpf-verifier-repair

18stars1forks

View on GitHub

How to install ebpf-verifier-repair?

eunomia-bpf/bpfix/ebpf-verifier-repair

$npx -y skills add eunomia-bpf/bpfix --skill ebpf-verifier-repair

Installs into the current project.

Summary

Files · 1

View on GitHub

SKILL.md

1	# eBPF Verifier Repair
2
3	## Overview
4
5	Repair verifier failures as missing proof obligations, not as string-matched
6	terminal errors. A full verbose verifier log plus source is sufficient evidence
7	to start; use `bpfix` only when it is available and helpful. Make the smallest
8	verifier-visible source change that preserves program semantics and proves the
9	required safety fact to the kernel verifier.
10
11	Do not split work into one skill per verifier error family. `BPFIX-E*`,
12	`failure_class`, and `next_action` values are routing signals inside this
13	workflow; the reusable user job is "repair this verifier rejection."
14
15	## Resource Routing
16
17	- Read `references/log-collection.md` when the user did not provide a full
18	verbose verifier log, the log is incomplete, or the framework/loader command
19	is unclear.
20	- Read `references/raw-log-triage.md` whenever repairing from a raw verifier
21	log. Use its rejected-instruction and proof-lifecycle procedure before
22	selecting a source rewrite.
23	- Read `references/diagnostic-routing.md` only when a BPFix diagnostic is
24	provided or generated. Do not block raw-log repair on this file.
25	- Read `references/repair-patterns.md` before editing source, selecting a
26	verifier-visible rewrite, or reviewing a proposed patch.
27	- Read `references/semantic-preservation.md` before editing a nontrivial
28	program, especially when it updates maps, emits events, has fallback policy,
29	or uses multiple acquired resources.
30	- Read `references/failure-directed-retry.md` after any candidate fails to
31	compile, load, or pass the semantic oracle. Route the next edit by the failure
32	stage instead of starting a new speculative repair.
33	- Run `scripts/run-bpfix-diagnostic.sh` only when BPFix is available and a
34	repeatable plain-text diagnostic artifact would make the repair loop clearer.
35	- Run `scripts/extract_verifier_failure.py verifier.log` when a raw log is too
36	large for the working context. Keep the original log and inspect omitted PCs
37	when the initial slice does not reveal proof origin or loss.
38
39	## Repair Workflow
40
41	1. Establish the failing load path.
42	Identify the loader command, framework, BPF source file, compiled object if
43	available, kernel/program type, and the exact command that produced the
44	rejection. Preserve the full verbose verifier/build/load log; the final
45	`Permission denied` or `invalid argument` line is not enough.
46
47	2. Choose the evidence path.
48	If only source and a raw verbose verifier log are available, work directly
49	from them. Find the rejected instruction, terminal verifier message,
50	register state, helper call, source annotation, and the earlier branch or
51	check that should have established the missing proof. Do not wait for BPFix.
52
53	If BPFix is available and the user did not ask for a raw-log-only repair, it
54	can add proof-aware plain-text evidence:
55
56	```bash
57	bpfix verifier.log
58	bpfix --fail-on-unsupported verifier.log > bpfix-diagnostic.txt
59	bpfix --object prog.o verifier.log
60	```
61
62	If this skill is checked out with the BPFix repo, the helper script can
63	produce a repeatable plain-text artifact:
64
65	```bash
66	skills/ebpf-verifier-repair/scripts/run-bpfix-diagnostic.sh --out .bpfix-agent verifier.log
67	skills/ebpf-verifier-repair/scripts/run-bpfix-diagnostic.sh --object prog.o verifier.log
68	```
69
70	3. Route by proof evidence, not by prose alone.
71	Inspect the diagnostic class, safety/confidence labels, next action,
72	required proof, source spans, and verifier evidence when a diagnostic
73	exists. With raw logs, infer the same facts manually from the
74	rejected PC, register classes/ranges, helper arguments, and source lines. If
75	the log is incomplete, fix log collection first. If the evidence points to
76	environment/configuration failure, confirm kernel/program-type/helper/BTF
77	availability before editing source.
78
79	4. Freeze the semantic contract.
80	List the observable behavior that the repair must preserve: program section
81	and return actions, packet or context fields consumed, map keys and values,
82	state mutations, event contents, helper calls, resource lifecycle, fallback
83	behavior, and meaningful branch outcomes. Read the project's tests and
84	loader when available. Distinguish a safety guard from a policy decision;
85	do not turn a missing proof into a new policy.
86
87	5. Form a proof-obligation hypothesis.
88	State the fact the verif

People who liked this also viewed

6 picks

Type