---
tags: 論文メモ
---

# Specification and verification in the field: Applying formal methods to BPF just-in-time compilers in the Linux kernel

## 背景

### 問題意識
- BPF JITの信頼性向上

### 問題への貢献
- jitterbug: JITの形式検証用フレームワーク
- RV32向けBPF JITの形式検証
- この過程で見つけた16個のバグのupstreamへのパッチ

## 具体的な手法など
- C likeなDSLで実装する
- Rosette
- DSLでサブセットを取り扱うことでjitterbug側でCの意味論をモデルするとかがなくなる
- 命令レベルの意味論中でSMTで解ける部分(bitvector云々)を公理として未解釈にしておいてSMTで解き,leanで答え合わせ
- smt builtinのbitvector操作は使わない
- 公理としてcomm,assoc,decomp,remなどにbitvectorの操作が含まれている