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/sbpf/sbpfver"
"github.com/Overclock-Validator/mithril/pkg/sealevel"
)
const (
meterLimit = 1000
elfHeaderSize = 64
sectionHeaderSize = 64
textOffset = 0x100
)
var sanity = []byte{
0xb7, 0x00, 0x00, 0x00, 0x01, 0x00, 0x00, 0x00,
0x95, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
}
var candidate = []byte{
0xb7, 0x00, 0x00, 0x00, 0x05, 0x00, 0x00, 0x00,
0xb7, 0x01, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
0xf7, 0x01, 0x00, 0x00, 0x01, 0x00, 0x00, 0x00,
0x6e, 0x10, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
0x95, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
}
var statusCandidate = []byte{
0xb7, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
0xb7, 0x01, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
0xf7, 0x01, 0x00, 0x00, 0x01, 0x00, 0x00, 0x00,
0x6e, 0x10, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
0x95, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
}
// oracleUrem32 implements the linked sBPF V2 definition:
// ((dst as u32) % (src as u32)) as u64, with a zero-divisor error.
func oracleUrem32(dst, src uint64) (value uint64, divideByZero bool) {
src32 := uint32(src)
if src32 == 0 {
return 0, true
}
return uint64(uint32(dst) % src32), false
}
func printOracle(caseName string, dst, src uint64) {
value, divideByZero := oracleUrem32(dst, src)
if divideByZero {
fmt.Printf(
"oracle=sbpf_v2_spec case=%s execute=error error=DivideByZero\n",
caseName,
)
return
}
fmt.Printf(
"oracle=sbpf_v2_spec case=%s execute=ok r0=0x%016x\n",
caseName,
value,
)
}
func decode(raw []byte) []sbpf.Slot {
text := make([]sbpf.Slot, len(raw)/sbpf.SlotSize)
for i := range text {
text[i] = sbpf.Slot(binary.LittleEndian.Uint64(
raw[i*sbpf.SlotSize:],
))
}
return text
}
func execute(caseName string, raw []byte) (uint64, uint64, error) {
fmt.Printf("implementation=mithril case=%s version=V2 ", caseName)
program := &sbpf.Program{
RO: raw,
TextBytes: raw,
Text: decode(raw),
TextVA: sbpf.VaddrProgram,
Entrypoint: 0,
Funcs: nil,
SbpfVersion: sbpfver.SbpfVersion{Version: sbpfver.SbpfVersionV2},
}
if err := program.Verify(); err != nil {
fmt.Printf("verify=rejected error=%q\n", err)
return 0, 0, err
}
fmt.Print("verify=accepted ")
meter := cu.NewComputeMeter(meterLimit)
interpreter := sbpf.NewInterpreter(program, &sbpf.VMOpts{
HeapMax: 0,
Syscalls: func(uint32) (sbpf.Syscall, bool) {
return nil, false
},
MaxCU: meterLimit,
ComputeMeter: &meter,
Input: []byte{0},
InputDataVaddr: sbpf.VaddrInput,
})
defer interpreter.Finish()
value, count, err := interpreter.Run()
if err != nil {
fmt.Printf("execute=error error=%q instruction_count=%d\n", err, count)
return value, count, err
}
fmt.Printf("execute=ok r0=0x%016x instruction_count=%d\n", value, count)
return value, count, nil
}
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)
}
// makeV2ELF creates a complete ELF64 ET_DYN/EM_BPF image containing only
// the ELF header, .text, .shstrtab, and their section headers.
func makeV2ELF(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)
binary.LittleEndian.PutUint64(buf[40:48], uint64(sectionTableOffset))
binary.LittleEndian.PutUint32(buf[48:52], sbpfver.SbpfVersionV2)
binary.LittleEndian.PutUint16(buf[52:54], elfHeaderSize)
binary.LittleEndian.PutUint16(buf[54:56], 56)
binary.LittleEndian.PutUint16(buf[56:58], 0)
binary.LittleEndian.PutUint16(buf[58:60], sectionHeaderSize)
binary.LittleEndian.PutUint16(buf[60:62], sectionCount)
binary.LittleEndian.PutUint16(buf[62:64], 2)
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 executeLoaded(
program *sbpf.Program,
syscalls sbpf.SyscallRegistry,
) (uint64, uint64, error) {
meter := cu.NewComputeMeter(meterLimit)
interpreter := sbpf.NewInterpreter(program, &sbpf.VMOpts{
HeapMax: 0,
Syscalls: syscalls,
MaxCU: meterLimit,
ComputeMeter: &meter,
Input: []byte{0},
InputDataVaddr: sbpf.VaddrInput,
})
defer interpreter.Finish()
return interpreter.Run()
}
func executeElf(caseName string, entryText []byte) (uint64, uint64, error) {
fmt.Printf(
"implementation=mithril case=valid_elf_%s version=V2 ",
caseName,
)
elfBytes := makeV2ELF(entryText)
featureSet := features.NewFeaturesDefault()
featureSet.EnableFeature(
features.EnableSbpfV2DeploymentAndExecution,
0,
)
if err := sealevel.ValidateUpgradeableLoaderProgram(
elfBytes,
featureSet,
); err != nil {
fmt.Printf(
"deploy_validate=rejected elf_load=not_run "+
"verify=not_run execute=not_run error=%q\n",
err,
)
return 0, 0, err
}
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 {
fmt.Printf(
"elf_load=rejected verify=not_run "+
"execute=not_run error=%q\n",
err,
)
return 0, 0, err
}
program, err := loader.Load()
if err != nil {
fmt.Printf(
"elf_load=rejected verify=not_run "+
"execute=not_run error=%q\n",
err,
)
return 0, 0, err
}
fmt.Print("elf_load=accepted ")
if err := program.Verify(); err != nil {
fmt.Printf("verify=rejected execute=not_run error=%q\n", err)
return 0, 0, err
}
fmt.Print("verify=accepted ")
value, count, err := executeLoaded(program, syscalls)
if err != nil {
fmt.Printf("execute=error error=%q instruction_count=%d\n", err, count)
return value, count, err
}
fmt.Printf("execute=ok r0=0x%016x instruction_count=%d\n", value, count)
return value, count, nil
}
func main() {
printOracle("urem32_reg_width", 5, 0x0000000100000000)
value, count, err := execute("sanity", sanity)
if err != nil || value != 1 || count != 2 {
panic(fmt.Sprintf(
"unexpected sanity result: r0=%d count=%d err=%v",
value,
count,
err,
))
}
value, count, err = execute("urem32_reg_width", candidate)
if err != nil || value != 5 || count != 5 {
panic(fmt.Sprintf(
"unexpected candidate result: r0=%d count=%d err=%v",
value,
count,
err,
))
}
printOracle("valid_elf_urem32_status", 0, 0x0000000100000000)
value, count, err = executeElf("sanity", sanity)
if err != nil || value != 1 || count != 2 {
panic(fmt.Sprintf(
"unexpected ELF sanity result: r0=%d count=%d err=%v",
value,
count,
err,
))
}
value, count, err = executeElf(
"urem32_status",
statusCandidate,
)
if err != nil || value != 0 || count != 5 {
panic(fmt.Sprintf(
"unexpected ELF candidate result: r0=%d count=%d err=%v",
value,
count,
err,
))
}
}
Overview
Mithril implements the V2 UREM32_REG instruction with the full 64-bit source
and destination registers. A source whose low 32 bits are zero but whose high
32 bits are nonzero is therefore treated as a valid divisor instead of zero.
Minimal program:
Expected and observed result:
The standalone Go reproducer below also places a status-oriented form of the
same program in a valid V2 ELF. Mithril's official deployment validator,
loader, and verifier all accept that ELF, after which its interpreter returns
successfully with r0=0. The expected V2 behavior is DivideByZero. This is a
success-versus-error semantic difference, not an error-label difference or a
malformed-input case.
Configuration:
The valid-ELF path uses Mithril's official deployment syscall registry, but the
program makes no calls. It does not access guest memory, so memory mapping
details cannot influence the result.
Tested Versions
Root Cause
The sBPF bytecode definition specifies opcode 0x6e as
((dst as u32) % (src as u32)) as u64 and requires division-by-zero handling
after applying the operation's width:
The reference implementation casts the source to u32 for the zero check and
truncates both operands before computing the remainder. Mithril instead checks
the full uint64 source and performs a 64-bit remainder:
See Mithril's OpUrem32Reg handler.
Mithril's verifier correctly accepts the register-form instruction because the
runtime register value is not statically known:
The behavior was introduced by
commit 1fb0c24,
which fixed the earlier F-D17 missing divide-by-zero guard. Before that change,
the remainder correctly truncated both operands to uint32, but an all-zero
source could panic in Go. The repair added a full-width guard and also changed
the remainder to full-width arithmetic. This report concerns that operand-width
regression, not the already recognized absence of a guard.
Suggested Fix
Truncate both operands before the zero check and remainder:
Add regressions for:
program.
Reproduction
Expected Results
The two oracle lines are a direct calculation of the linked V2 definition, not
output attributed to an embedded Anza runner. The other four lines come from
Mithril's official verifier, interpreter, deployment validator, and ELF loader.
Both sanity and candidate assertions are enforced by the Go program.