---
# System prepended metadata

title: 'Specification and verification in the field: Applying formal methods to BPF just-in-time compilers in the Linux kernel'
tags: [論文メモ]

---

---
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の操作が含まれている
    