verify-prevail

診斷來自PREVAIL驗證器的eBPF程式驗證失敗。使用此技能處理在獨立PREVAIL中驗證的Linux相容eBPF程式…

npx skills add https://github.com/microsoft/ebpf-for-windows --skill verify-prevail

Diagnose PREVAIL Verification Failures (Linux-Compatible Programs)

Diagnose eBPF program verification failures using the standalone PREVAIL verifier (external/ebpf-verifier). This skill covers linux-compatible eBPF programs that can be verified directly with the PREVAIL check or run_yaml tools.

When to Use

User shares a PREVAIL verifier error or log and asks why verification failed
User asks to diagnose, debug, or explain an eBPF verification failure in the PREVAIL repo (external/ebpf-verifier)
User asks to debug PREVAIL YAML test failures or abstract-interpretation issues
User is working on verifier internals (abstract domains, widening, transformers)
User mentions "verifier", "verification", "PREVAIL", or "abstract interpretation" errors for linux-compatible BPF programs

When NOT to Use

Program uses Windows-specific helpers or headers (e.g., ebpf_helpers.h, sample_ext_helpers.h, WFP hook types) → use verify-bpf instead
User wants to run the bpf2c pipeline (clang → bpf2c → native driver) → use verify-bpf instead
User needs to compile a .c BPF source to .o for ebpf-for-windows → use verify-bpf instead

Reference Document

Read the full PREVAIL diagnostic reference before diagnosing:

external/ebpf-verifier/docs/llm-context.md

This document contains:

How to interpret PREVAIL log output (register state, stack state, invariants)
Glossary of log terms, types, type groups, and assertions
Common failure patterns with symptoms, causes, and fixes
Advanced topics (widening, path-insensitivity, pointer provenance)
A step-by-step reasoning protocol for diagnosis

Always read this file first — it is the authoritative reference for PREVAIL diagnostics.

Diagnosis Instructions

Step 1: Read the Reference

Read external/ebpf-verifier/docs/llm-context.md to load the full diagnostic context.

Step 2: Gather the Error

Ask the user to provide (if not already given):

The verifier error message (the line with <pc>: <message> (<assertion>))
The pre-invariant at the failing instruction
The 3–5 instructions leading up to the failure
The source code of the eBPF program (or the relevant section)
Any map or context definitions (for map/context-related errors)

Step 3: Identify the Failure Pattern

Using the reference document, match the error to one of the common failure patterns:

Pattern	Key Symptom
Uninitialized register	`Invalid type (r<N>.type in {...})`
Unbounded packet access	`Upper bound must be at most packet_size`
Stack out-of-bounds	`Lower bound must be at least r10.stack_offset - EBPF_SUBPROGRAM_STACK_SIZE`
Null pointer (map lookup)	`Possible null access`
Type mismatch	`Only pointers can be dereferenced`
Pointer arithmetic error	`Only numbers can be added to pointers`
Infinite loop	`Loop counter is too large (pc[N] < 100000)`
Division by zero	`Possible division by zero`
Map key/value mismatch	`Illegal map update with a non-numerical value`
Context bounds violation	`Nonzero context offset` or context `Upper bound` error
Lost correlation (verifier limitation)	Bounds check present but verifier can't prove safety

Step 4: Trace the Root Cause

Follow the reasoning protocol from the reference:

Check the pre-invariant — what types and constraints do the relevant registers have?
Identify missing constraints — what constraint would make the assertion pass?
Trace backwards — where was the constraint lost or never established?
Check for verifier limitations — is this a code bug or a verifier precision issue?

Step 5: Recommend a Fix

Provide:

A clear explanation of why verification failed
The specific constraint that is missing or violated
A concrete code fix (with before/after examples when possible)
If it's a verifier limitation, suggest workarounds (direct pointer comparisons, restructured control flow, etc.)

Important Notes

PREVAIL is more conservative than the Linux kernel verifier — code accepted by Linux may be rejected by PREVAIL.
PREVAIL is path-insensitive — it uses a single abstract state per program point, so correlated conditions across branches may be lost.
Widening at loop headers can destroy constraints — if a loop-related failure occurs, check whether widening eliminated a needed bound.
Never assume a register has a type or constraint unless it appears in the pre-invariant.