Jitterbug

This repository contains the tool described in our upcoming OSDI'20 paper "Specification, implementation, and verification of just-in-time compilers for an in-kernel virtual machine".

This is a tool for formally verifying the Linux kernel BPF JITs that builds on our verification framework [Serval]. We have used this tool to aid the development in the following ways:

• develop the RV32 JIT:

  • riscv, bpf: Add RV32G eBPF JIT

• review the patches that add support for far jumps and branching in RV64:

  • riscv, bpf: add support for far branching
  • riscv, bpf: add support for far jumps and exits

• find bugs, validate patches, and write test cases:

  • arm, bpf: Fix bugs with ALU64 {RSH, ARSH} BPF_K shift by 0
  • arm, bpf: Fix offset overflow for BPF_MEM BPF_DW
  • arm64: insn: Fix two bugs in encoding 32-bit logical immediates
  • bpf, riscv: clear high 32 bits for ALU32 add/sub/neg/lsh/rsh/arsh
  • bpf, riscv: Fix tail call count off by one in RV32 BPF JIT
  • bpf, riscv: Fix stack layout of JITed code on RV32
  • riscv, bpf: Fix offset range checking for auipc+jalr on RV64
  • bpf, x32: Fix bug with ALU64 {LSH, RSH, ARSH} BPF_K shift by 0
  • bpf, x32: Fix bug with ALU64 {LSH, RSH, ARSH} BPF_X shift by 0
  • bpf, x32: Fix bug with JMP32 JSET BPF_X checking upper bits
  • bpf, x86_32: Fix incorrect encoding in BPF_LDX zero-extension
  • bpf, x86_32: Fix clobbering of dst for BPF_JSET
  • bpf, x86: Fix encoding for lower 8-bit registers in BPF_STX BPF_B
  • bpf, selftests: Add test for BPF_STX BPF_B storing R10
  • selftests: bpf: Add test for JMP32 JSET BPF_X with upper bits set
  • selftests: bpf: add tests for shifts by zero

• add optimizations:

  • bpf, arm: Optimize ALU64 ARSH X using orrpl conditional instruction
  • bpf, arm: Optimize ALU ARSH K using asr immediate instruction
  • bpf, arm64: Optimize AND,OR,XOR,JSET BPF_K using arm64 logical immediates
  • bpf, arm64: Optimize ADD,SUB,JMP BPF_K using arm64 add/sub immediates
  • bpf, riscv: Enable zext optimization for more RV64G ALU ops
  • Merge branch 'bpf-rv64-jit'
    • bpf, riscv: Enable missing verifier_zext optimizations on RV64
    • bpf, riscv: Optimize FROM_LE using verifier_zext on RV64
    • bpf, riscv: Optimize BPF_JMP BPF_K when imm == 0 on RV64
    • bpf, riscv: Optimize BPF_JSET BPF_K using andi on RV64

• add RVC support to the RV64 JIT:

  • bpf, riscv: Modify JIT ctx to support compressed instructions
  • bpf, riscv: Add encodings for compressed instructions
  • bpf, riscv: Use compressed instructions in the rv64 JIT

How to install dependencies

• Download and install [Racket] (tested on v8.9).

• Uninstall any previous versions of Serval:

raco pkg remove serval

• Clone the repository and install a good version of Serval with BPF JIT verification and synthesis:

git clone --recursive 'https://github.com/uw-unsat/jitterbug.git'
cd jitterbug
raco pkg install --auto ./serval

You may also wish to install the [Boolector] SMT solver. We tested using Boolector v3.2.1 configured to use the CaDiCal SAT solver. The verification and synthesis will attempt to use it first, before falling back to Z3, which may take significantly longer (e.g., more than 10x slower for synthesis).

Directory structure

• arch/ contains the C code of the BPF JITs from the Linux kernel.

• racket/<arch>/ contains the Racket implementations of the BPF JITs that correspond to the C code under arch/.

  • racket/<arch>/spec.rkt contains the specification for <arch>.
  • racket/<arch>/synthesis.rkt (if present) contains the synthesis infrastructure and sketch for the BPF JIT for <arch>.
  • racket/rv32/bpf_jit_comp32.c.tmpl is a template used with the racket/rv32/bpf_jit_comp32.rkt to generate the final C implementation.

• racket/lib/ contains the BPF JIT verification infrastructure.

  • racket/lib/bpf-common.rkt contains the BPF JIT correctness specification and other common BPF functionality.
  • racket/lib/riscv-common.rkt provides features specific to the JIT for the RISC-V ISA.
  • racket/lib/bvaxiom.rkt axiomatizes bvmul/bvudiv/bvurem.
  • racket/lib/lemmas.lean contains the axiomatization of bitvector operations in Lean.

• racket/test/ contains verification and synthesis test cases for different classes of instructions.

Running verification

Run all of the verification test cases in parallel using 8 jobs:

raco test --jobs 8 racket/test

You can also run individual files for a specific class of instructions:

raco test racket/test/rv64/verify-alu32-x.rkt

Finding bugs via verification

As an example, let's inject a bug fixed in commit [1e692f09e091]. Specifically, remove the zero extension for BPF_ALU|BPF_ADD|BPF_X in racket/rv64/bpf_jit_comp64.rkt:

    [((BPF_ALU BPF_ADD BPF_X)
      (BPF_ALU64 BPF_ADD BPF_X))
     (emit (if is64 (rv_add rd rd rs) (rv_addw rd rd rs)) ctx)
     (when (&& (! is64) (! (->prog->aux->verifier_zext ctx)))
       (emit_zext_32 rd ctx))]

Now we have a buggy JIT implementation:

    [((BPF_ALU BPF_ADD BPF_X)
      (BPF_ALU64 BPF_ADD BPF_X))
     (emit (if is64 (rv_add rd rd rs) (rv_addw rd rd rs)) ctx)]

Run the verification:

raco test racket/test/rv64/verify-alu32-x.rkt

Verification will fail with a counterexample:

[ RUN      ] "VERIFY (BPF_ALU BPF_ADD BPF_X)"
<unknown>: <unknown>: bpf-jit-specification: Final registers must match
--------------------
riscv64-alu32-x tests > VERIFY (BPF_ALU BPF_ADD BPF_X)
FAILURE
name:       check-unsat?
location:   [...]/bpf-common.rkt:218:4
params:
  '((model
   [x?$0 #f]
   [r0$0 (bv #x0000000080000000 64)]
   [r1$0 (bv #x0000000000000000 64)]
   [insn$0 (bv #x00800000 32)]
   [offsets$0 (fv (bitvector 32)~>(bitvector 32))]
   [target-pc-base$0 (bv #x0000000000000000 64)]
   [off$0 (bv #x8000 16)]))
--------------------

The counterexample produced by the tool gives BPF register values that will trigger the bug: it chooses r0 to be 0x0000000080000000 and r1 to be 0x0000000000000000. This demonstrates the bug because the RISC-V instructions sign extend the result of the 32-bit addition, where the BPF instruction performs zero extension.

Verification

The verification works by proving equivalence between a BPF instruction and the RISC-V instructions generated by the JIT for that instruction.

As a concrete example, consider verifying the BPF_ALU|BPF_ADD|BPF_X instruction. The verification starts by constructing a symbolic BPF instruction where the destination and source register fields can take on any legit value:

BPF_ALU32_REG(BPF_ADD, {{rd}}, {{rs}})

Next, the verifier symbolically evaluates the JIT on the BPF instruction, producing a set of possible sequences of symbolic RISC-V instructions:

addw {{rv_reg(rd)}} {{rv_reg(rd)}} {{rv_reg(rs)}}
slli {{rv_reg(rd)}} {{rv_reg(rd)}} 32
srli {{rv_reg(rd)}} {{rv_reg(rd)}} 32

Here, rv_reg denotes the RISC-V register associated with a particular BPF register.

Next, the tool proves that every possible sequence of generated RISC-V instructions has the equivalent behavior as the original BPF instruction, for all possible choices of registers rd and rs, and for all initial values of all RISC-V general-purpose registers. To do so, it leverages automated verifiers provided by the [Serval] verification framework, as follows.

The verifier starts with a symbolic BPF state and symbolic RISC-V state, called bpf-state and riscv-state, assuming that the two initial states match, e.g., riscv-state[rv_reg(reg)] == bpf-state[reg] for all reg. Next, it runs the Serval BPF and RISC-V verifiers on the BPF instruction over bpf-state and every possible sequence of generated RISC-V instructions over riscv-state, respectively. It then proves that the final BPF and RISC-V states still match.

Support for more complex instructions, such as jumps and branches, requires additional care. For the details, you can see the