Documentation

Solanalib.SBPF.Verifier

SBPF.Verifier — static checks and the step-safety theorem #

The instruction-level part of the Solana verifier, ported from verifier.thy, and the safety property it guarantees (VerifierSafety.thy, Lemma 6.4): an instruction the verifier accepts never drives step into the err state (the "malformed instruction" outcome the verifier exists to exclude).

verifyInstr models the Err-relevant content of verify_one: the version gating (e.g. addStk/pqr are v2-only, neg/le are v1-only) and the non-zero-divisor checks. The byte-level checks of verify_one (check_load_dw, check_jmp_offset, check_registers) concern other safety properties (in-bounds jumps, register ranges) that do not affect Err-freedom and are omitted here.

Main definitions #

Main statements #

The verifier #

source
def Solanalib.SBPF.checkImmNonzero (sop : SndOp) :
Bool

A division/remainder immediate operand must be non-zero.

Equations
Instances For
    source
    def Solanalib.SBPF.verifyAlu (bop : Binop) (sop : SndOp) (isV1 : Bool) :
    Bool

    Version/divisor checks for an ALU op (mul/div/mod are v1-only; div/mod immediates must be non-zero).

    Equations
    Instances For
      source
      def Solanalib.SBPF.verifyPqr (pop : Pqrop) (sop : SndOp) :
      Bool

      Divisor checks for a PQR op (div/rem immediates must be non-zero).

      Equations
      Instances For
        source
        def Solanalib.SBPF.verifyInstr (ins : BpfInstruction) (sv : SBPFV) :
        Bool

        The instruction-level verifier (verify_one, Err-relevant content).

        Equations
        Instances For

          Supporting lemmas #

          source
          @[simp]
          theorem Solanalib.SBPF.sndOp32_imm (i : U32) (rs : RegMap) :
          sndOp32 (SndOp.imm i) rs = i
          source
          @[simp]
          theorem Solanalib.SBPF.sndOp64_imm (i : U32) (rs : RegMap) :
          sndOp64 (SndOp.imm i) rs = BitVec.signExtend 64 i
          source
          @[simp]
          theorem Solanalib.SBPF.signExtend64_eq_zero (i : U32) :
          BitVec.signExtend 64 i = 0 ↔ i = 0

          Sign-extending to 64 bits is zero exactly when the source is.

          source
          theorem Solanalib.SBPF.stepRegOutcome_ne_err {o : RegOutcome} {pc : U64} {m : Mem} {ss : StackState} {sv : SBPFV} {fm : FuncMap} {cur remain : U64} (h : o ≠ RegOutcome.nok) :
          stepRegOutcome o pc m ss sv fm cur remain ≠ BpfState.err

          A non-nok ALU result keeps step out of the err state.

          source
          theorem Solanalib.SBPF.evalAlu32_ne_nok {bop : Binop} {dst : BpfIReg} {sop : SndOp} {rs : RegMap} {isV1 : Bool} (h : verifyAlu bop sop isV1 = true) :
          evalAlu32 bop dst sop rs isV1 ≠ RegOutcome.nok

          The 32-bit ALU never faults to err on a verified instruction.

          source
          theorem Solanalib.SBPF.evalAlu64_ne_nok {bop : Binop} {dst : BpfIReg} {sop : SndOp} {rs : RegMap} {isV1 : Bool} (h : verifyAlu bop sop isV1 = true) :
          evalAlu64 bop dst sop rs isV1 ≠ RegOutcome.nok

          The 64-bit ALU never faults to err on a verified instruction.

          source
          theorem Solanalib.SBPF.evalPqr32_ne_nok {pop : Pqrop} {dst : BpfIReg} {sop : SndOp} {rs : RegMap} {isV1 : Bool} (h : verifyPqr pop sop = true) :
          evalPqr32 pop dst sop rs isV1 ≠ RegOutcome.nok

          The 32-bit PQR never faults to err on a verified instruction.

          source
          theorem Solanalib.SBPF.evalPqr64_ne_nok {pop : Pqrop} {dst : BpfIReg} {sop : SndOp} {rs : RegMap} {isV1 : Bool} (h : verifyPqr pop sop = true) :
          evalPqr64 pop dst sop rs isV1 ≠ RegOutcome.nok

          The 64-bit PQR never faults to err on a verified instruction.

          Safety #

          source
          theorem Solanalib.SBPF.step_ne_err {ins : BpfInstruction} {sv : SBPFV} (h : verifyInstr ins sv = true) (pc : U64) (rs : RegMap) (m : Mem) (ss : StackState) (fm : FuncMap) (gaps : Bool) (vmAddr cur remain : U64) :
          step pc ins rs m ss sv fm gaps vmAddr cur remain ≠ BpfState.err

          Verifier step-safety (Lemma 6.4): if verifyInstr accepts an instruction, then step on it never returns the err state.